Canonical homomorphism from a finite family of monoids #
This file defines the construction of the canonical homomorphism from a family of monoids.
Given a family of morphisms ϕ i : N i →* M for each i : ι where elements in the
images of different morphisms commute, we obtain a canonical morphism
MonoidHom.noncommPiCoprod : (Π i, N i) →* M that coincides with ϕ
Main definitions #
MonoidHom.noncommPiCoprod : (Π i, N i) →* Mis the main homomorphismSubgroup.noncommPiCoprod : (Π i, H i) →* Gis the specialization toH i : Subgroup Gand the subgroup embedding.
Main theorems #
MonoidHom.noncommPiCoprodcoincides withϕ iwhen restricted toN iMonoidHom.noncommPiCoprod_mrange: The range ofMonoidHom.noncommPiCoprodis⨆ (i : ι), (ϕ i).mrangeMonoidHom.noncommPiCoprod_range: The range ofMonoidHom.noncommPiCoprodis⨆ (i : ι), (ϕ i).rangeSubgroup.noncommPiCoprod_range: The range ofSubgroup.noncommPiCoprodis⨆ (i : ι), H i.MonoidHom.injective_noncommPiCoprod_of_iSupIndep: in the case of groups,pi_hom.homis injective if theϕare injective and the ranges of theϕare independent.MonoidHom.independent_range_of_coprime_order: If theN ihave coprime orders, then the ranges of theϕare independent.Subgroup.independent_of_coprime_order: If commuting normal subgroupsH ihave coprime orders, they are independent.
theorem
Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep
{G : Type u_1}
[Group G]
{ι : Type u_2}
(s : Finset ι)
(f : ι → G)
(comm : (↑s).Pairwise (Function.onFun Commute f))
(K : ι → Subgroup G)
(hind : iSupIndep K)
(hmem : ∀ x ∈ s, f x ∈ K x)
(heq1 : s.noncommProd f comm = 1)
(i : ι)
:
Finset.noncommProd is “injective” in f if f maps into independent subgroups. This
generalizes (one direction of) Subgroup.disjoint_iff_mul_eq_one.
theorem
AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_iSupIndep
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
(s : Finset ι)
(f : ι → G)
(comm : (↑s).Pairwise (Function.onFun AddCommute f))
(K : ι → AddSubgroup G)
(hind : iSupIndep K)
(hmem : ∀ x ∈ s, f x ∈ K x)
(heq1 : s.noncommSum f comm = 0)
(i : ι)
:
Finset.noncommSum is “injective” in f if f maps into independent subgroups.
This generalizes (one direction of) AddSubgroup.disjoint_iff_add_eq_zero.
def
MonoidHom.noncommPiCoprod
{M : Type u_1}
[Monoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → Monoid (N i)]
(ϕ : (i : ι) → N i →* M)
(hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y))
:
The canonical homomorphism from a family of monoids.
Equations
- MonoidHom.noncommPiCoprod ϕ hcomm = { toFun := fun (f : (i : ι) → N i) => Finset.univ.noncommProd (fun (i : ι) => (ϕ i) (f i)) ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
def
AddMonoidHom.noncommPiCoprod
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
(ϕ : (i : ι) → N i →+ M)
(hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y))
:
The canonical homomorphism from a family of additive monoids. See also
LinearMap.lsum for a linear version without the commutativity assumption.
Equations
- AddMonoidHom.noncommPiCoprod ϕ hcomm = { toFun := fun (f : (i : ι) → N i) => Finset.univ.noncommSum (fun (i : ι) => (ϕ i) (f i)) ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
AddMonoidHom.noncommPiCoprod_single
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
(ϕ : (i : ι) → N i →+ M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)}
[DecidableEq ι]
(i : ι)
(y : N i)
:
def
MonoidHom.noncommPiCoprodEquiv
{M : Type u_1}
[Monoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → Monoid (N i)]
[DecidableEq ι]
:
The universal property of MonoidHom.noncommPiCoprod
Given monoid morphisms φᵢ : Nᵢ → M whose images pairwise commute,
there exists a unique monoid morphism φ : Πᵢ Nᵢ → M that induces the φᵢ,
and it is given by MonoidHom.noncommPiCoprod.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
AddMonoidHom.noncommPiCoprodEquiv
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
[DecidableEq ι]
:
The universal property of MonoidHom.noncommPiCoprod
Given monoid morphisms φᵢ : Nᵢ → M whose images pairwise commute,
there exists a unique monoid morphism φ : Πᵢ Nᵢ → M that induces the φᵢ,
and it is given by AddMonoidHom.noncommPiCoprod.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AddMonoidHom.noncommPiCoprod_mrange
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
(ϕ : (i : ι) → N i →+ M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)}
:
theorem
MonoidHom.commute_noncommPiCoprod
{M : Type u_1}
[Monoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → Monoid (N i)]
(ϕ : (i : ι) → N i →* M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)}
{m : M}
(comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x))
(h : (i : ι) → N i)
:
Commute m ((noncommPiCoprod ϕ hcomm) h)
theorem
AddMonoidHom.addCommute_noncommPiCoprod
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
(ϕ : (i : ι) → N i →+ M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)}
{m : M}
(comm : ∀ (i : ι) (x : N i), AddCommute m ((ϕ i) x))
(h : (i : ι) → N i)
:
AddCommute m ((noncommPiCoprod ϕ hcomm) h)
theorem
AddMonoidHom.noncommPiCoprod_apply
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
(ϕ : (i : ι) → N i →+ M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)}
(h : (i : ι) → N i)
:
theorem
MonoidHom.comp_noncommPiCoprod
{M : Type u_1}
[Monoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → Monoid (N i)]
(ϕ : (i : ι) → N i →* M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)}
{P : Type u_4}
[Monoid P]
{f : M →* P}
(hcomm' : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), Commute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y) := ⋯)
:
Given monoid morphisms φᵢ : Nᵢ → M and f : M → P, if we have sufficient commutativity, then
f ∘ (∐ᵢ φᵢ) = ∐ᵢ (f ∘ φᵢ)
theorem
AddMonoidHom.comp_noncommPiCoprod
{M : Type u_1}
[AddMonoid M]
{ι : Type u_2}
[Fintype ι]
{N : ι → Type u_3}
[(i : ι) → AddMonoid (N i)]
(ϕ : (i : ι) → N i →+ M)
{hcomm : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)}
{P : Type u_4}
[AddMonoid P]
{f : M →+ P}
(hcomm' : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y) := ⋯)
:
theorem
AddMonoidHom.noncommPiCoprod_range
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → Type u_3}
[(i : ι) → AddGroup (H i)]
(ϕ : (i : ι) → H i →+ G)
[Fintype ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)}
:
theorem
MonoidHom.injective_noncommPiCoprod_of_iSupIndep
{G : Type u_1}
[Group G]
{ι : Type u_2}
{H : ι → Type u_3}
[(i : ι) → Group (H i)]
(ϕ : (i : ι) → H i →* G)
[Fintype ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)}
(hind : iSupIndep fun (i : ι) => (ϕ i).range)
(hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i))
:
Function.Injective ⇑(noncommPiCoprod ϕ hcomm)
theorem
AddMonoidHom.injective_noncommPiCoprod_of_iSupIndep
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → Type u_3}
[(i : ι) → AddGroup (H i)]
(ϕ : (i : ι) → H i →+ G)
[Fintype ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y)}
(hind : iSupIndep fun (i : ι) => (ϕ i).range)
(hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i))
:
Function.Injective ⇑(noncommPiCoprod ϕ hcomm)
theorem
MonoidHom.independent_range_of_coprime_order
{G : Type u_1}
[Group G]
{ι : Type u_2}
{H : ι → Type u_3}
[(i : ι) → Group (H i)]
(ϕ : (i : ι) → H i →* G)
(hcomm : Pairwise fun (i j : ι) => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y))
[Finite ι]
[(i : ι) → Fintype (H i)]
(hcoprime : Pairwise fun (i j : ι) => (Fintype.card (H i)).Coprime (Fintype.card (H j)))
:
theorem
AddMonoidHom.independent_range_of_coprime_order
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → Type u_3}
[(i : ι) → AddGroup (H i)]
(ϕ : (i : ι) → H i →+ G)
(hcomm : Pairwise fun (i j : ι) => ∀ (x : H i) (y : H j), AddCommute ((ϕ i) x) ((ϕ j) y))
[Finite ι]
[(i : ι) → Fintype (H i)]
(hcoprime : Pairwise fun (i j : ι) => (Fintype.card (H i)).Coprime (Fintype.card (H j)))
:
theorem
AddSubgroup.addCommute_subtype_of_addCommute
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
(hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y)
(i j : ι)
(hne : i ≠ j)
(x : ↥(H i))
(y : ↥(H j))
:
AddCommute ((H i).subtype x) ((H j).subtype y)
theorem
Subgroup.independent_of_coprime_order
{G : Type u_1}
[Group G]
{ι : Type u_2}
{H : ι → Subgroup G}
(hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y)
[Finite ι]
[(i : ι) → Fintype ↥(H i)]
(hcoprime : Pairwise fun (i j : ι) => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j)))
:
theorem
AddSubgroup.independent_of_coprime_order
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
(hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y)
[Finite ι]
[(i : ι) → Fintype ↥(H i)]
(hcoprime : Pairwise fun (i j : ι) => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j)))
:
def
Subgroup.noncommPiCoprod
{G : Type u_1}
[Group G]
{ι : Type u_2}
{H : ι → Subgroup G}
[Fintype ι]
(hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y)
:
The canonical homomorphism from a family of subgroups where elements from different subgroups commute
Equations
- Subgroup.noncommPiCoprod hcomm = MonoidHom.noncommPiCoprod (fun (i : ι) => (H i).subtype) ⋯
Instances For
def
AddSubgroup.noncommPiCoprod
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
[Fintype ι]
(hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y)
:
The canonical homomorphism from a family of additive subgroups where elements from different subgroups commute
Equations
- AddSubgroup.noncommPiCoprod hcomm = AddMonoidHom.noncommPiCoprod (fun (i : ι) => (H i).subtype) ⋯
Instances For
@[simp]
theorem
AddSubgroup.noncommPiCoprod_single
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
[Fintype ι]
[DecidableEq ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y}
(i : ι)
(y : ↥(H i))
:
theorem
AddSubgroup.noncommPiCoprod_range
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
[Fintype ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y}
:
theorem
Subgroup.injective_noncommPiCoprod_of_iSupIndep
{G : Type u_1}
[Group G]
{ι : Type u_2}
{H : ι → Subgroup G}
[Fintype ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y}
(hind : iSupIndep H)
:
Function.Injective ⇑(noncommPiCoprod hcomm)
theorem
AddSubgroup.injective_noncommPiCoprod_of_iSupIndep
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
[Fintype ι]
{hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y}
(hind : iSupIndep H)
:
Function.Injective ⇑(noncommPiCoprod hcomm)
theorem
AddSubgroup.noncommPiCoprod_apply
{G : Type u_1}
[AddGroup G]
{ι : Type u_2}
{H : ι → AddSubgroup G}
[Fintype ι]
(comm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y)
(u : (i : ι) → ↥(H i))
: