mathlib documentation

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 #

Main theorems #

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) :
@[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) :
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)} :
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)} :
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)} :
(add_monoid_hom.noncomm_pi_coprod ϕ 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)} :
(monoid_hom.noncomm_pi_coprod ϕ 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 : ι → subgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jcommute x 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 : ι → add_subgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jadd_commute x 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 : ι → add_subgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jadd_commute x 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 : ι → subgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jcommute x 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 : ι → add_subgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jadd_commute x y} (i : ι) (y : (H i)) :
@[simp]
theorem subgroup.noncomm_pi_coprod_mul_single {G : Type u_1} [group G] {ι : Type u_2} [hdec : decidable_eq ι] [hfin : fintype ι] {H : ι → subgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jcommute x y} (i : ι) (y : (H i)) :
theorem subgroup.noncomm_pi_coprod_range {G : Type u_1} [group G] {ι : Type u_2} [hfin : fintype ι] {H : ι → subgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jcommute x 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 : ι → add_subgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jadd_commute x y} :
(add_subgroup.noncomm_pi_coprod hcomm).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 : ι → add_subgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jadd_commute x 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 : ι → subgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jcommute x y} (hind : complete_lattice.independent H) :
theorem subgroup.independent_of_coprime_order {G : Type u_1} [group G] {ι : Type u_2} {H : ι → subgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jcommute x 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 : ι → add_subgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jadd_commute x y) [finite ι] [Π (i : ι), fintype (H i)] (hcoprime : ∀ (i j : ι), i j(fintype.card (H i)).coprime (fintype.card (H j))) :