# mathlib3documentation

group_theory.noncomm_pi_coprod

# Canonical homomorphism from a finite family of monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 monoid_hom.noncomm_pi_coprod : (Π i, N i) →* M that coincides with ϕ

## Main definitions #

• monoid_hom.noncomm_pi_coprod : (Π i, N i) →* M is the main homomorphism
• subgroup.noncomm_pi_coprod : (Π i, H i) →* G is the specialization to H i : subgroup G and the subgroup embedding.

## Main theorems #

• monoid_hom.noncomm_pi_coprod coincides with ϕ i when restricted to N i
• monoid_hom.noncomm_pi_coprod_mrange: The range of monoid_hom.noncomm_pi_coprod is ⨆ (i : ι), (ϕ i).mrange
• monoid_hom.noncomm_pi_coprod_range: The range of monoid_hom.noncomm_pi_coprod is ⨆ (i : ι), (ϕ i).range
• subgroup.noncomm_pi_coprod_range: The range of subgroup.noncomm_pi_coprod is ⨆ (i : ι), H i.
• monoid_hom.injective_noncomm_pi_coprod_of_independent: in the case of groups, pi_hom.hom is injective if the ϕ are injective and the ranges of the ϕ are independent.
• monoid_hom.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 add_subgroup.eq_zero_of_noncomm_sum_eq_zero_of_independent {G : Type u_1} [add_group G] {ι : Type u_2} (s : finset ι) (f : ι G) (comm : s.pairwise (λ (a b : ι), add_commute (f a) (f b))) (K : ι ) (hind : complete_lattice.independent K) (hmem : (x : ι), x s f x K x) (heq1 : s.noncomm_sum f comm = 0) (i : ι) (H : i s) :
f i = 0

finset.noncomm_sum is “injective” in f if f maps into independent subgroups. This generalizes (one direction of) add_subgroup.disjoint_iff_add_eq_zero.

theorem subgroup.eq_one_of_noncomm_prod_eq_one_of_independent {G : Type u_1} [group G] {ι : Type u_2} (s : finset ι) (f : ι G) (comm : s.pairwise (λ (a b : ι), commute (f a) (f b))) (K : ι ) (hind : complete_lattice.independent K) (hmem : (x : ι), x s f x K x) (heq1 : s.noncomm_prod f comm = 1) (i : ι) (H : i s) :
f i = 1

finset.noncomm_prod is “injective” in f if f maps into independent subgroups. This generalizes (one direction of) subgroup.disjoint_iff_mul_eq_one.

