English
There is a natural isomorphism between the quotient K/(H ∩ K) and the quotient (gKg⁻¹)/(gHg⁻¹ ∩ gKg⁻¹) for any subgroups H, K of G and any conjugation action element g.
Русский
Для подгрупп H, K группы G и элемента сопряжения g существует естественное эквивалентное отображение: K/(H ∩ K) ≅ (gKg⁻¹)/(gHg⁻¹ ∩ gKg⁻¹).
LaTeX
$$$K \\,/\\ (H\\cap K) \\cong (gKg^{-1}) \\,/\\ (gHg^{-1} \\cap gKg^{-1})$$$
Lean4
/-- Equivalence of `K / (H ⊓ K)` with `gKg⁻¹/ (gHg⁻¹ ⊓ gKg⁻¹)` -/
def quotConjEquiv (H K : Subgroup G) (g : ConjAct G) :
K ⧸ H.subgroupOf K ≃ (g • K : Subgroup G) ⧸ (g • H).subgroupOf (g • K) :=
Quotient.congr (K.equivSMul g).toEquiv fun a b ↦ by
dsimp
rw [← Quotient.eq'', ← Quotient.eq'', QuotientGroup.eq, QuotientGroup.eq, mem_subgroupOf, mem_subgroupOf, ← map_inv,
← map_mul, equivSMul_apply_coe]
exact smul_mem_pointwise_smul_iff.symm
