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 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 : ι), x sf x K x) (heq1 : Finset.noncommSum s 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.

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 : ι), x sf x K x) (heq1 : Finset.noncommProd s 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 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) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i)) fun i x j x h => hcomm i j h (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 j)) = 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) :
ZeroHom.toFun { toFun := fun f => Finset.noncommSum Finset.univ (fun i => ↑(ϕ i) (f i)) fun i x j x h => hcomm i j h (f i) (f j), map_zero' := (_ : (Finset.noncommSum Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i)) fun i x j x h => hcomm i j h (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 j)) = 0) } (f + g) = ZeroHom.toFun { toFun := fun f => Finset.noncommSum Finset.univ (fun i => ↑(ϕ i) (f i)) fun i x j x h => hcomm i j h (f i) (f j), map_zero' := (_ : (Finset.noncommSum Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i)) fun i x j x h => hcomm i j h (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 j)) = 0) } f + ZeroHom.toFun { toFun := fun f => Finset.noncommSum Finset.univ (fun i => ↑(ϕ i) (f i)) fun i x j x h => hcomm i j h (f i) (f j), map_zero' := (_ : (Finset.noncommSum Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i)) fun i x j x h => hcomm i j h (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 i) (OfNat.ofNat ((i : ι) → N i) 0 Zero.toOfNat0 j)) = 0) } 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 : ι), j Finset.univi jAddCommute (↑(ϕ 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.
Instances For
    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.
    Instances For
      @[simp]
      theorem AddMonoidHom.noncommPiCoprod_single {M : Type u_1} [AddMonoid M] {ι : Type u_2} [hdec : 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} [hdec : 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
      def AddMonoidHom.noncommPiCoprodEquiv {M : Type u_1} [AddMonoid M] {ι : Type u_2} [hdec : DecidableEq ι] [Fintype ι] {N : ιType u_3} [(i : ι) → AddMonoid (N i)] :
      { ϕ // 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 AddMonoidHom.noncommPiCoprodEquiv.proof_4 {M : Type u_1} [AddMonoid M] {ι : Type u_2} [hdec : DecidableEq ι] [Fintype ι] {N : ιType u_3} [(i : ι) → AddMonoid (N i)] (f : ((i : ι) → N i) →+ M) :
        (fun ϕ => AddMonoidHom.noncommPiCoprod ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute (↑(ϕ i) x) (↑(ϕ j) y))) ((fun f => { val := fun i => AddMonoidHom.comp f (AddMonoidHom.single N i), property := (_ : ∀ (i j : ι), i j∀ (x : N i) (y : N j), AddCommute (f (Pi.single i x)) (f (Pi.single j y))) }) f) = f
        theorem AddMonoidHom.noncommPiCoprodEquiv.proof_3 {M : Type u_1} [AddMonoid M] {ι : Type u_2} [hdec : DecidableEq ι] [Fintype ι] {N : ιType u_3} [(i : ι) → AddMonoid (N i)] (ϕ : { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute (↑(ϕ i) x) (↑(ϕ j) y) }) :
        (fun f => { val := fun i => AddMonoidHom.comp f (AddMonoidHom.single N i), property := (_ : ∀ (i j : ι), i j∀ (x : N i) (y : N j), AddCommute (f (Pi.single i x)) (f (Pi.single j y))) }) ((fun ϕ => AddMonoidHom.noncommPiCoprod ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute (↑(ϕ i) x) (↑(ϕ j) y))) ϕ) = ϕ
        theorem AddMonoidHom.noncommPiCoprodEquiv.proof_1 {M : Type u_2} [AddMonoid M] {ι : Type u_1} {N : ιType u_3} [(i : ι) → AddMonoid (N i)] (ϕ : { ϕ // 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_2 {M : Type u_2} [AddMonoid M] {ι : Type u_1} [hdec : 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} [hdec : DecidableEq ι] [Fintype ι] {N : ιType u_3} [(i : ι) → Monoid (N i)] :
        { ϕ // 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
          theorem AddMonoidHom.noncommPiCoprod_mrange {M : Type u_1} [AddMonoid M] {ι : Type u_2} [hdec : 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)} :
          theorem MonoidHom.noncommPiCoprod_mrange {M : Type u_1} [Monoid M] {ι : Type u_2} [hdec : 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)} :
          theorem AddMonoidHom.noncommPiCoprod_range {G : Type u_1} [AddGroup G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ιType u_3} [(i : ι) → AddGroup (H i)] (ϕ : (i : ι) → H i →+ G) {hcomm : ∀ (i j : ι), i j∀ (x : H i) (y : H j), AddCommute (↑(ϕ i) x) (↑(ϕ j) y)} :
          theorem MonoidHom.noncommPiCoprod_range {G : Type u_1} [Group G] {ι : Type u_2} [hdec : DecidableEq ι] [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)} :
          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 : ∀ (i j : ι), 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)) :
          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 : ∀ (i j : ι), 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)) :
          theorem AddMonoidHom.independent_range_of_coprime_order {G : Type u_1} [AddGroup G] {ι : Type u_2} [hdec : DecidableEq ι] {H : ιType u_3} [(i : ι) → AddGroup (H i)] (ϕ : (i : ι) → H i →+ G) (hcomm : ∀ (i j : ι), i j∀ (x : H i) (y : H j), AddCommute (↑(ϕ i) x) (↑(ϕ j) y)) [Finite ι] [(i : ι) → Fintype (H i)] (hcoprime : ∀ (i j : ι), i jNat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
          theorem MonoidHom.independent_range_of_coprime_order {G : Type u_1} [Group G] {ι : Type u_2} [hdec : DecidableEq ι] {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 jNat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
          theorem AddSubgroup.commute_subtype_of_commute {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y) (i : ι) (j : ι) (hne : i j) (x : { x // x H i }) (y : { x // x 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 : ∀ (i j : ι), i j∀ (x y : G), x H iy H jCommute x y) (i : ι) (j : ι) (hne : i j) (x : { x // x H i }) (y : { x // x H j }) :
          Commute (↑(Subgroup.subtype (H i)) x) (↑(Subgroup.subtype (H j)) y)
          def AddSubgroup.noncommPiCoprod {G : Type u_1} [AddGroup G] {ι : Type u_2} [hfin : Fintype ι] {H : ιAddSubgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y) :
          ((i : ι) → { x // x H i }) →+ G

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem AddSubgroup.noncommPiCoprod.proof_1 {G : Type u_2} [AddGroup G] {ι : Type u_1} {H : ιAddSubgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y) (i : ι) (j : ι) (hne : i j) (x : { x // x H i }) (y : { x // x H j }) :
            AddCommute (↑(AddSubgroup.subtype (H i)) x) (↑(AddSubgroup.subtype (H j)) y)
            def Subgroup.noncommPiCoprod {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 : ι) → { x // x H i }) →* G

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem AddSubgroup.noncommPiCoprod_single {G : Type u_1} [AddGroup G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ιAddSubgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y} (i : ι) (y : { x // x H i }) :
              @[simp]
              theorem Subgroup.noncommPiCoprod_mulSingle {G : Type u_1} [Group G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ιSubgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jCommute x y} (i : ι) (y : { x // x H i }) :
              theorem AddSubgroup.noncommPiCoprod_range {G : Type u_1} [AddGroup G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ιAddSubgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y} :
              theorem Subgroup.noncommPiCoprod_range {G : Type u_1} [Group G] {ι : Type u_2} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ιSubgroup G} {hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jCommute 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 : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y} (hind : CompleteLattice.Independent H) :
              theorem Subgroup.injective_noncommPiCoprod_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 : CompleteLattice.Independent H) :
              theorem AddSubgroup.independent_of_coprime_order {G : Type u_1} [AddGroup G] {ι : Type u_2} [hdec : DecidableEq ι] {H : ιAddSubgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jAddCommute x y) [Finite ι] [(i : ι) → Fintype { x // x H i }] (hcoprime : ∀ (i j : ι), i jNat.Coprime (Fintype.card { x // x H i }) (Fintype.card { x // x H j })) :
              theorem Subgroup.independent_of_coprime_order {G : Type u_1} [Group G] {ι : Type u_2} [hdec : DecidableEq ι] {H : ιSubgroup G} (hcomm : ∀ (i j : ι), i j∀ (x y : G), x H iy H jCommute x y) [Finite ι] [(i : ι) → Fintype { x // x H i }] (hcoprime : ∀ (i j : ι), i jNat.Coprime (Fintype.card { x // x H i }) (Fintype.card { x // x H j })) :