fixingSubgroup_fixedField — Mathlib

English

For a subgroup H, if the extension is finite dimensional, then fixingSubgroup of fixedField(H) equals H.

Русский

Для подгруппы H, если расширение конечномерно, то fixingSubgroup(fixedField(H)) = H.

LaTeX

$$$[\text{FiniteDimensional } F E] \Rightarrow \operatorname{fixingSubgroup}(\operatorname{fixedField}(H)) = H$$$

Lean4

theorem fixingSubgroup_fixedField [FiniteDimensional F E] : fixingSubgroup (fixedField H) = H :=
  by
  have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl
  classical
  suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact
      SetLike.coe_injective
        (Set.eq_of_inclusion_surjective
            ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
                ⟨Set.inclusion_injective H_le, this⟩).2).symm
  apply Nat.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm

Похожие утверждения