Documentation

Mathlib.GroupTheory.Index

Index of a Subgroup #

In this file we define the index of a subgroup, and prove several divisibility properties. Several theorems proved in this file are known as Lagrange's theorem.

Main definitions #

Main results #

noncomputable def AddSubgroup.index {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :

The index of a subgroup as a natural number, and returns 0 if the index is infinite.

Equations
Instances For
    noncomputable def Subgroup.index {G : Type u_1} [Group G] (H : Subgroup G) :

    The index of a subgroup as a natural number, and returns 0 if the index is infinite.

    Equations
    Instances For
      noncomputable def AddSubgroup.relindex {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :

      The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.

      Equations
      Instances For
        noncomputable def Subgroup.relindex {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :

        The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.

        Equations
        Instances For
          theorem Subgroup.index_comap_of_surjective {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] {f : G' →* G} (hf : Function.Surjective f) :
          theorem Subgroup.index_comap {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] (f : G' →* G) :
          theorem Subgroup.relindex_comap {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] (f : G' →* G) (K : Subgroup G') :
          theorem Subgroup.index_dvd_of_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
          theorem Subgroup.relindex_mul_relindex {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (L : Subgroup G) (hHK : H K) (hKL : K L) :
          theorem Subgroup.relindex_dvd_of_le_left {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (L : Subgroup G) (hHK : H K) :
          theorem AddSubgroup.index_eq_two_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
          AddSubgroup.index H = 2 ∃ (a : G), ∀ (b : G), Xor' (b + a H) (b H)

          An additive subgroup has index two if and only if there exists a such that for all b, exactly one of b + a and b belong to H.

          theorem Subgroup.index_eq_two_iff {G : Type u_1} [Group G] {H : Subgroup G} :
          Subgroup.index H = 2 ∃ (a : G), ∀ (b : G), Xor' (b * a H) (b H)

          A subgroup has index two if and only if there exists a such that for all b, exactly one of b * a and b belong to H.

          theorem AddSubgroup.add_mem_iff_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : AddSubgroup.index H = 2) {a : G} {b : G} :
          a + b H (a H b H)
          theorem Subgroup.mul_mem_iff_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : Subgroup.index H = 2) {a : G} {b : G} :
          a * b H (a H b H)
          theorem AddSubgroup.add_self_mem_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : AddSubgroup.index H = 2) (a : G) :
          a + a H
          theorem Subgroup.mul_self_mem_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : Subgroup.index H = 2) (a : G) :
          a * a H
          theorem AddSubgroup.two_smul_mem_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : AddSubgroup.index H = 2) (a : G) :
          2 a H
          theorem Subgroup.sq_mem_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : Subgroup.index H = 2) (a : G) :
          a ^ 2 H
          @[simp]
          theorem Subgroup.index_top {G : Type u_1} [Group G] :
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          theorem Subgroup.relindex_self {G : Type u_1} [Group G] (H : Subgroup G) :
          theorem AddSubgroup.index_ker {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) :
          theorem Subgroup.index_ker {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) :
          theorem AddSubgroup.relindex_ker {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (K : AddSubgroup G) :
          theorem Subgroup.relindex_ker {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (K : Subgroup G) :
          @[simp]
          theorem Subgroup.card_mul_index {G : Type u_1} [Group G] (H : Subgroup G) :
          theorem AddSubgroup.nat_card_dvd_of_injective {G : Type u_2} {H : Type u_3} [AddGroup G] [AddGroup H] (f : G →+ H) (hf : Function.Injective f) :
          theorem Subgroup.nat_card_dvd_of_injective {G : Type u_2} {H : Type u_3} [Group G] [Group H] (f : G →* H) (hf : Function.Injective f) :
          theorem AddSubgroup.nat_card_dvd_of_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) (hHK : H K) :
          theorem Subgroup.nat_card_dvd_of_le {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (hHK : H K) :
          theorem Subgroup.nat_card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [Group G] [Group H] (f : G →* H) (hf : Function.Surjective f) :
          theorem Subgroup.card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [Group G] [Group H] [Fintype G] [Fintype H] (f : G →* H) (hf : Function.Surjective f) :
          theorem Subgroup.index_map_dvd {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] {f : G →* G'} (hf : Function.Surjective f) :
          theorem Subgroup.dvd_index_map {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] {f : G →* G'} (hf : MonoidHom.ker f H) :
          theorem Subgroup.index_map_eq {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] {f : G →* G'} (hf1 : Function.Surjective f) (hf2 : MonoidHom.ker f H) :
          theorem Subgroup.relindex_eq_zero_of_le_left {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hHK : H K) (hKL : Subgroup.relindex K L = 0) :
          theorem Subgroup.relindex_eq_zero_of_le_right {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hKL : K L) (hHK : Subgroup.relindex H K = 0) :
          theorem Subgroup.relindex_le_of_le_left {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hHK : H K) (hHL : Subgroup.relindex H L 0) :
          theorem Subgroup.relindex_le_of_le_right {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hKL : K L) (hHL : Subgroup.relindex H L 0) :
          theorem Subgroup.relindex_ne_zero_trans {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hHK : Subgroup.relindex H K 0) (hKL : Subgroup.relindex K L 0) :
          theorem Subgroup.relindex_inf_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hH : Subgroup.relindex H L 0) (hK : Subgroup.relindex K L 0) :
          theorem Subgroup.index_inf_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : Subgroup.index H 0) (hK : Subgroup.index K 0) :
          theorem AddSubgroup.relindex_iInf_ne_zero {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_2} [_hι : Finite ι] {f : ιAddSubgroup G} (hf : ∀ (i : ι), AddSubgroup.relindex (f i) L 0) :
          AddSubgroup.relindex (⨅ (i : ι), f i) L 0
          theorem Subgroup.relindex_iInf_ne_zero {G : Type u_1} [Group G] {L : Subgroup G} {ι : Type u_2} [_hι : Finite ι] {f : ιSubgroup G} (hf : ∀ (i : ι), Subgroup.relindex (f i) L 0) :
          Subgroup.relindex (⨅ (i : ι), f i) L 0
          theorem AddSubgroup.relindex_iInf_le {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_2} [Fintype ι] (f : ιAddSubgroup G) :
          AddSubgroup.relindex (⨅ (i : ι), f i) L Finset.prod Finset.univ fun (i : ι) => AddSubgroup.relindex (f i) L
          abbrev AddSubgroup.relindex_iInf_le.match_1 {G : Type u_2} [AddGroup G] {L : AddSubgroup G} {ι : Type u_1} [Fintype ι] (f : ιAddSubgroup G) (motive : (∃ a ∈ Finset.univ, Nat.card (L AddSubgroup.addSubgroupOf (f a) L) = 0)Prop) :
          ∀ (x : ∃ a ∈ Finset.univ, Nat.card (L AddSubgroup.addSubgroupOf (f a) L) = 0), (∀ (i : ι) (_hi : i Finset.univ) (h : Nat.card (L AddSubgroup.addSubgroupOf (f i) L) = 0), motive (_ : ∃ a ∈ Finset.univ, Nat.card (L AddSubgroup.addSubgroupOf (f a) L) = 0))motive x
          Equations
          • (_ : motive x) = (_ : motive x)
          Instances For
            theorem Subgroup.relindex_iInf_le {G : Type u_1} [Group G] {L : Subgroup G} {ι : Type u_2} [Fintype ι] (f : ιSubgroup G) :
            Subgroup.relindex (⨅ (i : ι), f i) L Finset.prod Finset.univ fun (i : ι) => Subgroup.relindex (f i) L
            theorem AddSubgroup.index_iInf_ne_zero {G : Type u_1} [AddGroup G] {ι : Type u_2} [Finite ι] {f : ιAddSubgroup G} (hf : ∀ (i : ι), AddSubgroup.index (f i) 0) :
            AddSubgroup.index (⨅ (i : ι), f i) 0
            theorem Subgroup.index_iInf_ne_zero {G : Type u_1} [Group G] {ι : Type u_2} [Finite ι] {f : ιSubgroup G} (hf : ∀ (i : ι), Subgroup.index (f i) 0) :
            Subgroup.index (⨅ (i : ι), f i) 0
            theorem AddSubgroup.index_iInf_le {G : Type u_1} [AddGroup G] {ι : Type u_2} [Fintype ι] (f : ιAddSubgroup G) :
            AddSubgroup.index (⨅ (i : ι), f i) Finset.prod Finset.univ fun (i : ι) => AddSubgroup.index (f i)
            theorem Subgroup.index_iInf_le {G : Type u_1} [Group G] {ι : Type u_2} [Fintype ι] (f : ιSubgroup G) :
            Subgroup.index (⨅ (i : ι), f i) Finset.prod Finset.univ fun (i : ι) => Subgroup.index (f i)
            @[simp]
            @[simp]
            theorem Subgroup.index_eq_one {G : Type u_1} [Group G] {H : Subgroup G} :
            @[simp]
            @[simp]
            theorem Subgroup.relindex_eq_one {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
            @[simp]
            theorem AddSubgroup.card_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
            Nat.card H = 1 H =
            @[simp]
            theorem Subgroup.card_eq_one {G : Type u_1} [Group G] {H : Subgroup G} :
            Nat.card H = 1 H =
            theorem Subgroup.index_ne_zero_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [hH : Finite (G H)] :
            noncomputable def AddSubgroup.fintypeOfIndexNeZero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : AddSubgroup.index H 0) :
            Fintype (G H)

            Finite index implies finite quotient.

            Equations
            Instances For
              noncomputable def Subgroup.fintypeOfIndexNeZero {G : Type u_1} [Group G] {H : Subgroup G} (hH : Subgroup.index H 0) :
              Fintype (G H)

              Finite index implies finite quotient.

              Equations
              Instances For
                theorem Subgroup.one_lt_index_of_ne_top {G : Type u_1} [Group G] {H : Subgroup G} [Finite (G H)] (hH : H ) :
                class Subgroup.FiniteIndex {G : Type u_1} [Group G] (H : Subgroup G) :

                Typeclass for finite index subgroups.

                Instances

                  Typeclass for finite index subgroups.

                  Instances

                    A finite index subgroup has finite quotient

                    Equations
                    Instances For
                      noncomputable def Subgroup.fintypeQuotientOfFiniteIndex {G : Type u_1} [Group G] (H : Subgroup G) [Subgroup.FiniteIndex H] :
                      Fintype (G H)

                      A finite index subgroup has finite quotient.

                      Equations
                      Instances For
                        Equations
                        Equations