Mathlib.GroupTheory.Index

Subgroup.index definition

: ℕ

Full source

/-- The index of a subgroup as a natural number. Returns `0` if the index is infinite. -/
@[to_additive "The index of an additive subgroup as a natural number.
Returns 0 if the index is infinite."]
noncomputable def index : ℕ :=
  Nat.card (G ⧸ H)

Index of a subgroup

Informal description

The index of a subgroup $H$ in a group $G$ is defined as the cardinality of the quotient group $G ⧸ H$ (the set of left cosets of $H$ in $G$), considered as a natural number. If the index is infinite, it is defined to be 0.

Subgroup.relindex definition

: ℕ

Full source

/-- If `H` and `K` are subgroups of a group `G`, then `relindex H K : ℕ` is the index
of `H ∩ K` in `K`. The function returns `0` if the index is infinite. -/
@[to_additive "If `H` and `K` are subgroups of an additive group `G`, then `relindex H K : ℕ`
is the index of `H ∩ K` in `K`. The function returns `0` if the index is infinite."]
noncomputable def relindex : ℕ :=
  (H.subgroupOf K).index

Relative index of a subgroup

Informal description

For subgroups $H$ and $K$ of a group $G$, the relative index $\text{relindex}(H, K)$ is the index of $H \cap K$ in $K$, defined as the cardinality of the quotient $K / (H \cap K)$. If this index is infinite, the function returns 0.

Subgroup.index_comap_of_surjective theorem

{f : G' →* G} (hf : Function.Surjective f) : (H.comap f).index = H.index

Full source

@[to_additive]
theorem index_comap_of_surjective {f : G' →* G} (hf : Function.Surjective f) :
    (H.comap f).index = H.index := by
  have key : ∀ x y : G',
      QuotientGroup.leftRelQuotientGroup.leftRel (H.comap f) x y ↔ QuotientGroup.leftRel H (f x) (f y) := by
    simp only [QuotientGroup.leftRel_apply]
    exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
  refine Cardinal.toNat_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)
  · simp_rw [← Quotient.eq''] at key
    refine Quotient.ind' fun x => ?_
    refine Quotient.ind' fun y => ?_
    exact (key x y).mpr
  · refine Quotient.ind' fun x => ?_
    obtain ⟨y, hy⟩ := hf x
    exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

Index Preservation under Surjective Homomorphism Preimage

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G' \to G$ a surjective group homomorphism. Then the index of the preimage subgroup $f^{-1}(H)$ in $G'$ equals the index of $H$ in $G$, i.e., $[G' : f^{-1}(H)] = [G : H]$.

Subgroup.index_comap theorem

(f : G' →* G) : (H.comap f).index = H.relindex f.range

Full source

@[to_additive]
theorem index_comap (f : G' →* G) :
    (H.comap f).index = H.relindex f.range :=
  Eq.trans (congr_arg index (by rfl))
    ((H.subgroupOf f.range).index_comap_of_surjective f.rangeRestrict_surjective)

Index of Preimage Subgroup Equals Relative Index in Homomorphism Range

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G' \to G$ a group homomorphism. Then the index of the preimage subgroup $f^{-1}(H)$ in $G'$ equals the relative index of $H$ in the range of $f$, i.e., $[G' : f^{-1}(H)] = [f(G') : H \cap f(G')]$.

Subgroup.relindex_comap theorem

(f : G' →* G) (K : Subgroup G') : relindex (comap f H) K = relindex H (map f K)

Full source

@[to_additive]
theorem relindex_comap (f : G' →* G) (K : Subgroup G') :
    relindex (comap f H) K = relindex H (map f K) := by
  rw [relindex, subgroupOf, comap_comap, index_comap, ← f.map_range, K.range_subtype]

Relative Index Preservation under Group Homomorphism: $[K : f^{-1}(H) \cap K] = [f(K) : H \cap f(K)]$

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, $K$ a subgroup of $G'$, and $f : G' \to G$ a group homomorphism. Then the relative index of the preimage subgroup $f^{-1}(H)$ in $K$ equals the relative index of $H$ in the image subgroup $f(K)$, i.e., \[ [K : f^{-1}(H) \cap K] = [f(K) : H \cap f(K)]. \]

Subgroup.relindex_mul_index theorem

(h : H ≤ K) : H.relindex K * K.index = H.index

Full source

@[to_additive relindex_mul_index]
theorem relindex_mul_index (h : H ≤ K) : H.relindex K * K.index = H.index :=
  ((mul_comm _ _).trans (Cardinal.toNat_mul _ _).symm).trans
    (congr_arg Cardinal.toNat (Equiv.cardinal_eq (quotientEquivProdOfLE h))).symm

Multiplicativity of Subgroup Indices: $|K : H| \cdot |G : K| = |G : H|$

Informal description

For any subgroups $H \leq K$ of a group $G$, the product of the relative index of $H$ in $K$ and the index of $K$ in $G$ equals the index of $H$ in $G$, i.e., \[ \text{relindex}(H, K) \cdot |G : K| = |G : H|. \]

Subgroup.index_dvd_of_le theorem

(h : H ≤ K) : K.index ∣ H.index

Full source

@[to_additive]
theorem index_dvd_of_le (h : H ≤ K) : K.index ∣ H.index :=
  dvd_of_mul_left_eq (H.relindex K) (relindex_mul_index h)

Divisibility of Subgroup Indices: $|G : K|$ divides $|G : H|$ when $H \leq K$

Informal description

For any subgroups $H \leq K$ of a group $G$, the index of $K$ in $G$ divides the index of $H$ in $G$, i.e., $|G : K|$ divides $|G : H|$.

Subgroup.relindex_dvd_index_of_le theorem

(h : H ≤ K) : H.relindex K ∣ H.index

Full source

@[to_additive]
theorem relindex_dvd_index_of_le (h : H ≤ K) : H.relindex K ∣ H.index :=
  dvd_of_mul_right_eq K.index (relindex_mul_index h)

Divisibility of Subgroup Indices: $|K : H|$ divides $|G : H|$

Informal description

For any subgroups $H \leq K$ of a group $G$, the relative index of $H$ in $K$ divides the index of $H$ in $G$, i.e., $|K : H|$ divides $|G : H|$.

Subgroup.relindex_subgroupOf theorem

(hKL : K ≤ L) : (H.subgroupOf L).relindex (K.subgroupOf L) = H.relindex K

Full source

@[to_additive]
theorem relindex_subgroupOf (hKL : K ≤ L) :
    (H.subgroupOf L).relindex (K.subgroupOf L) = H.relindex K :=
  ((index_comap (H.subgroupOf L) (inclusion hKL)).trans (congr_arg _ (inclusion_range hKL))).symm

Relative Index Preservation Under Subgroup Restriction

Informal description

Let $H$, $K$, and $L$ be subgroups of a group $G$ such that $K \leq L$. Then the relative index of $H \cap L$ in $K \cap L$ equals the relative index of $H$ in $K$, i.e., $$(H \cap L).\text{relindex}\, (K \cap L) = H.\text{relindex}\, K.$$

Subgroup.relindex_mul_relindex theorem

(hHK : H ≤ K) (hKL : K ≤ L) : H.relindex K * K.relindex L = H.relindex L

Full source

@[to_additive relindex_mul_relindex]
theorem relindex_mul_relindex (hHK : H ≤ K) (hKL : K ≤ L) :
    H.relindex K * K.relindex L = H.relindex L := by
  rw [← relindex_subgroupOf hKL]
  exact relindex_mul_index fun x hx => hHK hx

Multiplicativity of Relative Indices in Subgroup Tower: $|K : H| \cdot |L : K| = |L : H|$

Informal description

For subgroups $H \leq K \leq L$ of a group $G$, the product of the relative index of $H$ in $K$ and the relative index of $K$ in $L$ equals the relative index of $H$ in $L$, i.e., \[ |K : H| \cdot |L : K| = |L : H|. \]

Subgroup.inf_relindex_right theorem

: (H ⊓ K).relindex K = H.relindex K

Full source

@[to_additive]
theorem inf_relindex_right : (H ⊓ K).relindex K = H.relindex K := by
  rw [relindex, relindex, inf_subgroupOf_right]

Relative Index of Intersection Equals Relative Index

Informal description

For any subgroups $H$ and $K$ of a group $G$, the relative index of $H \cap K$ in $K$ is equal to the relative index of $H$ in $K$, i.e., $(H \cap K).\text{relindex}\, K = H.\text{relindex}\, K$.

Subgroup.inf_relindex_left theorem

: (H ⊓ K).relindex H = K.relindex H

Full source

@[to_additive]
theorem inf_relindex_left : (H ⊓ K).relindex H = K.relindex H := by
  rw [inf_comm, inf_relindex_right]

Relative Index of Intersection Equals Relative Index (Left Version)

Informal description

For any subgroups $H$ and $K$ of a group $G$, the relative index of $H \cap K$ in $H$ is equal to the relative index of $K$ in $H$, i.e., $(H \cap K).\text{relindex}\, H = K.\text{relindex}\, H$.

Subgroup.relindex_inf_mul_relindex theorem

: H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L

Full source

@[to_additive relindex_inf_mul_relindex]
theorem relindex_inf_mul_relindex : H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L := by
  rw [← inf_relindex_right H (K ⊓ L), ← inf_relindex_right K L, ← inf_relindex_right (H ⊓ K) L,
    inf_assoc, relindex_mul_relindex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]

Relative Index Product Formula for Subgroup Intersection: $|K \cap L : H| \cdot |L : K| = |L : H \cap K|$

Informal description

For any subgroups $H$, $K$, and $L$ of a group $G$, the product of the relative index of $H$ in $K \cap L$ and the relative index of $K$ in $L$ equals the relative index of $H \cap K$ in $L$, i.e., \[ |K \cap L : H| \cdot |L : K| = |L : H \cap K|. \]

Subgroup.relindex_sup_right theorem

[K.Normal] : K.relindex (H ⊔ K) = K.relindex H

Full source

@[to_additive (attr := simp)]
theorem relindex_sup_right [K.Normal] : K.relindex (H ⊔ K) = K.relindex H :=
  Nat.card_congr (QuotientGroup.quotientInfEquivProdNormalQuotient H K).toEquiv.symm

Relative Index Equality for Normal Subgroup and Join: $|K : H \sqcup K| = |K : H|$

Informal description

For any normal subgroup $K$ of a group $G$ and any subgroup $H$ of $G$, the relative index of $K$ in the join $H \sqcup K$ equals the relative index of $K$ in $H$, i.e., \[ K.\text{relindex}\, (H \sqcup K) = K.\text{relindex}\, H. \]

Subgroup.relindex_sup_left theorem

[K.Normal] : K.relindex (K ⊔ H) = K.relindex H

Full source

@[to_additive (attr := simp)]
theorem relindex_sup_left [K.Normal] : K.relindex (K ⊔ H) = K.relindex H := by
  rw [sup_comm, relindex_sup_right]

Relative Index Equality for Normal Subgroup and Join (Left Version): $|K : K \sqcup H| = |K : H|$

Informal description

For any normal subgroup $K$ of a group $G$ and any subgroup $H$ of $G$, the relative index of $K$ in the join $K \sqcup H$ equals the relative index of $K$ in $H$, i.e., \[ K.\text{relindex}\, (K \sqcup H) = K.\text{relindex}\, H. \]

Subgroup.relindex_dvd_index_of_normal theorem

[H.Normal] : H.relindex K ∣ H.index

Full source

@[to_additive]
theorem relindex_dvd_index_of_normal [H.Normal] : H.relindex K ∣ H.index :=
  relindex_sup_right K H ▸ relindex_dvd_index_of_le le_sup_right

Divisibility of Relative Index by Index for Normal Subgroups: $|K : H|$ divides $|G : H|$

Informal description

For any normal subgroup $H$ of a group $G$ and any subgroup $K$ of $G$, the relative index of $H$ in $K$ divides the index of $H$ in $G$, i.e., $|K : H|$ divides $|G : H|$.

Subgroup.index_eq_two_iff theorem

: H.index = 2 ↔ ∃ a, ∀ b, Xor' (b * a ∈ H) (b ∈ H)

Full source

/-- 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`. -/
@[to_additive "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 index_eq_two_iff : H.index = 2 ↔ ∃ a, ∀ b, Xor' (b * a ∈ H) (b ∈ H) := by
  simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff,
    QuotientGroup.exists_mk, QuotientGroup.forall_mk, Ne, QuotientGroup.eq, mul_one,
    xor_iff_iff_not]
  refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
  · exact ha.1 ((mul_mem_cancel_left hb).1 hba)
  · exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
  · rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]
    exact one_mem _
  · rwa [ha, inv_mem_iff (x := b)]

Characterization of Subgroups of Index Two via Coset Condition

Informal description

A subgroup $H$ of a group $G$ has index $2$ if and only if there exists an element $a \in G$ such that for every element $b \in G$, exactly one of the following holds: either $b \cdot a \in H$ or $b \in H$ (but not both).

Subgroup.mul_mem_iff_of_index_two theorem

(h : H.index = 2) {a b : G} : a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Full source

@[to_additive]
theorem mul_mem_iff_of_index_two (h : H.index = 2) {a b : G} : a * b ∈ Ha * b ∈ H ↔ (a ∈ H ↔ b ∈ H) := by
  by_cases ha : a ∈ H; · simp only [ha, true_iff, mul_mem_cancel_left ha]
  by_cases hb : b ∈ H; · simp only [hb, iff_true, mul_mem_cancel_right hb]
  simp only [ha, hb, iff_true]
  rcases index_eq_two_iff.1 h with ⟨c, hc⟩
  refine (hc _).or.resolve_left ?_
  rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]

Product Membership Criterion for Index Two Subgroups: $a \cdot b \in H \leftrightarrow (a \in H \leftrightarrow b \in H)$

Informal description

Let $H$ be a subgroup of a group $G$ with index $2$. Then for any elements $a, b \in G$, the product $a \cdot b$ belongs to $H$ if and only if $a$ and $b$ are either both in $H$ or both not in $H$.

Subgroup.mul_self_mem_of_index_two theorem

(h : H.index = 2) (a : G) : a * a ∈ H

Full source

@[to_additive]
theorem mul_self_mem_of_index_two (h : H.index = 2) (a : G) : a * a ∈ H := by
  rw [mul_mem_iff_of_index_two h]

Square Elements Belong to Index Two Subgroups: $a^2 \in H$ for $[G:H]=2$

Informal description

Let $H$ be a subgroup of a group $G$ with index $2$. Then for any element $a \in G$, the product $a \cdot a$ (i.e., $a^2$) belongs to $H$.

Subgroup.sq_mem_of_index_two theorem

(h : H.index = 2) (a : G) : a ^ 2 ∈ H

Full source

@[to_additive two_smul_mem_of_index_two]
theorem sq_mem_of_index_two (h : H.index = 2) (a : G) : a ^ 2 ∈ H :=
  (pow_two a).symm ▸ mul_self_mem_of_index_two h a

Squares in Subgroups of Index Two: $a^2 \in H$ when $[G:H] = 2$

Informal description

Let $H$ be a subgroup of a group $G$ with index $2$. Then for any element $a \in G$, the square $a^2$ belongs to $H$.

Subgroup.index_top theorem

: (⊤ : Subgroup G).index = 1

Full source

@[to_additive (attr := simp)]
theorem index_top : (⊤ : Subgroup G).index = 1 :=
  Nat.card_eq_one_iff_unique.mpr ⟨QuotientGroup.subsingleton_quotient_top, ⟨1⟩⟩

Index of Trivial Subgroup is One: $[\top : G] = 1$

Informal description

The index of the trivial subgroup $\top$ in a group $G$ is equal to $1$.

Subgroup.index_bot theorem

: (⊥ : Subgroup G).index = Nat.card G

Full source

@[to_additive (attr := simp)]
theorem index_bot : (⊥ : Subgroup G).index = Nat.card G :=
  Cardinal.toNat_congr QuotientGroup.quotientBot.toEquiv

Index of Trivial Subgroup Equals Group Cardinality: $[\{\text{id}_G\} : G] = |G|$

Informal description

The index of the trivial subgroup $\{\text{id}_G\}$ in a group $G$ is equal to the cardinality of $G$ as a natural number, i.e., $[\{\text{id}_G\} : G] = |G|$.

Subgroup.relindex_top_left theorem

: (⊤ : Subgroup G).relindex H = 1

Full source

@[to_additive (attr := simp)]
theorem relindex_top_left : (⊤ : Subgroup G).relindex H = 1 :=
  index_top

Relative Index of Trivial Subgroup is One: $\text{relindex}(\top, H) = 1$

Informal description

For any subgroup $H$ of a group $G$, the relative index of the trivial subgroup $\top$ in $H$ is equal to $1$, i.e., $\text{relindex}(\top, H) = 1$.

Subgroup.relindex_top_right theorem

: H.relindex ⊤ = H.index

Full source

@[to_additive (attr := simp)]
theorem relindex_top_right : H.relindex ⊤ = H.index := by
  rw [← relindex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]

Relative Index of Subgroup in Trivial Subgroup Equals Its Index: $H.\text{relindex}(\top) = H.\text{index}$

Informal description

For any subgroup $H$ of a group $G$, the relative index of $H$ in the trivial subgroup $\top$ is equal to the index of $H$ in $G$, i.e., $H.\text{relindex}(\top) = H.\text{index}$.

Subgroup.relindex_bot_left theorem

: (⊥ : Subgroup G).relindex H = Nat.card H

Full source

@[to_additive (attr := simp)]
theorem relindex_bot_left : (⊥ : Subgroup G).relindex H = Nat.card H := by
  rw [relindex, bot_subgroupOf, index_bot]

Relative Index of Trivial Subgroup in $H$ Equals $|H|$

Informal description

For any subgroup $H$ of a group $G$, the relative index of the trivial subgroup $\{\text{id}_G\}$ in $H$ is equal to the cardinality of $H$ as a natural number, i.e., $\text{relindex}(\{\text{id}_G\}, H) = |H|$.

Subgroup.relindex_bot_right theorem

: H.relindex ⊥ = 1

Full source

@[to_additive (attr := simp)]
theorem relindex_bot_right : H.relindex ⊥ = 1 := by rw [relindex, subgroupOf_bot_eq_top, index_top]

Relative Index of Subgroup in Trivial Subgroup is One

Informal description

For any subgroup $H$ of a group $G$, the relative index of $H$ in the trivial subgroup $\bot$ is equal to $1$, i.e., $\text{relindex}(H, \bot) = 1$.

Subgroup.relindex_self theorem

: H.relindex H = 1

Full source

@[to_additive (attr := simp)]
theorem relindex_self : H.relindex H = 1 := by rw [relindex, subgroupOf_self, index_top]

Relative Index of Subgroup in Itself is One

Informal description

For any subgroup $H$ of a group $G$, the relative index of $H$ in itself is equal to $1$, i.e., $\text{relindex}(H, H) = 1$.

Subgroup.index_ker theorem

(f : G →* G') : f.ker.index = Nat.card f.range

Full source

@[to_additive]
theorem index_ker (f : G →* G') : f.ker.index = Nat.card f.range := by
  rw [← MonoidHom.comap_bot, index_comap, relindex_bot_left]

Index of Kernel Equals Cardinality of Range

Informal description

For any group homomorphism $f \colon G \to G'$, the index of the kernel $\ker f$ in $G$ equals the cardinality of the range $f(G)$, i.e., $[G : \ker f] = |f(G)|$.

Subgroup.relindex_ker theorem

(f : G →* G') : f.ker.relindex K = Nat.card (K.map f)

Full source

@[to_additive]
theorem relindex_ker (f : G →* G') : f.ker.relindex K = Nat.card (K.map f) := by
  rw [← MonoidHom.comap_bot, relindex_comap, relindex_bot_left]

Relative Index of Kernel Equals Cardinality of Image Subgroup

Informal description

For any group homomorphism $f \colon G \to G'$ and any subgroup $K$ of $G$, the relative index of the kernel of $f$ in $K$ is equal to the cardinality of the image of $K$ under $f$, i.e., \[ [K : \ker f \cap K] = |f(K)|. \]

Subgroup.card_mul_index theorem

: Nat.card H * H.index = Nat.card G

Full source

@[to_additive (attr := simp) card_mul_index]
theorem card_mul_index : Nat.card H * H.index = Nat.card G := by
  rw [← relindex_bot_left, ← index_bot]
  exact relindex_mul_index bot_le

Lagrange's Theorem: $|H| \cdot [G : H] = |G|$

Informal description

For any subgroup $H$ of a group $G$, the product of the cardinality of $H$ and the index of $H$ in $G$ equals the cardinality of $G$, i.e., \[ |H| \cdot [G : H] = |G|. \]

Subgroup.card_dvd_of_surjective theorem

(f : G →* G') (hf : Function.Surjective f) : Nat.card G' ∣ Nat.card G

Full source

@[to_additive]
theorem card_dvd_of_surjective (f : G →* G') (hf : Function.Surjective f) :
    Nat.cardNat.card G' ∣ Nat.card G := by
  rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]
  exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

Cardinality Divisibility under Surjective Group Homomorphism

Informal description

For any surjective group homomorphism $f \colon G \to G'$, the cardinality of $G'$ divides the cardinality of $G$, i.e., $|G'| \mid |G|$.

Subgroup.card_range_dvd theorem

(f : G →* G') : Nat.card f.range ∣ Nat.card G

Full source

@[to_additive]
theorem card_range_dvd (f : G →* G') : Nat.cardNat.card f.range ∣ Nat.card G :=
  card_dvd_of_surjective f.rangeRestrict f.rangeRestrict_surjective

Cardinality of Range Divides Cardinality of Domain

Informal description

For any group homomorphism $f \colon G \to G'$, the cardinality of the range of $f$ divides the cardinality of $G$, i.e., $|f(G)| \mid |G|$.

Subgroup.card_map_dvd theorem

(f : G →* G') : Nat.card (H.map f) ∣ Nat.card H

Full source

@[to_additive]
theorem card_map_dvd (f : G →* G') : Nat.cardNat.card (H.map f) ∣ Nat.card H :=
  card_dvd_of_surjective (f.subgroupMap H) (f.subgroupMap_surjective H)

Cardinality Divisibility of Image Subgroup: $|f(H)| \mid |H|$

Informal description

For any group homomorphism $f \colon G \to G'$ and subgroup $H$ of $G$, the cardinality of the image subgroup $f(H)$ divides the cardinality of $H$, i.e., $|f(H)| \mid |H|$.

Subgroup.index_map theorem

(f : G →* G') : (H.map f).index = (H ⊔ f.ker).index * f.range.index

Full source

@[to_additive]
theorem index_map (f : G →* G') :
    (H.map f).index = (H ⊔ f.ker).index * f.range.index := by
  rw [← comap_map_eq, index_comap, relindex_mul_index (H.map_le_range f)]

Index of Image Subgroup Equals Product of Indices of Join and Range

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G \to G'$ a group homomorphism. Then the index of the image subgroup $f(H)$ in $G'$ equals the product of the index of $H \sqcup \ker f$ in $G$ and the index of the range of $f$ in $G'$, i.e., \[ [G' : f(H)] = [G : H \sqcup \ker f] \cdot [G' : f(G)]. \]

Subgroup.index_map_dvd theorem

{f : G →* G'} (hf : Function.Surjective f) : (H.map f).index ∣ H.index

Full source

@[to_additive]
theorem index_map_dvd {f : G →* G'} (hf : Function.Surjective f) :
    (H.map f).index ∣ H.index := by
  rw [index_map, f.range_eq_top_of_surjective hf, index_top, mul_one]
  exact index_dvd_of_le le_sup_left

Divisibility of Subgroup Indices under Surjective Homomorphism: $[G' : f(H)] \mid [G : H]$

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G \to G'$ a surjective group homomorphism. Then the index of the image subgroup $f(H)$ in $G'$ divides the index of $H$ in $G$, i.e., $[G' : f(H)] \mid [G : H]$.

Subgroup.dvd_index_map theorem

{f : G →* G'} (hf : f.ker ≤ H) : H.index ∣ (H.map f).index

Full source

@[to_additive]
theorem dvd_index_map {f : G →* G'} (hf : f.ker ≤ H) :
    H.index ∣ (H.map f).index := by
  rw [index_map, sup_of_le_left hf]
  apply dvd_mul_right

Divisibility of Subgroup Indices under Homomorphism with Kernel Condition

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G \to G'$ a group homomorphism. If the kernel of $f$ is contained in $H$, then the index of $H$ in $G$ divides the index of the image subgroup $f(H)$ in $G'$, i.e., \[ [G : H] \mid [G' : f(H)]. \]

Subgroup.index_map_eq theorem

(hf1 : Surjective f) (hf2 : f.ker ≤ H) : (H.map f).index = H.index

Full source

@[to_additive]
theorem index_map_eq (hf1 : Surjective f) (hf2 : f.ker ≤ H) : (H.map f).index = H.index :=
  Nat.dvd_antisymm (H.index_map_dvd hf1) (H.dvd_index_map hf2)

Index Preservation under Surjective Homomorphism with Kernel Condition: $[G' : f(H)] = [G : H]$

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G \to G'$ a group homomorphism. If $f$ is surjective and the kernel of $f$ is contained in $H$, then the index of the image subgroup $f(H)$ in $G'$ is equal to the index of $H$ in $G$, i.e., \[ [G' : f(H)] = [G : H]. \]

Subgroup.index_map_of_bijective theorem

(hf : Bijective f) (H : Subgroup G) : (H.map f).index = H.index

Full source

@[to_additive]
lemma index_map_of_bijective (hf : Bijective f) (H : Subgroup G) : (H.map f).index = H.index :=
  index_map_eq _ hf.2 (by rw [f.ker_eq_bot_iff.2 hf.1]; exact bot_le)

Index Preservation under Bijective Homomorphism: $[G' : f(H)] = [G : H]$

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G \to G'$ a bijective group homomorphism. Then the index of the image subgroup $f(H)$ in $G'$ is equal to the index of $H$ in $G$, i.e., \[ [G' : f(H)] = [G : H]. \]

Subgroup.index_map_of_injective theorem

{f : G →* G'} (hf : Function.Injective f) : (H.map f).index = H.index * f.range.index

Full source

@[to_additive]
theorem index_map_of_injective {f : G →* G'} (hf : Function.Injective f) :
    (H.map f).index = H.index * f.range.index := by
  rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]

Index of Image Subgroup under Injective Homomorphism Equals Product of Indices

Informal description

Let $G$ and $G'$ be groups, $H$ a subgroup of $G$, and $f : G \to G'$ an injective group homomorphism. Then the index of the image subgroup $f(H)$ in $G'$ is equal to the product of the index of $H$ in $G$ and the index of the range of $f$ in $G'$, i.e., \[ [G' : f(H)] = [G : H] \cdot [G' : f(G)]. \]

Subgroup.index_map_subtype theorem

{H : Subgroup G} (K : Subgroup H) : (K.map H.subtype).index = K.index * H.index

Full source

@[to_additive]
theorem index_map_subtype {H : Subgroup G} (K : Subgroup H) :
    (K.map H.subtype).index = K.index * H.index := by
  rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]

Index of Subgroup Image under Inclusion Equals Product of Indices

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. For any subgroup $K$ of $H$, the index of the image of $K$ under the inclusion homomorphism $H \hookrightarrow G$ in $G$ is equal to the product of the index of $K$ in $H$ and the index of $H$ in $G$, i.e., \[ [G : K \hookrightarrow G] = [H : K] \cdot [G : H]. \]

Subgroup.index_eq_card theorem

: H.index = Nat.card (G ⧸ H)

Full source

@[to_additive]
theorem index_eq_card : H.index = Nat.card (G ⧸ H) :=
  rfl

Index of Subgroup Equals Cardinality of Quotient Group

Informal description

The index of a subgroup $H$ in a group $G$ is equal to the cardinality of the quotient group $G/H$, i.e., $[G : H] = |G/H|$.

Subgroup.index_mul_card theorem

: H.index * Nat.card H = Nat.card G

Full source

@[to_additive index_mul_card]
theorem index_mul_card : H.index * Nat.card H = Nat.card G := by
  rw [mul_comm, card_mul_index]

Lagrange's Theorem: $[G : H] \cdot |H| = |G|$

Informal description

For any subgroup $H$ of a group $G$, the product of the index of $H$ in $G$ and the cardinality of $H$ equals the cardinality of $G$, i.e., \[ [G : H] \cdot |H| = |G|. \]

Subgroup.index_dvd_card theorem

: H.index ∣ Nat.card G

Full source

@[to_additive]
theorem index_dvd_card : H.index ∣ Nat.card G :=
  ⟨Nat.card H, H.index_mul_card.symm⟩

Index Divisor Theorem: $[G : H]$ divides $|G|$

Informal description

For any subgroup $H$ of a group $G$, the index of $H$ in $G$ divides the cardinality of $G$, i.e., $[G : H] \mid |G|$.

Subgroup.relindex_dvd_card theorem

: H.relindex K ∣ Nat.card K

Full source

@[to_additive]
theorem relindex_dvd_card : H.relindex K ∣ Nat.card K :=
  (H.subgroupOf K).index_dvd_card

Relative Index Divisor Theorem: $\text{relindex}(H, K) \mid |K|$

Informal description

For any subgroups $H$ and $K$ of a group $G$, the relative index of $H$ in $K$ divides the cardinality of $K$, i.e., $\text{relindex}(H, K) \mid |K|$.

Subgroup.relindex_eq_zero_of_le_left theorem

(hHK : H ≤ K) (hKL : K.relindex L = 0) : H.relindex L = 0

Full source

@[to_additive]
theorem relindex_eq_zero_of_le_left (hHK : H ≤ K) (hKL : K.relindex L = 0) : H.relindex L = 0 :=
  eq_zero_of_zero_dvd (hKL ▸ relindex_dvd_of_le_left L hHK)

Vanishing Relative Index Under Subgroup Inclusion

Informal description

For subgroups $H$, $K$, and $L$ of a group $G$, if $H \leq K$ and the relative index of $K$ in $L$ is zero, then the relative index of $H$ in $L$ is also zero.

Subgroup.relindex_eq_zero_of_le_right theorem

(hKL : K ≤ L) (hHK : H.relindex K = 0) : H.relindex L = 0

Full source

@[to_additive]
theorem relindex_eq_zero_of_le_right (hKL : K ≤ L) (hHK : H.relindex K = 0) : H.relindex L = 0 :=
  Finite.card_eq_zero_of_embedding (quotientSubgroupOfEmbeddingOfLE H hKL) hHK

Vanishing Relative Index Under Subgroup Inclusion

Informal description

For subgroups $H$, $K$, and $L$ of a group $G$, if $K$ is a subgroup of $L$ and the relative index of $H$ in $K$ is zero, then the relative index of $H$ in $L$ is also zero.

Subgroup.index_eq_zero_of_relindex_eq_zero theorem

(h : H.relindex K = 0) : H.index = 0

Full source

@[to_additive]
theorem index_eq_zero_of_relindex_eq_zero (h : H.relindex K = 0) : H.index = 0 :=
  H.relindex_top_right.symm.trans (relindex_eq_zero_of_le_right le_top h)

Vanishing Index from Vanishing Relative Index

Informal description

For any subgroups $H$ and $K$ of a group $G$, if the relative index of $H$ in $K$ is zero, then the index of $H$ in $G$ is also zero.

Subgroup.relindex_le_of_le_left theorem

(hHK : H ≤ K) (hHL : H.relindex L ≠ 0) : K.relindex L ≤ H.relindex L

Full source

@[to_additive]
theorem relindex_le_of_le_left (hHK : H ≤ K) (hHL : H.relindex L ≠ 0) :
    K.relindex L ≤ H.relindex L :=
  Nat.le_of_dvd (Nat.pos_of_ne_zero hHL) (relindex_dvd_of_le_left L hHK)

Monotonicity of Relative Index under Left Subgroup Inclusion

Informal description

For subgroups $H$, $K$, and $L$ of a group $G$, if $H \leq K$ and the relative index of $H$ in $L$ is nonzero, then the relative index of $K$ in $L$ is less than or equal to the relative index of $H$ in $L$, i.e., $\text{relindex}(K, L) \leq \text{relindex}(H, L)$.

Subgroup.relindex_le_of_le_right theorem

(hKL : K ≤ L) (hHL : H.relindex L ≠ 0) : H.relindex K ≤ H.relindex L

Full source

@[to_additive]
theorem relindex_le_of_le_right (hKL : K ≤ L) (hHL : H.relindex L ≠ 0) :
    H.relindex K ≤ H.relindex L :=
  Finite.card_le_of_embedding' (quotientSubgroupOfEmbeddingOfLE H hKL) fun h => (hHL h).elim

Monotonicity of Relative Index under Subgroup Inclusion

Informal description

Let $H$, $K$, and $L$ be subgroups of a group $G$ such that $K \leq L$ and the relative index of $H$ in $L$ is nonzero. Then the relative index of $H$ in $K$ is less than or equal to the relative index of $H$ in $L$, i.e., $\text{relindex}(H, K) \leq \text{relindex}(H, L)$.

Subgroup.relindex_ne_zero_trans theorem

(hHK : H.relindex K ≠ 0) (hKL : K.relindex L ≠ 0) : H.relindex L ≠ 0

Full source

@[to_additive]
theorem relindex_ne_zero_trans (hHK : H.relindex K ≠ 0) (hKL : K.relindex L ≠ 0) :
    H.relindex L ≠ 0 := fun h =>
  mul_ne_zero (mt (relindex_eq_zero_of_le_right (show K ⊓ L ≤ K from inf_le_left)) hHK) hKL
    ((relindex_inf_mul_relindex H K L).trans (relindex_eq_zero_of_le_left inf_le_left h))

Nonzero Relative Index Transitivity: $|K : H| \neq 0$ and $|L : K| \neq 0$ implies $|L : H| \neq 0$

Informal description

For subgroups $H$, $K$, and $L$ of a group $G$, if the relative index of $H$ in $K$ is nonzero and the relative index of $K$ in $L$ is nonzero, then the relative index of $H$ in $L$ is also nonzero.

Subgroup.relindex_inf_ne_zero theorem

(hH : H.relindex L ≠ 0) (hK : K.relindex L ≠ 0) : (H ⊓ K).relindex L ≠ 0

Full source

@[to_additive]
theorem relindex_inf_ne_zero (hH : H.relindex L ≠ 0) (hK : K.relindex L ≠ 0) :
    (H ⊓ K).relindex L ≠ 0 := by
  replace hH : H.relindex (K ⊓ L) ≠ 0 := mt (relindex_eq_zero_of_le_right inf_le_right) hH
  rw [← inf_relindex_right] at hH hK ⊢
  rw [inf_assoc]
  exact relindex_ne_zero_trans hH hK

Nonzero Relative Index of Intersection: $|L : H \cap K| \neq 0$ when $|L : H| \neq 0$ and $|L : K| \neq 0$

Informal description

For subgroups $H$, $K$, and $L$ of a group $G$, if the relative indices of $H$ in $L$ and $K$ in $L$ are both nonzero, then the relative index of $H \cap K$ in $L$ is also nonzero.

Subgroup.index_inf_ne_zero theorem

(hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0

Full source

@[to_additive]
theorem index_inf_ne_zero (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0 := by
  rw [← relindex_top_right] at hH hK ⊢
  exact relindex_inf_ne_zero hH hK

Nonzero Index of Subgroup Intersection: $|G : H \cap K| \neq 0$ when $|G : H| \neq 0$ and $|G : K| \neq 0$

Informal description

For any subgroups $H$ and $K$ of a group $G$, if the indices of $H$ and $K$ in $G$ are both nonzero, then the index of their intersection $H \cap K$ in $G$ is also nonzero.

Subgroup.relindex_inf_le theorem

: (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

Full source

@[to_additive]
theorem relindex_inf_le : (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L := by
  by_cases h : H.relindex L = 0
  · exact (le_of_eq (relindex_eq_zero_of_le_left inf_le_left h)).trans (zero_le _)
  rw [← inf_relindex_right, inf_assoc, ← relindex_mul_relindex _ _ L inf_le_right inf_le_right,
    inf_relindex_right, inf_relindex_right]
  exact mul_le_mul_right' (relindex_le_of_le_right inf_le_right h) (K.relindex L)

Relative Index Bound for Subgroup Intersection: $|L : H \cap K| \leq |L : H| \cdot |L : K|$

Informal description

For any subgroups $H$, $K$, and $L$ of a group $G$, the relative index of $H \cap K$ in $L$ is bounded by the product of the relative indices of $H$ in $L$ and $K$ in $L$, i.e., \[ |L : H \cap K| \leq |L : H| \cdot |L : K|. \]

Subgroup.index_inf_le theorem

: (H ⊓ K).index ≤ H.index * K.index

Full source

@[to_additive]
theorem index_inf_le : (H ⊓ K).index ≤ H.index * K.index := by
  simp_rw [← relindex_top_right, relindex_inf_le]

Index Bound for Subgroup Intersection: $(H \cap K).\text{index} \leq H.\text{index} \cdot K.\text{index}$

Informal description

For any subgroups $H$ and $K$ of a group $G$, the index of their intersection satisfies the inequality $$(H \cap K).\text{index} \leq H.\text{index} \cdot K.\text{index}.$$ Here, $\text{index}$ denotes the index of a subgroup in $G$, defined as the cardinality of the quotient group $G/H$ (or 0 if infinite).

Subgroup.relindex_iInf_ne_zero theorem

 {ι : Type*} [_hι : Finite ι] {f : ι → Subgroup G} (hf : ∀ i, (f i).relindex L ≠ 0) : (⨅ i, f i).relindex L ≠ 0

Full source

@[to_additive]
theorem relindex_iInf_ne_zero {ι : Type*} [_hι : Finite ι] {f : ι → Subgroup G}
    (hf : ∀ i, (f i).relindex L ≠ 0) : (⨅ i, f i).relindex L ≠ 0 :=
  haveI := Fintype.ofFinite ι
  (Finset.prod_ne_zero_iff.mpr fun i _hi => hf i) ∘
    Nat.card_pi.symm.trans ∘
      Finite.card_eq_zero_of_embedding (quotientiInfSubgroupOfEmbedding f L)

Nonzero Relative Index of Finite Intersection of Subgroups

Informal description

Let $G$ be a group, $L$ a subgroup of $G$, and $\iota$ a finite type. Given a family of subgroups $f : \iota \to \text{Subgroup } G$ such that for each $i \in \iota$, the relative index of $f(i)$ with respect to $L$ is nonzero, then the relative index of the intersection $\bigcap_{i \in \iota} f(i)$ with respect to $L$ is also nonzero.

Subgroup.relindex_iInf_le theorem

{ι : Type*} [Fintype ι] (f : ι → Subgroup G) : (⨅ i, f i).relindex L ≤ ∏ i, (f i).relindex L

Full source

@[to_additive]
theorem relindex_iInf_le {ι : Type*} [Fintype ι] (f : ι → Subgroup G) :
    (⨅ i, f i).relindex L ≤ ∏ i, (f i).relindex L :=
  le_of_le_of_eq
    (Finite.card_le_of_embedding' (quotientiInfSubgroupOfEmbedding f L) fun h =>
      let ⟨i, _hi, h⟩ := Finset.prod_eq_zero_iff.mp (Nat.card_pi.symm.trans h)
      relindex_eq_zero_of_le_left (iInf_le f i) h)
    Nat.card_pi

Relative Index Inequality for Finite Intersection of Subgroups: $\text{relindex}(\bigcap_i H_i, L) \leq \prod_i \text{relindex}(H_i, L)$

Informal description

Let $G$ be a group, $L$ a subgroup of $G$, and $\{H_i\}_{i \in \iota}$ a finite family of subgroups of $G$ indexed by a finite set $\iota$. Then the relative index of the intersection $\bigcap_{i \in \iota} H_i$ with respect to $L$ satisfies the inequality \[ \text{relindex}\left(\bigcap_{i \in \iota} H_i, L\right) \leq \prod_{i \in \iota} \text{relindex}(H_i, L), \] where $\text{relindex}(H, K)$ denotes the index of $H \cap K$ in $K$ (or 0 if infinite).

Subgroup.index_iInf_ne_zero theorem

{ι : Type*} [Finite ι] {f : ι → Subgroup G} (hf : ∀ i, (f i).index ≠ 0) : (⨅ i, f i).index ≠ 0

Full source

@[to_additive]
theorem index_iInf_ne_zero {ι : Type*} [Finite ι] {f : ι → Subgroup G}
    (hf : ∀ i, (f i).index ≠ 0) : (⨅ i, f i).index ≠ 0 := by
  simp_rw [← relindex_top_right] at hf ⊢
  exact relindex_iInf_ne_zero hf

Nonzero Index of Finite Intersection of Subgroups with Nonzero Indices

Informal description

Let $G$ be a group and $\{H_i\}_{i \in \iota}$ be a finite family of subgroups of $G$ indexed by a finite type $\iota$. If for each $i \in \iota$, the index of $H_i$ in $G$ is nonzero, then the index of the intersection $\bigcap_{i \in \iota} H_i$ in $G$ is also nonzero.

Subgroup.index_iInf_le theorem

{ι : Type*} [Fintype ι] (f : ι → Subgroup G) : (⨅ i, f i).index ≤ ∏ i, (f i).index

Full source

@[to_additive]
theorem index_iInf_le {ι : Type*} [Fintype ι] (f : ι → Subgroup G) :
    (⨅ i, f i).index ≤ ∏ i, (f i).index := by simp_rw [← relindex_top_right, relindex_iInf_le]

Inequality for Index of Intersection of Subgroups

Informal description

Let $G$ be a group and $\{H_i\}_{i \in \iota}$ be a finite family of subgroups of $G$ indexed by a finite type $\iota$. Then the index of the infimum (intersection) of all $H_i$ in $G$ is less than or equal to the product of the indices of each $H_i$ in $G$. In other words, \[ \left(\bigcap_{i \in \iota} H_i\right).\text{index} \leq \prod_{i \in \iota} (H_i.\text{index}). \]

Subgroup.index_eq_one theorem

: H.index = 1 ↔ H = ⊤

Full source

@[to_additive (attr := simp) index_eq_one]
theorem index_eq_one : H.index = 1 ↔ H = ⊤ :=
  ⟨fun h =>
    QuotientGroup.subgroup_eq_top_of_subsingleton H (Nat.card_eq_one_iff_unique.mp h).1,
    fun h => (congr_arg index h).trans index_top⟩

Index-One Subgroup Characterization: $[G:H] = 1 \leftrightarrow H = G$

Informal description

For a subgroup $H$ of a group $G$, the index of $H$ in $G$ is equal to $1$ if and only if $H$ is equal to the entire group $G$ (i.e., $H = \top$).

Subgroup.relindex_eq_one theorem

: H.relindex K = 1 ↔ K ≤ H

Full source

@[to_additive (attr := simp) relindex_eq_one]
theorem relindex_eq_one : H.relindex K = 1 ↔ K ≤ H :=
  index_eq_one.trans subgroupOf_eq_top

Relative Index-One Characterization: $[K : H \cap K] = 1 \leftrightarrow K \subseteq H$

Informal description

For subgroups $H$ and $K$ of a group $G$, the relative index of $H$ in $K$ is equal to $1$ if and only if $K$ is a subgroup of $H$, i.e., $[K : H \cap K] = 1 \leftrightarrow K \leq H$.

Subgroup.card_eq_one theorem

: Nat.card H = 1 ↔ H = ⊥

Full source

@[to_additive (attr := simp) card_eq_one]
theorem card_eq_one : Nat.cardNat.card H = 1 ↔ H = ⊥ :=
  H.relindex_bot_left ▸ relindex_eq_one.trans le_bot_iff

Trivial Subgroup Characterization: $|H| = 1 \leftrightarrow H = \{\text{id}_G\}$

Informal description

For a subgroup $H$ of a group $G$, the cardinality of $H$ is equal to $1$ if and only if $H$ is the trivial subgroup $\{\text{id}_G\}$.

Subgroup.inf_eq_bot_of_coprime theorem

(h : Nat.Coprime (Nat.card H) (Nat.card K)) : H ⊓ K = ⊥

Full source

@[to_additive]
lemma inf_eq_bot_of_coprime (h : Nat.Coprime (Nat.card H) (Nat.card K)) : H ⊓ K = ⊥ :=
  card_eq_one.1 <| Nat.eq_one_of_dvd_coprimes h
    (card_dvd_of_le inf_le_left) (card_dvd_of_le inf_le_right)

Trivial Intersection of Coprime Order Subgroups: $H \cap K = \{\text{id}_G\}$ when $\gcd(|H|, |K|) = 1$

Informal description

For any two subgroups $H$ and $K$ of a group $G$, if the orders of $H$ and $K$ are coprime (i.e., $\gcd(|H|, |K|) = 1$), then their intersection is the trivial subgroup $\{\text{id}_G\}$.

Subgroup.index_ne_zero_of_finite theorem

[hH : Finite (G ⧸ H)] : H.index ≠ 0

Full source

@[to_additive]
theorem index_ne_zero_of_finite [hH : Finite (G ⧸ H)] : H.index ≠ 0 := by
  cases nonempty_fintype (G ⧸ H)
  rw [index_eq_card]
  exact Nat.card_pos.ne'

Nonzero Index of Finite Quotient Group

Informal description

For any subgroup $H$ of a group $G$, if the quotient group $G/H$ is finite, then the index $[G : H]$ is nonzero.

Subgroup.fintypeOfIndexNeZero definition

(hH : H.index ≠ 0) : Fintype (G ⧸ H)

Full source

/-- Finite index implies finite quotient. -/
@[to_additive "Finite index implies finite quotient."]
noncomputable def fintypeOfIndexNeZero (hH : H.index ≠ 0) : Fintype (G ⧸ H) :=
  @Fintype.ofFinite _ (Nat.finite_of_card_ne_zero hH)

Finite quotient group from nonzero index

Informal description

Given a subgroup $ H $ of a group $ G $, if the index of $ H $ in $ G $ is nonzero, then the quotient group $ G ⧸ H $ is finite and can be equipped with a finite type structure.

Subgroup.index_eq_zero_iff_infinite theorem

: H.index = 0 ↔ Infinite (G ⧸ H)

Full source

@[to_additive]
lemma index_eq_zero_iff_infinite : H.index = 0 ↔ Infinite (G ⧸ H) := by
  simp [index_eq_card, Nat.card_eq_zero]

Index Zero iff Quotient Infinite

Informal description

The index $[G : H]$ of a subgroup $H$ in a group $G$ is zero if and only if the quotient group $G ⧸ H$ is infinite.

Subgroup.one_lt_index_of_ne_top theorem

[Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index

Full source

@[to_additive one_lt_index_of_ne_top]
theorem one_lt_index_of_ne_top [Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index :=
  Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨index_ne_zero_of_finite, mt index_eq_one.mp hH⟩

Index Greater Than One for Proper Subgroups with Finite Quotient

Informal description

For a subgroup $H$ of a group $G$, if the quotient group $G/H$ is finite and $H$ is not equal to the entire group $G$ (i.e., $H \neq G$), then the index $[G:H]$ is strictly greater than $1$.

Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero theorem

 {X : Type*} [MulAction G X] [Finite <| MulAction.orbitRel.Quotient G X] (hi : H.index ≠ 0) :
  Finite <| MulAction.orbitRel.Quotient H X

Full source

@[to_additive]
lemma finite_quotient_of_finite_quotient_of_index_ne_zero {X : Type*} [MulAction G X]
    [Finite <| MulAction.orbitRel.Quotient G X] (hi : H.index ≠ 0) :
    Finite <| MulAction.orbitRel.Quotient H X := by
  have := fintypeOfIndexNeZero hi
  exact MulAction.finite_quotient_of_finite_quotient_of_finite_quotient

Finiteness of $H$-Orbit Quotient under Finite $G$-Orbit Quotient and Finite Index

Informal description

Let $G$ be a group acting on a set $X$, and let $H$ be a subgroup of $G$. If the quotient of $X$ by the $G$-action is finite and the index $[G : H]$ is nonzero, then the quotient of $X$ by the $H$-action is also finite.

Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero theorem

 {X : Type*} [MulAction G X] [MulAction.IsPretransitive G X] (hi : H.index ≠ 0) :
  Finite <| MulAction.orbitRel.Quotient H X

Full source

@[to_additive]
lemma finite_quotient_of_pretransitive_of_index_ne_zero {X : Type*} [MulAction G X]
    [MulAction.IsPretransitive G X] (hi : H.index ≠ 0) :
    Finite <| MulAction.orbitRel.Quotient H X := by
  have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance
  exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

Finiteness of $H$-Orbit Quotient under Pretransitive Action and Finite Index

Informal description

Let $G$ be a group acting pretransitively on a set $X$, and let $H$ be a subgroup of $G$ with finite index (i.e., $[G : H] \neq 0$). Then the quotient set $X/H$ (formed by the $H$-orbit equivalence relation) is finite.

Subgroup.exists_pow_mem_of_index_ne_zero theorem

(h : H.index ≠ 0) (a : G) : ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Full source

@[to_additive]
lemma exists_pow_mem_of_index_ne_zero (h : H.index ≠ 0) (a : G) :
    ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H := by
  suffices ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hlt, hle, he⟩
    refine ⟨n₂ - n₁, by omega, by omega, ?_⟩
    rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he
    rw [← zpow_natCast]
    convert he
    omega
  suffices ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧
      ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
    rcases hne.lt_or_lt with hlt | hlt
    · exact ⟨n₁, n₂, hlt, hle₂, he⟩
    · exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩
  by_contra hc
  simp_rw [not_exists] at hc
  let f : (Set.Icc 0 H.index) → G ⧸ H := fun n ↦ (a ^ (n : ℕ) : G)
  have hf : Function.Injective f := by
    rintro ⟨n₁, h₁, hle₁⟩ ⟨n₂, h₂, hle₂⟩ he
    have hc' := hc n₁ n₂
    dsimp only [f] at he
    simpa [hle₁, hle₂, he] using hc'
  have := (fintypeOfIndexNeZero h).finite
  have hcard := Finite.card_le_of_injective f hf
  simp [← index_eq_card] at hcard

Existence of Positive Power in Subgroup for Finite Index: $a^n \in H$ with $0 < n \leq H.index$

Informal description

For any subgroup $H$ of a group $G$ with finite index (i.e., $H.index \neq 0$) and any element $a \in G$, there exists a positive integer $n$ such that $0 < n \leq H.index$ and $a^n \in H$.

Subgroup.exists_pow_mem_of_relindex_ne_zero theorem

(h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) : ∃ n, 0 < n ∧ n ≤ H.relindex K ∧ a ^ n ∈ H ⊓ K

Full source

@[to_additive]
lemma exists_pow_mem_of_relindex_ne_zero (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) :
    ∃ n, 0 < n ∧ n ≤ H.relindex K ∧ a ^ n ∈ H ⊓ K := by
  rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩
  refine ⟨n, hlt, hle, ?_⟩
  simpa [pow_mem ha, mem_subgroupOf] using he

Existence of Positive Power in Subgroup Intersection for Finite Relative Index: $a^n \in H \cap K$ with $0 < n \leq H.\text{relindex} K$

Informal description

For any subgroups $H$ and $K$ of a group $G$ with finite relative index (i.e., $H.\text{relindex} K \neq 0$) and any element $a \in K$, there exists a positive integer $n$ such that $0 < n \leq H.\text{relindex} K$ and $a^n \in H \cap K$.

Subgroup.pow_mem_of_index_ne_zero_of_dvd theorem

(h : H.index ≠ 0) (a : G) {n : ℕ} (hn : ∀ m, 0 < m → m ≤ H.index → m ∣ n) : a ^ n ∈ H

Full source

@[to_additive]
lemma pow_mem_of_index_ne_zero_of_dvd (h : H.index ≠ 0) (a : G) {n : ℕ}
    (hn : ∀ m, 0 < m → m ≤ H.index → m ∣ n) : a ^ n ∈ H := by
  rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩
  rcases hn m hlt hle with ⟨k, rfl⟩
  rw [pow_mul]
  exact pow_mem he _

Power Membership in Subgroup via Divisibility Condition: $a^n \in H$ when $n$ is divisible by all $0 < m \leq H.index$

Informal description

For any subgroup $H$ of a group $G$ with finite index (i.e., $H.index \neq 0$) and any element $a \in G$, if a natural number $n$ is divisible by every positive integer $m$ satisfying $0 < m \leq H.index$, then $a^n \in H$.

Subgroup.pow_mem_of_relindex_ne_zero_of_dvd theorem

 (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ} (hn : ∀ m, 0 < m → m ≤ H.relindex K → m ∣ n) : a ^ n ∈ H ⊓ K

Full source

@[to_additive]
lemma pow_mem_of_relindex_ne_zero_of_dvd (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ}
    (hn : ∀ m, 0 < m → m ≤ H.relindex K → m ∣ n) : a ^ n ∈ H ⊓ K := by
  convert pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn
  simp [pow_mem ha, mem_subgroupOf]

Power Membership in Subgroup Intersection via Divisibility Condition: $a^n \in H \cap K$ when $n$ is divisible by all $0 < m \leq H.\text{relindex} K$

Informal description

Let $H$ and $K$ be subgroups of a group $G$ with finite relative index (i.e., $H.\text{relindex} K \neq 0$). For any element $a \in K$ and any natural number $n$ that is divisible by every positive integer $m$ satisfying $0 < m \leq H.\text{relindex} K$, we have $a^n \in H \cap K$.

Subgroup.index_prod theorem

(H : Subgroup G) (K : Subgroup G') : (H.prod K).index = H.index * K.index

Full source

@[to_additive (attr := simp) index_prod]
lemma index_prod (H : Subgroup G) (K : Subgroup G') : (H.prod K).index = H.index * K.index := by
  simp_rw [index, ← Nat.card_prod]
  refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.prodQuotientEquiv _ _).symm)
  rw [QuotientGroup.leftRel_prod]

Index of Product Subgroup Equals Product of Indices

Informal description

Let $G$ and $G'$ be groups with subgroups $H \subseteq G$ and $K \subseteq G'$ respectively. The index of the product subgroup $H \times K$ in $G \times G'$ is equal to the product of the indices of $H$ in $G$ and $K$ in $G'$, i.e., $$(H \times K).\text{index} = H.\text{index} \cdot K.\text{index}.$$

Subgroup.index_pi theorem

{ι : Type*} [Fintype ι] (H : ι → Subgroup G) : (Subgroup.pi Set.univ H).index = ∏ i, (H i).index

Full source

@[to_additive (attr := simp)]
lemma index_pi {ι : Type*} [Fintype ι] (H : ι → Subgroup G) :
    (Subgroup.pi Set.univ H).index = ∏ i, (H i).index := by
  simp_rw [index, ← Nat.card_pi]
  refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)
  rw [QuotientGroup.leftRel_pi]

Product Formula for Subgroup Indices: $\text{index}(\prod_i H_i) = \prod_i \text{index}(H_i)$

Informal description

Let $G$ be a group and $\iota$ a finite type. For any family of subgroups $H_i \leq G$ indexed by $\iota$, the index of the product subgroup $\prod_{i \in \iota} H_i$ in $G$ is equal to the product of the indices of the subgroups $H_i$ in $G$, i.e., \[ \text{index}(\prod_{i \in \iota} H_i) = \prod_{i \in \iota} \text{index}(H_i). \]

Subgroup.index_toAddSubgroup theorem

: (Subgroup.toAddSubgroup H).index = H.index

Full source

@[simp]
lemma index_toAddSubgroup : (Subgroup.toAddSubgroup H).index = H.index :=
  rfl

Equality of Indices for Multiplicative and Additive Subgroups

Informal description

For any subgroup $H$ of a group $G$, the index of $H$ as an additive subgroup (via the conversion `Subgroup.toAddSubgroup`) is equal to the index of $H$ as a multiplicative subgroup.

AddSubgroup.index_toSubgroup theorem

{G : Type*} [AddGroup G] (H : AddSubgroup G) : (AddSubgroup.toSubgroup H).index = H.index

Full source

@[simp]
lemma _root_.AddSubgroup.index_toSubgroup {G : Type*} [AddGroup G] (H : AddSubgroup G) :
    (AddSubgroup.toSubgroup H).index = H.index :=
  rfl

Equality of Indices for Additive and Multiplicative Subgroups

Informal description

For any additive subgroup $H$ of an additive group $G$, the index of $H$ as an additive subgroup is equal to the index of $H$ when viewed as a multiplicative subgroup via the natural equivalence between additive and multiplicative subgroups.

Subgroup.relindex_toAddSubgroup theorem

: (Subgroup.toAddSubgroup H).relindex (Subgroup.toAddSubgroup K) = H.relindex K

Full source

@[simp]
lemma relindex_toAddSubgroup :
    (Subgroup.toAddSubgroup H).relindex (Subgroup.toAddSubgroup K) = H.relindex K :=
  rfl

Equality of Relative Indices for Multiplicative and Additive Subgroups

Informal description

For any subgroups $H$ and $K$ of a group $G$, the relative index of $H$ in $K$ is equal to the relative index of the corresponding additive subgroups under the natural conversion between multiplicative and additive subgroups. That is, $\text{relindex}(\text{toAddSubgroup}(H), \text{toAddSubgroup}(K)) = \text{relindex}(H, K)$.

AddSubgroup.relindex_toSubgroup theorem

 {G : Type*} [AddGroup G] (H K : AddSubgroup G) :
  (AddSubgroup.toSubgroup H).relindex (AddSubgroup.toSubgroup K) = H.relindex K

Full source

@[simp]
lemma _root_.AddSubgroup.relindex_toSubgroup {G : Type*} [AddGroup G] (H K : AddSubgroup G) :
    (AddSubgroup.toSubgroup H).relindex (AddSubgroup.toSubgroup K) = H.relindex K :=
  rfl

Equality of Relative Indices for Additive and Multiplicative Subgroups

Informal description

For any additive subgroups $H$ and $K$ of an additive group $G$, the relative index of $H$ in $K$ is equal to the relative index of the corresponding multiplicative subgroups under the natural equivalence between additive and multiplicative subgroups. That is, $\text{relindex}(H_{\text{add}}, K_{\text{add}}) = \text{relindex}(H_{\text{mul}}, K_{\text{mul}})$, where $H_{\text{mul}}$ and $K_{\text{mul}}$ are the multiplicative versions of $H$ and $K$ respectively.

AddSubgroup.FiniteIndex structure

{G : Type*} [AddGroup G] (H : AddSubgroup G)

Full source

/-- Typeclass for finite index subgroups. -/
class _root_.AddSubgroup.FiniteIndex {G : Type*} [AddGroup G] (H : AddSubgroup G) : Prop where
  /-- The additive subgroup has finite index;
  recall that `AddSubgroup.index` returns 0 when the index is infinite. -/
  index_ne_zero : H.index ≠ 0

Finite index subgroup of an additive group

Informal description

The structure representing the property that a subgroup $ H $ of an additive group $ G $ has finite index, meaning the number of cosets of $ H $ in $ G $ is finite.

Subgroup.FiniteIndex structure

Full source

/-- Typeclass for finite index subgroups. -/
@[to_additive] class FiniteIndex : Prop where
  /-- The subgroup has finite index;
  recall that `Subgroup.index` returns 0 when the index is infinite. -/
  index_ne_zero : H.index ≠ 0

Finite index subgroup

Informal description

The structure `Subgroup.FiniteIndex` is a typeclass that asserts a subgroup $ H $ of a group $ G $ has finite index, meaning the number of cosets $ G/H $ is finite.

AddSubgroup.IsFiniteRelIndex structure

{G : Type*} [AddGroup G] (H K : AddSubgroup G)

Full source

/-- Typeclass for a subgroup `H` to have finite index in a subgroup `K`. -/
class _root_.AddSubgroup.IsFiniteRelIndex {G : Type*} [AddGroup G] (H K : AddSubgroup G) :
    Prop where
  protected relindex_ne_zero : H.relindex K ≠ 0

Finite relative index of additive subgroups

Informal description

The structure representing the property that a subgroup $ H $ of an additive group $ G $ has finite relative index in another subgroup $ K $, meaning the number of cosets $ K/H $ is finite.

Subgroup.IsFiniteRelIndex structure

Full source

/-- Typeclass for a subgroup `H` to have finite index in a subgroup `K`. -/
@[to_additive] class IsFiniteRelIndex : Prop where
  protected relindex_ne_zero : H.relindex K ≠ 0

Finite relative index subgroup

Informal description

The structure `Subgroup.IsFiniteRelIndex` is a typeclass that asserts a subgroup $ H $ of a group $ G $ has finite relative index in another subgroup $ K $, meaning the number of cosets $ K/H $ is finite.

Subgroup.relindex_ne_zero theorem

[H.IsFiniteRelIndex K] : H.relindex K ≠ 0

Full source

@[to_additive] lemma relindex_ne_zero  [H.IsFiniteRelIndex K] : H.relindex K ≠ 0 :=
  IsFiniteRelIndex.relindex_ne_zero

Nonzero Relative Index for Finite Index Subgroups

Informal description

For any subgroups $H$ and $K$ of a group $G$, if $H$ has finite relative index in $K$, then the relative index $\text{relindex}(H, K)$ is nonzero.

Subgroup.IsFiniteRelIndex.to_finiteIndex_subgroupOf instance

[H.IsFiniteRelIndex K] : (H.subgroupOf K).FiniteIndex

Full source

@[to_additive]
instance IsFiniteRelIndex.to_finiteIndex_subgroupOf [H.IsFiniteRelIndex K] :
    (H.subgroupOf K).FiniteIndex where
  index_ne_zero := relindex_ne_zero

Finite Relative Index Implies Finite Index in Subgroup

Informal description

For any subgroups $H$ and $K$ of a group $G$, if $H$ has finite relative index in $K$, then the subgroup $H \cap K$ has finite index in $K$.

Subgroup.fintypeQuotientOfFiniteIndex definition

[FiniteIndex H] : Fintype (G ⧸ H)

Full source

/-- A finite index subgroup has finite quotient. -/
@[to_additive "A finite index subgroup has finite quotient"]
noncomputable def fintypeQuotientOfFiniteIndex [FiniteIndex H] : Fintype (G ⧸ H) :=
  fintypeOfIndexNeZero FiniteIndex.index_ne_zero

Finite type structure on quotient group from finite index subgroup

Informal description

Given a subgroup $ H $ of a group $ G $ with finite index, the quotient group $ G ⧸ H $ can be equipped with a finite type structure.

Subgroup.finite_quotient_of_finiteIndex instance

[FiniteIndex H] : Finite (G ⧸ H)

Full source

@[to_additive]
instance finite_quotient_of_finiteIndex [FiniteIndex H] : Finite (G ⧸ H) :=
  fintypeQuotientOfFiniteIndex.finite

Finite Quotient from Finite Index Subgroup

Informal description

For any subgroup $H$ of a group $G$ with finite index, the quotient group $G ⧸ H$ is finite.

Subgroup.finiteIndex_of_finite_quotient theorem

[Finite (G ⧸ H)] : FiniteIndex H

Full source

@[to_additive]
theorem finiteIndex_of_finite_quotient [Finite (G ⧸ H)] : FiniteIndex H :=
  ⟨index_ne_zero_of_finite⟩

Finite Quotient Implies Finite Index Subgroup

Informal description

For any subgroup $H$ of a group $G$, if the quotient group $G/H$ is finite, then $H$ has finite index in $G$.

Subgroup.finiteIndex_of_finite instance

[Finite G] : FiniteIndex H

Full source

@[to_additive]
instance (priority := 100) finiteIndex_of_finite [Finite G] : FiniteIndex H :=
  @finiteIndex_of_finite_quotient _ _ H (Quotient.finite _)

Finite Groups Have Finite Index Subgroups

Informal description

For any finite group $G$ and subgroup $H$ of $G$, $H$ has finite index in $G$.

Subgroup.instFiniteIndexTop instance

: FiniteIndex (⊤ : Subgroup G)

Full source

@[to_additive]
instance : FiniteIndex (⊤ : Subgroup G) :=
  ⟨ne_of_eq_of_ne index_top one_ne_zero⟩

Finite Index of Trivial Subgroup

Informal description

The trivial subgroup $\top$ of a group $G$ has finite index.

Subgroup.instFiniteIndexMin instance

[FiniteIndex H] [FiniteIndex K] : FiniteIndex (H ⊓ K)

Full source

@[to_additive]
instance [FiniteIndex H] [FiniteIndex K] : FiniteIndex (H ⊓ K) :=
  ⟨index_inf_ne_zero FiniteIndex.index_ne_zero FiniteIndex.index_ne_zero⟩

Finite Index Property of Subgroup Intersection

Informal description

For any subgroups $H$ and $K$ of a group $G$, if both $H$ and $K$ have finite index in $G$, then their intersection $H \cap K$ also has finite index in $G$.

Subgroup.finiteIndex_iInf theorem

{ι : Type*} [Finite ι] {f : ι → Subgroup G} (hf : ∀ i, (f i).FiniteIndex) : (⨅ i, f i).FiniteIndex

Full source

@[to_additive]
theorem finiteIndex_iInf {ι : Type*} [Finite ι] {f : ι → Subgroup G}
    (hf : ∀ i, (f i).FiniteIndex) : (⨅ i, f i).FiniteIndex :=
  ⟨index_iInf_ne_zero fun i => (hf i).index_ne_zero⟩

Finite Index Property of Finite Intersection of Subgroups

Informal description

Let $G$ be a group and $\{H_i\}_{i \in \iota}$ be a finite family of subgroups of $G$ indexed by a finite type $\iota$. If each subgroup $H_i$ has finite index in $G$, then the intersection $\bigcap_{i \in \iota} H_i$ also has finite index in $G$.

Subgroup.finiteIndex_iInf' theorem

 {ι : Type*} {s : Finset ι} (f : ι → Subgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) : (⨅ i ∈ s, f i).FiniteIndex

Full source

@[to_additive]
theorem finiteIndex_iInf' {ι : Type*} {s : Finset ι}
    (f : ι → Subgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) :
    (⨅ i ∈ s, f i).FiniteIndex := by
  rw [iInf_subtype']
  exact finiteIndex_iInf fun ⟨i, hi⟩ => hs i hi

Finite Index Property of Finite Intersection of Subgroups (Finset Version)

Informal description

Let $G$ be a group and $\{H_i\}_{i \in \iota}$ be a family of subgroups of $G$ indexed by a finite set $s \subseteq \iota$. If each subgroup $H_i$ for $i \in s$ has finite index in $G$, then the intersection $\bigcap_{i \in s} H_i$ also has finite index in $G$.

Subgroup.instFiniteIndex_subgroupOf instance

(H K : Subgroup G) [H.FiniteIndex] : (H.subgroupOf K).FiniteIndex

Full source

@[to_additive]
instance instFiniteIndex_subgroupOf (H K : Subgroup G) [H.FiniteIndex] :
    (H.subgroupOf K).FiniteIndex :=
  ⟨fun h => H.index_ne_zero_of_finite <| H.index_eq_zero_of_relindex_eq_zero h⟩

Finite Index Property of Subgroup Intersection

Informal description

For any subgroups $H$ and $K$ of a group $G$, if $H$ has finite index in $G$, then the subgroup $H \cap K$ has finite index in $K$.

Subgroup.finiteIndex_of_le theorem

[FiniteIndex H] (h : H ≤ K) : FiniteIndex K

Full source

@[to_additive]
theorem finiteIndex_of_le [FiniteIndex H] (h : H ≤ K) : FiniteIndex K :=
  ⟨ne_zero_of_dvd_ne_zero FiniteIndex.index_ne_zero (index_dvd_of_le h)⟩

Finite index is preserved under subgroup inclusion

Informal description

If $H$ is a subgroup of finite index in a group $G$ and $H \leq K$ for another subgroup $K$ of $G$, then $K$ also has finite index in $G$.

Subgroup.index_antitone theorem

(h : H ≤ K) [H.FiniteIndex] : K.index ≤ H.index

Full source

@[to_additive (attr := gcongr)]
lemma index_antitone (h : H ≤ K) [H.FiniteIndex] : K.index ≤ H.index :=
  Nat.le_of_dvd (Nat.zero_lt_of_ne_zero FiniteIndex.index_ne_zero) (index_dvd_of_le h)

Monotonicity of Subgroup Index: $|G : K| \leq |G : H|$ for $H \leq K$

Informal description

For any subgroups $H \leq K$ of a group $G$ where $H$ has finite index, the index of $K$ in $G$ is less than or equal to the index of $H$ in $G$, i.e., $|G : K| \leq |G : H|$.

Subgroup.index_strictAnti theorem

(h : H < K) [H.FiniteIndex] : K.index < H.index

Full source

@[to_additive (attr := gcongr)]
lemma index_strictAnti (h : H < K) [H.FiniteIndex] : K.index < H.index := by
  have h0 : K.index ≠ 0 := (finiteIndex_of_le h.le).index_ne_zero
  apply lt_of_le_of_ne (index_antitone h.le)
  rw [← relindex_mul_index h.le, Ne, eq_comm, mul_eq_right₀ h0, relindex_eq_one]
  exact h.not_le

Strict Monotonicity of Subgroup Index: $|G : K| < |G : H|$ for $H < K$

Informal description

For any subgroups $H < K$ of a group $G$ where $H$ has finite index, the index of $K$ in $G$ is strictly less than the index of $H$ in $G$, i.e., $|G : K| < |G : H|$.

Subgroup.finiteIndex_ker instance

{G' : Type*} [Group G'] (f : G →* G') [Finite f.range] : f.ker.FiniteIndex

Full source

@[to_additive]
instance finiteIndex_ker {G' : Type*} [Group G'] (f : G →* G') [Finite f.range] :
    f.ker.FiniteIndex :=
  @finiteIndex_of_finite_quotient G _ f.ker
    (Finite.of_equiv f.range (QuotientGroup.quotientKerEquivRange f).symm)

Finite Index of Kernel for Homomorphism with Finite Range

Informal description

For any group homomorphism $f \colon G \to G'$ with finite range, the kernel of $f$ has finite index in $G$.

Subgroup.finiteIndex_normalCore instance

[H.FiniteIndex] : H.normalCore.FiniteIndex

Full source

instance finiteIndex_normalCore [H.FiniteIndex] : H.normalCore.FiniteIndex := by
  rw [normalCore_eq_ker]
  infer_instance

Finite Index of Normal Core for Finite Index Subgroups

Informal description

For any subgroup $H$ of a group $G$ with finite index, the normal core of $H$ also has finite index in $G$.

MulAction.index_stabilizer theorem

: (stabilizer G x).index = (orbit G x).ncard

Full source

@[to_additive] theorem index_stabilizer :
    (stabilizer G x).index = (orbit G x).ncard :=
  (Nat.card_congr (MulAction.orbitEquivQuotientStabilizer G x)).symm.trans
    (Set.Nat.card_coe_set_eq (orbit G x))

Orbit-Stabilizer Index Theorem

Informal description

For a group $G$ acting on a set $X$ and an element $x \in X$, the index of the stabilizer subgroup $\text{stabilizer}(G, x)$ in $G$ is equal to the cardinality of the orbit of $x$ under the action of $G$. In symbols: $$[G : \text{stabilizer}(G, x)] = |G \cdot x|$$

MulAction.index_stabilizer_of_transitive theorem

[IsPretransitive G X] : (stabilizer G x).index = Nat.card X

Full source

@[to_additive] theorem index_stabilizer_of_transitive [IsPretransitive G X] :
    (stabilizer G x).index = Nat.card X := by
  rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]

Index of Stabilizer in Transitive Group Action Equals Set Cardinality

Informal description

For a group $G$ acting transitively on a set $X$ and any element $x \in X$, the index of the stabilizer subgroup $\text{stabilizer}(G, x)$ in $G$ is equal to the cardinality of $X$. In symbols: $$[G : \text{stabilizer}(G, x)] = |X|$$

MonoidHom.surjective_of_card_ker_le_div theorem

 {G M : Type*} [Group G] [Group M] [Finite G] [Finite M] (f : G →* M) (h : Nat.card f.ker ≤ Nat.card G / Nat.card M) :
  Function.Surjective f

Full source

@[to_additive AddMonoidHom.surjective_of_card_ker_le_div]
lemma surjective_of_card_ker_le_div {G M : Type*} [Group G] [Group M] [Finite G] [Finite M]
    (f : G →* M) (h : Nat.card f.ker ≤ Nat.card G / Nat.card M) : Function.Surjective f := by
  refine range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_
  rw [Subgroup.coe_top, Set.ncard_univ, ← Set.Nat.card_coe_set_eq, SetLike.coe_sort_coe,
    ← Nat.card_congr (QuotientGroup.quotientKerEquivRange f).toEquiv]
  exact Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos

Surjectivity Criterion for Group Homomorphisms via Kernel Cardinality

Informal description

Let $G$ and $M$ be finite groups, and let $f \colon G \to M$ be a group homomorphism. If the cardinality of the kernel of $f$ satisfies $|\ker f| \leq |G| / |M|$, then $f$ is surjective.

MonoidHom.card_fiber_eq_of_mem_range theorem

(f : F) {x y : M} (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) : #{g | f g = x} = #{g | f g = y}

Full source

@[to_additive]
lemma card_fiber_eq_of_mem_range (f : F) {x y : M} (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) :
    #{g | f g = x} = #{g | f g = y} := by
  rcases hx with ⟨x, rfl⟩
  rcases hy with ⟨y, rfl⟩
  rcases mul_left_surjective x y with ⟨y, rfl⟩
  conv_lhs =>
    rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]
  congr 2 with g
  simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]
  let f' := MonoidHomClass.toMonoidHom f
  show f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y
  rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]

Equal Fiber Cardinality for Elements in the Range of a Monoid Homomorphism

Informal description

For a monoid homomorphism $f \colon G \to M$ and elements $x, y \in M$ that are in the range of $f$, the number of elements $g \in G$ such that $f(g) = x$ is equal to the number of elements $g \in G$ such that $f(g) = y$.

AddSubgroup.index_smul theorem

(a : G) (S : AddSubgroup A) : (a • S).index = S.index

Full source

@[simp]
lemma index_smul (a : G) (S : AddSubgroup A) : (a • S).index = S.index :=
  index_map_of_bijective (MulAction.bijective _) _

Invariance of Subgroup Index under Translation

Informal description

For any element $a$ in a group $G$ and any additive subgroup $S$ of an additive group $A$, the index of the left translate $a \cdot S$ equals the index of $S$.

Mathlib.GroupTheory.Index

Main definitions

Main results