English
For subgroups D ≤ H of a group G where D has finite index in H, there exists a finite left transversal of D in H. Equivalently, H is covered by finitely many left cosets of D with a complement property.
Русский
Для подгрупп D ≤ H в G, где D имеет конечный индекс в H, существует конечный левый транзверсал D в H.
LaTeX
$$$\exists t : Finset H, \, IsComplement (t : Set H) (D.subgroupOf H) \, \wedge \, \bigcup_{g \in t} g D = H$$$
Lean4
@[to_additive]
theorem exists_leftTransversal_of_FiniteIndex {D H : Subgroup G} [D.FiniteIndex] (hD_le_H : D ≤ H) :
∃ t : Finset H, IsComplement (t : Set H) (D.subgroupOf H) ∧ ⋃ g ∈ t, (g : G) • (D : Set G) = H :=
by
have ⟨t, ht⟩ := (D.subgroupOf H).exists_isComplement_left 1
have hf : t.Finite := ht.1.finite_left_iff.mpr inferInstance
refine ⟨hf.toFinset, hf.coe_toFinset.symm ▸ ht.1, ?_⟩
ext x
suffices (∃ y ∈ t, ∃ d ∈ D, y * d = x) ↔ x ∈ H by simpa using this
constructor
· rintro ⟨⟨y, hy⟩, -, d, h, rfl⟩
exact H.mul_mem hy (hD_le_H h)
· intro hx
exact ⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _, ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩
