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) →* M is the main homomorphism
• Subgroup.noncommPiCoprod : (Π i, H i) →* G is the specialization to H i : Subgroup G and the subgroup embedding.

Main theorems

• MonoidHom.noncommPiCoprod coincides with ϕ i when restricted to N i
• MonoidHom.noncommPiCoprod_mrange: The range of MonoidHom.noncommPiCoprod is ⨆ (i : ι), (ϕ i).mrange
• MonoidHom.noncommPiCoprod_range: The range of MonoidHom.noncommPiCoprod is ⨆ (i : ι), (ϕ i).range
• Subgroup.noncommPiCoprod_range: The range of Subgroup.noncommPiCoprod is ⨆ (i : ι), H i.
• MonoidHom.injective_noncommPiCoprod_of_independent: in the case of groups, pi_hom.hom is injective if the ϕ are injective and the ranges of the ϕ are independent.
• MonoidHom.independent_range_of_coprime_order: If the N i have coprime orders, then the ranges of the ϕ are independent.
• Subgroup.independent_of_coprime_order: If commuting normal subgroups H i have coprime orders, they are independent.

theorem AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_independent {G : Type u_1} [AddGroup G] {ι : Type u_2} (s : Finset ι) (f : ι → G) (comm : Set.Pairwise ↑s fun (a b : ι) => AddCommute (f a) (f b)) (K : ι → AddSubgroup G) (hind : CompleteLattice.Independent K) (hmem : ∀ x ∈ s, f x ∈ K x) (heq1 : Finset.noncommSum s f comm = 0) (i : ι) : i ∈ s → f i = 0

Finset.noncommSum is “injective” in f if f maps into independent subgroups. This generalizes (one direction of) AddSubgroup.disjoint_iff_add_eq_zero.

theorem Subgroup.eq_one_of_noncommProd_eq_one_of_independent {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (f : ι → G) (comm : Set.Pairwise ↑s fun (a b : ι) => Commute (f a) (f b)) (K : ι → Subgroup G) (hind : CompleteLattice.Independent K) (hmem : ∀ x ∈ s, f x ∈ K x) (heq1 : Finset.noncommProd s f comm = 1) (i : ι) : i ∈ s → f i = 1

Finset.noncommProd is “injective” in f if f maps into independent subgroups. This generalizes (one direction of) Subgroup.disjoint_iff_mul_eq_one.

theorem AddMonoidHom.noncommPiCoprod.proof_2 {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)) : Finset.noncommSum Finset.univ (fun (i : ι) => (ϕ i) (0 i)) ⋯ = 0

theorem AddMonoidHom.noncommPiCoprod.proof_3 {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)) (f : (i : ι) → N i) (g : (i : ι) → N i) : { toFun := fun (f : (i : ι) → N i) => Finset.noncommSum Finset.univ (fun (i : ι) => (ϕ i) (f i)) ⋯, map_zero' := ⋯ }.toFun (f + g) = { toFun := fun (f : (i : ι) → N i) => Finset.noncommSum Finset.univ (fun (i : ι) => (ϕ i) (f i)) ⋯, map_zero' := ⋯ }.toFun f + { toFun := fun (f : (i : ι) → N i) => Finset.noncommSum Finset.univ (fun (i : ι) => (ϕ i) (f i)) ⋯, map_zero' := ⋯ }.toFun g

theorem AddMonoidHom.noncommPiCoprod.proof_1 {M : Type u_2} [AddMonoid M] {ι : Type u_1} [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)) (f : (i : ι) → N i) (i : ι) : i ∈ ↑Finset.univ → ∀ j ∈ ↑Finset.univ, i ≠ j → AddCommute ((ϕ i) (f i)) ((ϕ j) (f j))

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)) : ((i : ι) → N i) →+ M

The canonical homomorphism from a family of additive monoids. See also LinearMap.lsum for a linear version without the commutativity assumption.

Equations

• One or more equations did not get rendered due to their size.

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)) : ((i : ι) → N i) →* M

The canonical homomorphism from a family of monoids.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddMonoidHom.noncommPiCoprod_single {M : Type u_1} [AddMonoid M] {ι : Type u_2} [DecidableEq ι] [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)} (i : ι) (y : N i) : (AddMonoidHom.noncommPiCoprod ϕ hcomm) (Pi.single i y) = (ϕ i) y

