English
There is a natural equivalence between the fixed points of the action of H on its cosets and the quotient of the normalizer by H.
Русский
Существует естественное эквивалентность между фиксированными точками действия H на косетах и делением нормализатора на H.
LaTeX
$$Equiv (MulAction.fixedPoints H (G ⧸ H)) (normalizer H ⧸ comap (normalizer H).subtype H)$$
Lean4
/-- The fixed points of the action of `H` on its cosets correspond to `normalizer H / H`. -/
def fixedPointsMulLeftCosetsEquivQuotient (H : Subgroup G) [Finite (H : Set G)] :
MulAction.fixedPoints H (G ⧸ H) ≃ normalizer H ⧸ Subgroup.comap ((normalizer H).subtype : normalizer H →* G) H :=
@subtypeQuotientEquivQuotientSubtype G (normalizer H : Set G) (_) (_) (MulAction.fixedPoints H (G ⧸ H))
(fun _ => (@mem_fixedPoints_mul_left_cosets_iff_mem_normalizer _ _ _ ‹_› _).symm)
(by
intros
unfold_projs
rw [leftRel_apply (α := normalizer H), leftRel_apply]
rfl)