def monoid_hom.noncomm_pi_coprod {M : Type u_1} [monoid M] {ι : Type u_2} [fintype ι] {N : ι Type u_3} [Π (i : ι), monoid (N i)] (ϕ : Π (i : ι), N i →* M) (hcomm : pairwise (λ (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
def add_monoid_hom.noncomm_pi_coprod {M : Type u_1} [add_monoid M] {ι : Type u_2} [fintype ι] {N : ι Type u_3} [Π (i : ι), add_monoid (N i)] (ϕ : Π (i : ι), N i →+ M) (hcomm : pairwise (λ (i j : ι), (x : N i) (y : N j), add_commute ((ϕ i) x) ((ϕ j) y))) :
(Π (i : ι), N i) →+ M

The canonical homomorphism from a family of additive monoids.

See also linear_map.lsum for a linear version without the commutativity assumption.

Equations
@[simp]
theorem monoid_hom.noncomm_pi_coprod_mul_single {M : Type u_1} [monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι Type u_3} [Π (i : ι), monoid (N i)] (ϕ : Π (i : ι), N i →* M) {hcomm : pairwise (λ (i j : ι), (x : N i) (y : N j), commute ((ϕ i) x) ((ϕ j) y))} (i : ι) (y : N i) :
hcomm) y) = (ϕ i) y
@[simp]
theorem add_monoid_hom.noncomm_pi_coprod_single {M : Type u_1} [add_monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι Type u_3} [Π (i : ι), add_monoid (N i)] (ϕ : Π (i : ι), N i →+ M) {hcomm : pairwise (λ (i j : ι), (x : N i) (y : N j), add_commute ((ϕ i) x) ((ϕ j) y))} (i : ι) (y : N i) :
hcomm) y) = (ϕ i) y
def monoid_hom.noncomm_pi_coprod_equiv {M : Type u_1} [monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι Type u_3} [Π (i : ι), monoid (N i)] :
{ϕ // pairwise (λ (i j : ι), (x : N i) (y : N j), commute ((ϕ i) x) ((ϕ j) y))} ((Π (i : ι), N i) →* M)

The universal property of noncomm_pi_coprod

Equations
def add_monoid_hom.noncomm_pi_coprod_equiv {M : Type u_1} [add_monoid M] {ι : Type u_2} [hdec : decidable_eq ι] [fintype ι] {N : ι Type u_3} [Π (i : ι), add_monoid (N i)] :
{ϕ // pairwise (λ (i j : ι), (x : N i) (y : N j), add_commute ((ϕ i) x) ((ϕ j) y))} ((Π (i : ι), N i) →+ M)

The universal property of noncomm_pi_coprod

Equations
theorem add_monoid_hom.noncomm_pi_coprod_mrange {M : Type u_1} [add_monoid M] {ι : Type u_2} [fintype ι] {N : ι Type u_3} [Π (i : ι), add_monoid (N i)] (ϕ : Π (i : ι), N i →+ M) {hcomm : pairwise (λ (i j : ι), (x : N i) (y : N j), add_commute ((ϕ i) x) ((ϕ j) y))} :
= (i : ι),
theorem monoid_hom.noncomm_pi_coprod_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 (λ (i j : ι), (x : N i) (y : N j), commute ((ϕ i) x) ((ϕ j) y))} :
= (i : ι), monoid_hom.mrange (ϕ i)
theorem add_monoid_hom.noncomm_pi_coprod_range {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι Type u_3} [Π (i : ι), add_group (H i)] (ϕ : Π (i : ι), H i →+ G) {hcomm : (i j : ι), i j (x : H i) (y : H j), add_commute ((ϕ i) x) ((ϕ j) y)} :
hcomm).range = (i : ι), (ϕ i).range
theorem monoid_hom.noncomm_pi_coprod_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 : (i j : ι), i j (x : H i) (y : H j), commute ((ϕ i) x) ((ϕ j) y)} :
hcomm).range = (i : ι), (ϕ i).range
theorem monoid_hom.injective_noncomm_pi_coprod_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 : (i j : ι), i j (x : H i) (y : H j), commute ((ϕ i) x) ((ϕ j) y)} (hind : complete_lattice.independent (λ (i : ι), (ϕ i).range)) (hinj : (i : ι), function.injective (ϕ i)) :
theorem add_monoid_hom.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι Type u_3} [Π (i : ι), add_group (H i)] (ϕ : Π (i : ι), H i →+ G) {hcomm : (i j : ι), i j (x : H i) (y : H j), add_commute ((ϕ i) x) ((ϕ j) y)} (hind : complete_lattice.independent (λ (i : ι), (ϕ i).range)) (hinj : (i : ι), function.injective (ϕ i)) :
theorem add_monoid_hom.independent_range_of_coprime_order {G : Type u_1} [add_group G] {ι : Type u_2} {H : ι Type u_3} [Π (i : ι), add_group (H i)] (ϕ : Π (i : ι), H i →+ G) (hcomm : (i j : ι), i j (x : H i) (y : H j), add_commute ((ϕ i) x) ((ϕ j) y)) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : (i j : ι), i j (fintype.card (H i)).coprime (fintype.card (H j))) :
complete_lattice.independent (λ (i : ι), (ϕ i).range)
theorem monoid_hom.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 : (i j : ι), i j (x : H i) (y : H j), commute ((ϕ i) x) ((ϕ j) y)) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : (i j : ι), i j (fintype.card (H i)).coprime (fintype.card (H j))) :
complete_lattice.independent (λ (i : ι), (ϕ i).range)
theorem subgroup.commute_subtype_of_commute {G : Type u_1} [group G] {ι : Type u_2} {H : ι } (hcomm : (i j : ι), i j (x y : G), x H i y H j y) (i j : ι) (hne : i j) (x : (H i)) (y : (H j)) :
commute (((H i).subtype) x) (((H j).subtype) y)
theorem add_subgroup.commute_subtype_of_commute {G : Type u_1} [add_group G] {ι : Type u_2} {H : ι } (hcomm : (i j : ι), i j (x y : G), x H i y H j y) (i j : ι) (hne : i j) (x : (H i)) (y : (H j)) :
add_commute (((H i).subtype) x) (((H j).subtype) y)
def add_subgroup.noncomm_pi_coprod {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι } (hcomm : (i j : ι), i j (x y : G), x H i y H j y) :
(Π (i : ι), (H i)) →+ G

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

Equations
def subgroup.noncomm_pi_coprod {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι } (hcomm : (i j : ι), i j (x y : G), x H i y H j y) :
(Π (i : ι), (H i)) →* G

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

Equations
@[simp]
theorem add_subgroup.noncomm_pi_coprod_single {G : Type u_1} [add_group G] {ι : Type u_2} [hdec : decidable_eq ι] [hfin : fintype ι] {H : ι } {hcomm : (i j : ι), i j (x y : G), x H i y H j y} (i : ι) (y : (H i)) :
y) = y
@[simp]
theorem subgroup.noncomm_pi_coprod_mul_single {G : Type u_1} [group G] {ι : Type u_2} [hdec : decidable_eq ι] [hfin : fintype ι] {H : ι } {hcomm : (i j : ι), i j (x y : G), x H i y H j y} (i : ι) (y : (H i)) :
theorem subgroup.noncomm_pi_coprod_range {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι } {hcomm : (i j : ι), i j (x y : G), x H i y H j y} :
(subgroup.noncomm_pi_coprod hcomm).range = (i : ι), H i
theorem add_subgroup.noncomm_pi_coprod_range {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι } {hcomm : (i j : ι), i j (x y : G), x H i y H j y} :
.range = (i : ι), H i
theorem add_subgroup.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [add_group G] {ι : Type u_2} [hfin : fintype ι] {H : ι } {hcomm : (i j : ι), i j (x y : G), x H i y H j y} (hind : complete_lattice.independent H) :
theorem subgroup.injective_noncomm_pi_coprod_of_independent {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι } {hcomm : (i j : ι), i j (x y : G), x H i y H j y} (hind : complete_lattice.independent H) :
theorem subgroup.independent_of_coprime_order {G : Type u_1} [group G] {ι : Type u_2} {H : ι } (hcomm : (i j : ι), i j (x y : G), x H i y H j y) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : (i j : ι), i j (fintype.card (H i)).coprime (fintype.card (H j))) :
theorem add_subgroup.independent_of_coprime_order {G : Type u_1} [add_group G] {ι : Type u_2} {H : ι } (hcomm : (i j : ι), i j (x y : G), x H i y H j y) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : (i j : ι), i j (fintype.card (H i)).coprime (fintype.card (H j))) :