@[simp]

theorem MonoidHom.noncommPiCoprod_mulSingle {M : Type u_1} [Monoid M] {ι : Type u_2} [DecidableEq ι] [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)} (i : ι) (y : N i) : (MonoidHom.noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = (ϕ i) y

theorem AddMonoidHom.noncommPiCoprodEquiv.proof_3 {M : Type u_1} [AddMonoid M] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {N : ι → Type u_3} [(i : ι) → AddMonoid (N i)] (ϕ : { ϕ : (i : ι) → N i →+ M // Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) }) : (fun (f : ((i : ι) → N i) →+ M) => { val := fun (i : ι) => AddMonoidHom.comp f (AddMonoidHom.single N i), property := ⋯ }) ((fun (ϕ : { ϕ : (i : ι) → N i →+ M // Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) }) => AddMonoidHom.noncommPiCoprod ↑ϕ ⋯) ϕ) = ϕ

def AddMonoidHom.noncommPiCoprodEquiv {M : Type u_1} [AddMonoid M] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {N : ι → Type u_3} [(i : ι) → AddMonoid (N i)] : { ϕ : (i : ι) → N i →+ M // Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) } ≃ (((i : ι) → N i) →+ M)

The universal property of AddMonoidHom.noncommPiCoprod

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidHom.noncommPiCoprodEquiv.proof_1 {M : Type u_2} [AddMonoid M] {ι : Type u_1} {N : ι → Type u_3} [(i : ι) → AddMonoid (N i)] (ϕ : { ϕ : (i : ι) → N i →+ M // Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) }) : Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((↑ϕ i) x) ((↑ϕ j) y)

theorem AddMonoidHom.noncommPiCoprodEquiv.proof_4 {M : Type u_1} [AddMonoid M] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {N : ι → Type u_3} [(i : ι) → AddMonoid (N i)] (f : ((i : ι) → N i) →+ M) : (fun (ϕ : { ϕ : (i : ι) → N i →+ M // Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y) }) => AddMonoidHom.noncommPiCoprod ↑ϕ ⋯) ((fun (f : ((i : ι) → N i) →+ M) => { val := fun (i : ι) => AddMonoidHom.comp f (AddMonoidHom.single N i), property := ⋯ }) f) = f

theorem AddMonoidHom.noncommPiCoprodEquiv.proof_2 {M : Type u_2} [AddMonoid M] {ι : Type u_1} [DecidableEq ι] {N : ι → Type u_3} [(i : ι) → AddMonoid (N i)] (f : ((i : ι) → N i) →+ M) (i : ι) (j : ι) (hij : i ≠ j) (x : N i) (y : N j) : AddCommute (f (Pi.single i x)) (f (Pi.single j y))

def MonoidHom.noncommPiCoprodEquiv {M : Type u_1} [Monoid M] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {N : ι → Type u_3} [(i : ι) → Monoid (N i)] : { ϕ : (i : ι) → N i →* M // Pairwise fun (i j : ι) => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y) } ≃ (((i : ι) → N i) →* M)

The universal property of MonoidHom.noncommPiCoprod

Equations

• One or more equations did not get rendered due to their size.

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)} : AddMonoidHom.mrange (AddMonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), AddMonoidHom.mrange (ϕ i)

theorem MonoidHom.noncommPiCoprod_mrange {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)} : MonoidHom.mrange (MonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), MonoidHom.mrange (ϕ i)

theorem AddMonoidHom.noncommPiCoprod_range {G : Type u_1} [AddGroup G] {ι : Type u_2} [hfin : Fintype ι] {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)} : AddMonoidHom.range (AddMonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), AddMonoidHom.range (ϕ i)

theorem MonoidHom.noncommPiCoprod_range {G : Type u_1} [Group G] {ι : Type u_2} [hfin : Fintype ι] {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)} : MonoidHom.range (MonoidHom.noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), MonoidHom.range (ϕ i)

theorem AddMonoidHom.injective_noncommPiCoprod_of_independent {G : Type u_1} [AddGroup G] {ι : Type u_2} [hfin : Fintype ι] {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)} (hind : CompleteLattice.Independent fun (i : ι) => AddMonoidHom.range (ϕ i)) (hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)) : Function.Injective ⇑(AddMonoidHom.noncommPiCoprod ϕ hcomm)

theorem MonoidHom.injective_noncommPiCoprod_of_independent {G : Type u_1} [Group G] {ι : Type u_2} [hfin : Fintype ι] {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)} (hind : CompleteLattice.Independent fun (i : ι) => MonoidHom.range (ϕ i)) (hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)) : Function.Injective ⇑(MonoidHom.noncommPiCoprod ϕ hcomm)

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 : ι) => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) : CompleteLattice.Independent fun (i : ι) => AddMonoidHom.range (ϕ i)

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 : ι) => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) : CompleteLattice.Independent fun (i : ι) => MonoidHom.range (ϕ i)

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 ((AddSubgroup.subtype (H i)) x) ((AddSubgroup.subtype (H j)) y)

