# mathlibdocumentation

group_theory.noncomm_pi_coprod

# 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 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.
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 : ∀ (i j : ι), 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 : ∀ (i j : ι), 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 : ∀ (i j : ι), 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 : ∀ (i j : ι), 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 : ∀ (i j : ι), 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 : ∀ (i j : ι), 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy 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 iy H j y) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : ∀ (i j : ι), i j(fintype.card (H i)).coprime (fintype.card (H j))) :