Documentation

Mathlib.GroupTheory.Complement

Complements #

In this file we define the complement of a subgroup.

Main definitions #

Main results #

def AddSubgroup.IsComplement {G : Type u_1} [AddGroup G] (S : Set G) (T : Set G) :

S and T are complements if (+) : S × T → G is a bijection

Equations
Instances For
    def Subgroup.IsComplement {G : Type u_1} [Group G] (S : Set G) (T : Set G) :

    S and T are complements if (*) : S × T → G is a bijection. This notion generalizes left transversals, right transversals, and complementary subgroups.

    Equations
    Instances For
      @[reducible, inline]
      abbrev AddSubgroup.IsComplement' {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :

      H and K are complements if (+) : H × K → G is a bijection

      Equations
      Instances For
        @[reducible, inline]
        abbrev Subgroup.IsComplement' {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :

        H and K are complements if (*) : H × K → G is a bijection

        Equations
        Instances For
          def AddSubgroup.leftTransversals {G : Type u_1} [AddGroup G] (T : Set G) :
          Set (Set G)

          The set of left-complements of T : Set G

          Equations
          Instances For
            def Subgroup.leftTransversals {G : Type u_1} [Group G] (T : Set G) :
            Set (Set G)

            The set of left-complements of T : Set G

            Equations
            Instances For
              def AddSubgroup.rightTransversals {G : Type u_1} [AddGroup G] (S : Set G) :
              Set (Set G)

              The set of right-complements of S : Set G

              Equations
              Instances For
                def Subgroup.rightTransversals {G : Type u_1} [Group G] (S : Set G) :
                Set (Set G)

                The set of right-complements of S : Set G

                Equations
                Instances For
                  theorem AddSubgroup.isComplement'_def {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} :
                  H.IsComplement' K AddSubgroup.IsComplement H K
                  theorem Subgroup.isComplement'_def {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
                  H.IsComplement' K Subgroup.IsComplement H K
                  theorem AddSubgroup.isComplement_iff_existsUnique {G : Type u_1} [AddGroup G] {S : Set G} {T : Set G} :
                  AddSubgroup.IsComplement S T ∀ (g : G), ∃! x : S × T, x.1 + x.2 = g
                  theorem Subgroup.isComplement_iff_existsUnique {G : Type u_1} [Group G] {S : Set G} {T : Set G} :
                  Subgroup.IsComplement S T ∀ (g : G), ∃! x : S × T, x.1 * x.2 = g
                  theorem AddSubgroup.IsComplement.existsUnique {G : Type u_1} [AddGroup G] {S : Set G} {T : Set G} (h : AddSubgroup.IsComplement S T) (g : G) :
                  ∃! x : S × T, x.1 + x.2 = g
                  theorem Subgroup.IsComplement.existsUnique {G : Type u_1} [Group G] {S : Set G} {T : Set G} (h : Subgroup.IsComplement S T) (g : G) :
                  ∃! x : S × T, x.1 * x.2 = g
                  theorem AddSubgroup.IsComplement'.symm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H.IsComplement' K) :
                  K.IsComplement' H
                  theorem Subgroup.IsComplement'.symm {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.IsComplement' K) :
                  K.IsComplement' H
                  theorem AddSubgroup.isComplement'_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} :
                  H.IsComplement' K K.IsComplement' H
                  theorem Subgroup.isComplement'_comm {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
                  H.IsComplement' K K.IsComplement' H
                  theorem AddSubgroup.isComplement_singleton_left {G : Type u_1} [AddGroup G] {S : Set G} {g : G} :
                  AddSubgroup.IsComplement {g} S S = Set.univ
                  theorem Subgroup.isComplement_singleton_left {G : Type u_1} [Group G] {S : Set G} {g : G} :
                  Subgroup.IsComplement {g} S S = Set.univ
                  theorem AddSubgroup.isComplement_singleton_right {G : Type u_1} [AddGroup G] {S : Set G} {g : G} :
                  AddSubgroup.IsComplement S {g} S = Set.univ
                  theorem Subgroup.isComplement_singleton_right {G : Type u_1} [Group G] {S : Set G} {g : G} :
                  Subgroup.IsComplement S {g} S = Set.univ
                  theorem AddSubgroup.isComplement_univ_left {G : Type u_1} [AddGroup G] {S : Set G} :
                  AddSubgroup.IsComplement Set.univ S ∃ (g : G), S = {g}
                  theorem Subgroup.isComplement_univ_left {G : Type u_1} [Group G] {S : Set G} :
                  Subgroup.IsComplement Set.univ S ∃ (g : G), S = {g}
                  theorem AddSubgroup.isComplement_univ_right {G : Type u_1} [AddGroup G] {S : Set G} :
                  AddSubgroup.IsComplement S Set.univ ∃ (g : G), S = {g}
                  theorem Subgroup.isComplement_univ_right {G : Type u_1} [Group G] {S : Set G} :
                  Subgroup.IsComplement S Set.univ ∃ (g : G), S = {g}
                  theorem AddSubgroup.IsComplement.add_eq {G : Type u_1} [AddGroup G] {S : Set G} {T : Set G} (h : AddSubgroup.IsComplement S T) :
                  S + T = Set.univ
                  theorem Subgroup.IsComplement.mul_eq {G : Type u_1} [Group G] {S : Set G} {T : Set G} (h : Subgroup.IsComplement S T) :
                  S * T = Set.univ
                  theorem Subgroup.IsComplement.card_mul_card {G : Type u_1} [Group G] {S : Set G} {T : Set G} (h : Subgroup.IsComplement S T) :
                  theorem AddSubgroup.isComplement'_top_bot {G : Type u_1} [AddGroup G] :
                  .IsComplement'
                  theorem Subgroup.isComplement'_top_bot {G : Type u_1} [Group G] :
                  .IsComplement'
                  theorem AddSubgroup.isComplement'_bot_top {G : Type u_1} [AddGroup G] :
                  .IsComplement'
                  theorem Subgroup.isComplement'_bot_top {G : Type u_1} [Group G] :
                  .IsComplement'
                  @[simp]
                  theorem AddSubgroup.isComplement'_bot_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                  .IsComplement' H H =
                  @[simp]
                  theorem Subgroup.isComplement'_bot_left {G : Type u_1} [Group G] {H : Subgroup G} :
                  .IsComplement' H H =
                  @[simp]
                  theorem AddSubgroup.isComplement'_bot_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                  H.IsComplement' H =
                  @[simp]
                  theorem Subgroup.isComplement'_bot_right {G : Type u_1} [Group G] {H : Subgroup G} :
                  H.IsComplement' H =
                  @[simp]
                  theorem AddSubgroup.isComplement'_top_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                  .IsComplement' H H =
                  @[simp]
                  theorem Subgroup.isComplement'_top_left {G : Type u_1} [Group G] {H : Subgroup G} :
                  .IsComplement' H H =
                  @[simp]
                  theorem AddSubgroup.isComplement'_top_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                  H.IsComplement' H =
                  @[simp]
                  theorem Subgroup.isComplement'_top_right {G : Type u_1} [Group G] {H : Subgroup G} :
                  H.IsComplement' H =
                  theorem AddSubgroup.mem_leftTransversals_iff_existsUnique_neg_add_mem {G : Type u_1} [AddGroup G] {S : Set G} {T : Set G} :
                  S AddSubgroup.leftTransversals T ∀ (g : G), ∃! s : S, -s + g T
                  theorem Subgroup.mem_leftTransversals_iff_existsUnique_inv_mul_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} :
                  S Subgroup.leftTransversals T ∀ (g : G), ∃! s : S, (↑s)⁻¹ * g T
                  theorem AddSubgroup.mem_rightTransversals_iff_existsUnique_add_neg_mem {G : Type u_1} [AddGroup G] {S : Set G} {T : Set G} :
                  S AddSubgroup.rightTransversals T ∀ (g : G), ∃! s : S, g + -s T
                  theorem Subgroup.mem_rightTransversals_iff_existsUnique_mul_inv_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} :
                  S Subgroup.rightTransversals T ∀ (g : G), ∃! s : S, g * (↑s)⁻¹ T
                  theorem Subgroup.mem_leftTransversals_iff_bijective {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} :
                  S Subgroup.leftTransversals H Function.Bijective (S.restrict Quotient.mk'')
                  theorem Subgroup.mem_rightTransversals_iff_bijective {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} :
                  S Subgroup.rightTransversals H Function.Bijective (S.restrict Quotient.mk'')
                  theorem AddSubgroup.card_left_transversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S AddSubgroup.leftTransversals H) :
                  Nat.card S = H.index
                  theorem Subgroup.card_left_transversal {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S Subgroup.leftTransversals H) :
                  Nat.card S = H.index
                  theorem AddSubgroup.card_right_transversal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S AddSubgroup.rightTransversals H) :
                  Nat.card S = H.index
                  theorem Subgroup.card_right_transversal {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S Subgroup.rightTransversals H) :
                  Nat.card S = H.index
                  theorem AddSubgroup.range_mem_leftTransversals {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
                  theorem Subgroup.range_mem_leftTransversals {G : Type u_1} [Group G] {H : Subgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) :
                  theorem AddSubgroup.exists_left_transversal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (g : G) :
                  SAddSubgroup.leftTransversals H, g S
                  theorem Subgroup.exists_left_transversal {G : Type u_1} [Group G] (H : Subgroup G) (g : G) :
                  SSubgroup.leftTransversals H, g S
                  theorem Subgroup.exists_right_transversal {G : Type u_1} [Group G] (H : Subgroup G) (g : G) :
                  SSubgroup.rightTransversals H, g S
                  theorem AddSubgroup.exists_left_transversal_of_le {G : Type u_1} [AddGroup G] {H' : AddSubgroup G} {H : AddSubgroup G} (h : H' H) :
                  ∃ (S : Set G), S + H' = H Nat.card S * Nat.card H' = Nat.card H

                  Given two subgroups H' ⊆ H, there exists a transversal to H' inside H

                  theorem Subgroup.exists_left_transversal_of_le {G : Type u_1} [Group G] {H' : Subgroup G} {H : Subgroup G} (h : H' H) :
                  ∃ (S : Set G), S * H' = H Nat.card S * Nat.card H' = Nat.card H

                  Given two subgroups H' ⊆ H, there exists a left transversal to H' inside H.

                  theorem AddSubgroup.exists_right_transversal_of_le {G : Type u_1} [AddGroup G] {H' : AddSubgroup G} {H : AddSubgroup G} (h : H' H) :
                  ∃ (S : Set G), H' + S = H Nat.card H' * Nat.card S = Nat.card H

                  Given two subgroups H' ⊆ H, there exists a transversal to H' inside H

                  theorem Subgroup.exists_right_transversal_of_le {G : Type u_1} [Group G] {H' : Subgroup G} {H : Subgroup G} (h : H' H) :
                  ∃ (S : Set G), H' * S = H Nat.card H' * Nat.card S = Nat.card H

                  Given two subgroups H' ⊆ H, there exists a right transversal to H' inside H.

                  noncomputable def Subgroup.IsComplement.equiv {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) :
                  G S × T

                  The equivalence G ≃ S × T, such that the inverse is (*) : S × T → G

                  Equations
                  Instances For
                    @[simp]
                    theorem Subgroup.IsComplement.equiv_symm_apply {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) (x : S × T) :
                    hST.equiv.symm x = x.1 * x.2
                    @[simp]
                    theorem Subgroup.IsComplement.equiv_fst_mul_equiv_snd {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) (g : G) :
                    (hST.equiv g).1 * (hST.equiv g).2 = g
                    theorem Subgroup.IsComplement.equiv_fst_eq_mul_inv {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) (g : G) :
                    (hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹
                    theorem Subgroup.IsComplement.equiv_snd_eq_inv_mul {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) (g : G) :
                    (hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g
                    theorem Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S K) {g₁ : G} {g₂ : G} :
                    (hSK.equiv g₁).1 = (hSK.equiv g₂).1 LeftCosetEquivalence (↑K) g₁ g₂
                    theorem Subgroup.IsComplement.equiv_snd_eq_iff_rightCosetEquivalence {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) {g₁ : G} {g₂ : G} :
                    (hHT.equiv g₁).2 = (hHT.equiv g₂).2 RightCosetEquivalence (↑H) g₁ g₂
                    theorem Subgroup.IsComplement.leftCosetEquivalence_equiv_fst {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S K) (g : G) :
                    LeftCosetEquivalence (↑K) g (hSK.equiv g).1
                    theorem Subgroup.IsComplement.rightCosetEquivalence_equiv_snd {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) (g : G) :
                    RightCosetEquivalence (↑H) g (hHT.equiv g).2
                    theorem Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 T) (hg : g S) :
                    (hST.equiv g).1 = g, hg
                    theorem Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 S) (hg : g T) :
                    (hST.equiv g).2 = g, hg
                    theorem Subgroup.IsComplement.equiv_snd_eq_one_of_mem_of_one_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 T) (hg : g S) :
                    (hST.equiv g).2 = 1, h1
                    theorem Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 S) (hg : g T) :
                    (hST.equiv g).1 = 1, h1
                    @[simp]
                    theorem Subgroup.IsComplement.equiv_mul_right {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S K) (g : G) (k : K) :
                    hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
                    theorem Subgroup.IsComplement.equiv_mul_right_of_mem {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S K) {g : G} {k : G} (h : k K) :
                    hSK.equiv (g * k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k, h)
                    @[simp]
                    theorem Subgroup.IsComplement.equiv_mul_left {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) (h : H) (g : G) :
                    hHT.equiv (h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)
                    theorem Subgroup.IsComplement.equiv_mul_left_of_mem {G : Type u_1} [Group G] {H : Subgroup G} {T : Set G} (hHT : Subgroup.IsComplement (↑H) T) {h : G} {g : G} (hh : h H) :
                    hHT.equiv (h * g) = (h, hh * (hHT.equiv g).1, (hHT.equiv g).2)
                    theorem Subgroup.IsComplement.equiv_one {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) (hs1 : 1 S) (ht1 : 1 T) :
                    hST.equiv 1 = (1, hs1, 1, ht1)
                    theorem Subgroup.IsComplement.equiv_fst_eq_self_iff_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 T) :
                    (hST.equiv g).1 = g g S
                    theorem Subgroup.IsComplement.equiv_snd_eq_self_iff_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 S) :
                    (hST.equiv g).2 = g g T
                    theorem Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 S) :
                    (hST.equiv g).1 = 1 g T
                    theorem Subgroup.IsComplement.coe_equiv_snd_eq_one_iff_mem {G : Type u_1} [Group G] {S : Set G} {T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 T) :
                    (hST.equiv g).2 = 1 g S
                    noncomputable def AddSubgroup.MemLeftTransversals.toEquiv {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S AddSubgroup.leftTransversals H) :
                    G H S

                    A left transversal is in bijection with left cosets.

                    Equations
                    Instances For
                      noncomputable def Subgroup.MemLeftTransversals.toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S Subgroup.leftTransversals H) :
                      G H S

                      A left transversal is in bijection with left cosets.

                      Equations
                      Instances For
                        theorem AddSubgroup.MemLeftTransversals.finite_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S AddSubgroup.leftTransversals H) :
                        Finite S H.FiniteIndex

                        A left transversal is finite iff the subgroup has finite index

                        theorem Subgroup.MemLeftTransversals.finite_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S Subgroup.leftTransversals H) :
                        Finite S H.FiniteIndex
                        theorem AddSubgroup.MemLeftTransversals.toEquiv_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
                        theorem Subgroup.MemLeftTransversals.toEquiv_apply {G : Type u_1} [Group G] {H : Subgroup G} {f : G HG} (hf : ∀ (q : G H), (f q) = q) (q : G H) :
                        noncomputable def AddSubgroup.MemLeftTransversals.toFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S AddSubgroup.leftTransversals H) :
                        GS

                        A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

                        Equations
                        Instances For
                          noncomputable def Subgroup.MemLeftTransversals.toFun {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S Subgroup.leftTransversals H) :
                          GS

                          A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.

                          Equations
                          Instances For

                            A right transversal is in bijection with right cosets.

                            Equations
                            Instances For
                              noncomputable def Subgroup.MemRightTransversals.toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S Subgroup.rightTransversals H) :

                              A right transversal is in bijection with right cosets.

                              Equations
                              Instances For
                                theorem AddSubgroup.MemRightTransversals.finite_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (h : S AddSubgroup.rightTransversals H) :
                                Finite S H.FiniteIndex

                                A right transversal is finite iff the subgroup has finite index

                                theorem Subgroup.MemRightTransversals.finite_iff {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (h : S Subgroup.rightTransversals H) :
                                Finite S H.FiniteIndex
                                noncomputable def AddSubgroup.MemRightTransversals.toFun {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : S AddSubgroup.rightTransversals H) :
                                GS

                                A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

                                Equations
                                Instances For
                                  noncomputable def Subgroup.MemRightTransversals.toFun {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} (hS : S Subgroup.rightTransversals H) :
                                  GS

                                  A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.

                                  Equations
                                  Instances For
                                    Equations
                                    • AddSubgroup.instAddActionElemSetLeftTransversalsCoe = AddAction.mk
                                    Equations
                                    • Subgroup.instMulActionElemSetLeftTransversalsCoe = MulAction.mk
                                    theorem Subgroup.smul_toFun {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (T : (Subgroup.leftTransversals H)) (g : G) :
                                    theorem Subgroup.smul_toEquiv {G : Type u_1} [Group G] {H : Subgroup G} {F : Type u_2} [Group F] [MulAction F G] [MulAction.QuotientAction F H] (f : F) (T : (Subgroup.leftTransversals H)) (q : G H) :
                                    Equations
                                    • AddSubgroup.instInhabitedElemSetLeftTransversalsCoe = { default := Set.range Quotient.out', }
                                    Equations
                                    • Subgroup.instInhabitedElemSetLeftTransversalsCoe = { default := Set.range Quotient.out', }
                                    Equations
                                    • AddSubgroup.instInhabitedElemSetRightTransversalsCoe = { default := Set.range Quotient.out', }
                                    Equations
                                    • Subgroup.instInhabitedElemSetRightTransversalsCoe = { default := Set.range Quotient.out', }
                                    theorem Subgroup.IsComplement'.isCompl {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.IsComplement' K) :
                                    theorem Subgroup.IsComplement'.sup_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.IsComplement' K) :
                                    H K =
                                    theorem Subgroup.IsComplement'.disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.IsComplement' K) :
                                    theorem Subgroup.IsComplement'.index_eq_card {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.IsComplement' K) :
                                    K.index = Nat.card H
                                    theorem Subgroup.IsComplement.card_mul {G : Type u_1} [Group G] {S : Set G} {T : Set G} (h : Subgroup.IsComplement S T) :
                                    theorem Subgroup.IsComplement'.card_mul {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.IsComplement' K) :
                                    theorem Subgroup.isComplement'_of_disjoint_and_mul_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h1 : Disjoint H K) (h2 : H * K = Set.univ) :
                                    H.IsComplement' K
                                    theorem Subgroup.isComplement'_of_card_mul_and_disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Finite G] (h1 : Nat.card H * Nat.card K = Nat.card G) (h2 : Disjoint H K) :
                                    H.IsComplement' K
                                    theorem Subgroup.isComplement'_iff_card_mul_and_disjoint {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Finite G] :
                                    H.IsComplement' K Nat.card H * Nat.card K = Nat.card G Disjoint H K
                                    theorem Subgroup.isComplement'_of_coprime {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Finite G] (h1 : Nat.card H * Nat.card K = Nat.card G) (h2 : (Nat.card H).Coprime (Nat.card K)) :
                                    H.IsComplement' K
                                    theorem Subgroup.isComplement'_stabilizer {G : Type u_1} [Group G] {H : Subgroup G} {α : Type u_2} [MulAction G α] (a : α) (h1 : ∀ (h : H), h a = ah = 1) (h2 : ∀ (g : G), ∃ (h : H), h g a = a) :
                                    H.IsComplement' (MulAction.stabilizer G a)
                                    noncomputable def Subgroup.quotientEquivSigmaZMod {G : Type u} [Group G] (H : Subgroup G) (g : G) :
                                    G H (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G H)) × ZMod (Function.minimalPeriod (fun (x : G H) => g x) (Quotient.out' q))

                                    Partition G ⧸ H into orbits of the action of g : G.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Subgroup.quotientEquivSigmaZMod_symm_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G H)) (k : ZMod (Function.minimalPeriod (fun (x : G H) => g x) (Quotient.out' q))) :
                                      (H.quotientEquivSigmaZMod g).symm q, k = g ^ k.cast Quotient.out' q
                                      theorem Subgroup.quotientEquivSigmaZMod_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G H)) (k : ) :
                                      (H.quotientEquivSigmaZMod g) (g ^ k Quotient.out' q) = q, k
                                      noncomputable def Subgroup.transferFunction {G : Type u} [Group G] (H : Subgroup G) (g : G) :
                                      G HG

                                      The transfer transversal as a function. Given a ⟨g⟩-orbit q₀, g • q₀, ..., g ^ (m - 1) • q₀ in G ⧸ H, an element g ^ k • q₀ is mapped to g ^ k • g₀ for a fixed choice of representative g₀ of q₀.

                                      Equations
                                      Instances For
                                        theorem Subgroup.transferFunction_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G H) :
                                        H.transferFunction g q = g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out' (Quotient.out' ((H.quotientEquivSigmaZMod g) q).fst)
                                        theorem Subgroup.coe_transferFunction {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G H) :
                                        (H.transferFunction g q) = q
                                        def Subgroup.transferSet {G : Type u} [Group G] (H : Subgroup G) (g : G) :
                                        Set G

                                        The transfer transversal as a set. Contains elements of the form g ^ k • g₀ for fixed choices of representatives g₀ of fixed choices of representatives q₀ of ⟨g⟩-orbits in G ⧸ H.

                                        Equations
                                        • H.transferSet g = Set.range (H.transferFunction g)
                                        Instances For
                                          theorem Subgroup.mem_transferSet {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G H) :
                                          H.transferFunction g q H.transferSet g
                                          def Subgroup.transferTransversal {G : Type u} [Group G] (H : Subgroup G) (g : G) :

                                          The transfer transversal. Contains elements of the form g ^ k • g₀ for fixed choices of representatives g₀ of fixed choices of representatives q₀ of ⟨g⟩-orbits in G ⧸ H.

                                          Equations
                                          • H.transferTransversal g = H.transferSet g,
                                          Instances For
                                            theorem Subgroup.transferTransversal_apply {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : G H) :
                                            ((Subgroup.MemLeftTransversals.toEquiv ) q) = H.transferFunction g q
                                            theorem Subgroup.transferTransversal_apply'' {G : Type u} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G H)) (k : ZMod (Function.minimalPeriod (fun (x : G H) => g x) (Quotient.out' q))) :
                                            ((Subgroup.MemLeftTransversals.toEquiv ) (g ^ k.cast Quotient.out' q)) = if k = 0 then g ^ Function.minimalPeriod (fun (x : G H) => g x) (Quotient.out' q) * Quotient.out' (Quotient.out' q) else g ^ k.cast * Quotient.out' (Quotient.out' q)