theorem Subgroup.commute_subtype_of_commute {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) (i : ι) (j : ι) (hne : i ≠ j) (x : ↥(H i)) (y : ↥(H j)) : Commute ((Subgroup.subtype (H i)) x) ((Subgroup.subtype (H j)) y)

theorem AddSubgroup.noncommPiCoprod.proof_1 {G : Type u_2} [AddGroup G] {ι : Type u_1} {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 ((AddSubgroup.subtype (H i)) x) ((AddSubgroup.subtype (H j)) y)

def AddSubgroup.noncommPiCoprod {G : Type u_1} [AddGroup G] {ι : Type u_2} [hfin : Fintype ι] {H : ι → AddSubgroup G} (hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y) : ((i : ι) → ↥(H i)) →+ G

The canonical homomorphism from a family of additive subgroups where elements from different subgroups commute

Equations

• AddSubgroup.noncommPiCoprod hcomm = AddMonoidHom.noncommPiCoprod (fun (i : ι) => AddSubgroup.subtype (H i)) ⋯

def Subgroup.noncommPiCoprod {G : Type u_1} [Group G] {ι : Type u_2} [hfin : Fintype ι] {H : ι → Subgroup G} (hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) : ((i : ι) → ↥(H i)) →* G

The canonical homomorphism from a family of subgroups where elements from different subgroups commute

Equations

• Subgroup.noncommPiCoprod hcomm = MonoidHom.noncommPiCoprod (fun (i : ι) => Subgroup.subtype (H i)) ⋯

@[simp]

theorem AddSubgroup.noncommPiCoprod_single {G : Type u_1} [AddGroup G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ι → AddSubgroup G} {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y} (i : ι) (y : ↥(H i)) : (AddSubgroup.noncommPiCoprod hcomm) (Pi.single i y) = ↑y

@[simp]

theorem Subgroup.noncommPiCoprod_mulSingle {G : Type u_1} [Group G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ι → Subgroup G} {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y} (i : ι) (y : ↥(H i)) : (Subgroup.noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y

theorem AddSubgroup.noncommPiCoprod_range {G : Type u_1} [AddGroup G] {ι : Type u_2} [hfin : Fintype ι] {H : ι → AddSubgroup G} {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y} : AddMonoidHom.range (AddSubgroup.noncommPiCoprod hcomm) = ⨆ (i : ι), H i

theorem Subgroup.noncommPiCoprod_range {G : Type u_1} [Group G] {ι : Type u_2} [hfin : Fintype ι] {H : ι → Subgroup G} {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y} : MonoidHom.range (Subgroup.noncommPiCoprod hcomm) = ⨆ (i : ι), H i

theorem AddSubgroup.injective_noncommPiCoprod_of_independent {G : Type u_1} [AddGroup G] {ι : Type u_2} [hfin : Fintype ι] {H : ι → AddSubgroup G} {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y} (hind : CompleteLattice.Independent H) : Function.Injective ⇑(AddSubgroup.noncommPiCoprod hcomm)

theorem Subgroup.injective_noncommPiCoprod_of_independent {G : Type u_1} [Group G] {ι : Type u_2} [hfin : Fintype ι] {H : ι → Subgroup G} {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y} (hind : CompleteLattice.Independent H) : Function.Injective ⇑(Subgroup.noncommPiCoprod hcomm)

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 : ι) => Nat.Coprime (Fintype.card ↥(H i)) (Fintype.card ↥(H j))) : CompleteLattice.Independent H

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 : ι) => Nat.Coprime (Fintype.card ↥(H i)) (Fintype.card ↥(H j))) : CompleteLattice.Independent H