English
Let K be a subgroup and S its complement in G, then two elements g1,g2 have equal left coset representatives in the decomposition if and only if the left cosets of K containing g1 and g2 are equal.
Русский
Пусть K — подгруппа и S — её дополнение в G. Два элемента g1,g2 имеют равные представления левых косет в разложении тогда и только тогда, когда левые косеты, содержащие g1 и g2, совпадают.
LaTeX
$$$ (\exists! s\in S, t\in K): g_i = s t \text{ for } i=1,2 \quad\text{iff}\quad \text{LeftCosetEquivalence}(K,g_1,g_2). $$$
Lean4
theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} :
(hSK.equiv g₁).fst = (hSK.equiv g₂).fst ↔ LeftCosetEquivalence K g₁ g₂ :=
by
rw [LeftCosetEquivalence, leftCoset_eq_iff]
constructor
· intro h
rw [← hSK.equiv_fst_mul_equiv_snd g₂, ← hSK.equiv_fst_mul_equiv_snd g₁, ← h, mul_inv_rev, ← mul_assoc,
inv_mul_cancel_right, ← coe_inv, ← coe_mul]
exact Subtype.property _
· intro h
apply (isComplement_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique
· -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
rw [equiv_fst_eq_mul_inv]; simp
· rw [SetLike.mem_coe, ← mul_mem_cancel_right h]
-- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
rw [equiv_fst_eq_mul_inv]; simp [← mul_assoc]
