Documentation

Mathlib.GroupTheory.NoncommPiCoprod

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 #

Main theorems #

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 (Commute on f)) (K : ιSubgroup G) (hind : iSupIndep K) (hmem : xs, f x K x) (heq1 : s.noncommProd f comm = 1) (i : ι) :
i sf 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 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 (AddCommute on f)) (K : ιAddSubgroup G) (hind : iSupIndep K) (hmem : xs, f x K x) (heq1 : s.noncommSum f comm = 0) (i : ι) :
i sf 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.

@[deprecated Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep]
theorem Subgroup.eq_one_of_noncommProd_eq_one_of_independent {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (f : ιG) (comm : (↑s).Pairwise (Commute on f)) (K : ιSubgroup G) (hind : iSupIndep K) (hmem : xs, f x K x) (heq1 : s.noncommProd f comm = 1) (i : ι) :
i sf i = 1

Alias of Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep.


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

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
  • 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)) :
    ((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
    • 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 MonoidHom.noncommPiCoprod_mulSingle {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)} [DecidableEq ι] (i : ι) (y : N i) :
      (MonoidHom.noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = (ϕ i) y
      @[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) :
      (AddMonoidHom.noncommPiCoprod ϕ hcomm) (Pi.single i y) = (ϕ i) y
      def MonoidHom.noncommPiCoprodEquiv {M : Type u_1} [Monoid M] {ι : Type u_2} [Fintype ι] {N : ιType u_3} [(i : ι) → Monoid (N i)] [DecidableEq ι] :
      { ϕ : (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.
      Instances For
        def AddMonoidHom.noncommPiCoprodEquiv {M : Type u_1} [AddMonoid M] {ι : Type u_2} [Fintype ι] {N : ιType u_3} [(i : ι) → AddMonoid (N i)] [DecidableEq ι] :
        { ϕ : (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.
        Instances For
          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)} :
          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) :
          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) :
          theorem MonoidHom.noncommPiCoprod_apply {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)} (h : (i : ι) → N i) :
          (MonoidHom.noncommPiCoprod ϕ hcomm) h = Finset.univ.noncommProd (fun (i : ι) => (ϕ i) (h i))
          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) :
          (AddMonoidHom.noncommPiCoprod ϕ hcomm) h = Finset.univ.noncommSum (fun (i : ι) => (ϕ i) (h i))
          theorem MonoidHom.noncommPiCoprod_range {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)} :
          (MonoidHom.noncommPiCoprod ϕ hcomm).range = ⨆ (i : ι), (ϕ i).range
          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)} :
          (AddMonoidHom.noncommPiCoprod ϕ hcomm).range = ⨆ (i : ι), (ϕ i).range
          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)) :
          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)) :
          @[deprecated MonoidHom.injective_noncommPiCoprod_of_iSupIndep]
          theorem MonoidHom.injective_noncommPiCoprod_of_independent {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)) :

          Alias of MonoidHom.injective_noncommPiCoprod_of_iSupIndep.

          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))) :
          iSupIndep fun (i : ι) => (ϕ i).range
          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))) :
          iSupIndep fun (i : ι) => (ϕ i).range
          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 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 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 iy H jAddCommute 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 iy H jCommute 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 iy H jAddCommute 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 iy H jCommute x y) :
          ((i : ι) → (H i)) →* G

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

          Equations
          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 iy H jAddCommute x y) :
            ((i : ι) → (H i)) →+ G

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

            Equations
            Instances For
              @[simp]
              theorem Subgroup.noncommPiCoprod_mulSingle {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} [Fintype ι] [DecidableEq ι] {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x H iy H jCommute x y} (i : ι) (y : (H i)) :
              @[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 iy H jAddCommute x y} (i : ι) (y : (H i)) :
              theorem Subgroup.noncommPiCoprod_range {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} [Fintype ι] {hcomm : Pairwise fun (i j : ι) => ∀ (x y : G), x H iy H jCommute x y} :
              (Subgroup.noncommPiCoprod hcomm).range = ⨆ (i : ι), 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 iy H jAddCommute x y} :
              (AddSubgroup.noncommPiCoprod hcomm).range = ⨆ (i : ι), H i
              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 iy H jCommute x y} (hind : iSupIndep H) :
              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 iy H jAddCommute x y} (hind : iSupIndep H) :
              theorem Subgroup.noncommPiCoprod_apply {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} [Fintype ι] (comm : Pairwise fun (i j : ι) => ∀ (x y : G), x H iy H jCommute x y) (u : (i : ι) → (H i)) :
              (Subgroup.noncommPiCoprod comm) u = Finset.univ.noncommProd (fun (i : ι) => (u i))
              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 iy H jAddCommute x y) (u : (i : ι) → (H i)) :
              (AddSubgroup.noncommPiCoprod comm) u = Finset.univ.noncommSum (fun (i : ι) => (u i))