fixingSubgroupEquiv — Mathlib

English

The fixing subgroup of K is canonically isomorphic to the automorphism group of E over the fixed field of H, i.e., fixingSubgroup(K) ≃* E ≃ₐ[K] E.

Русский

Подгруппа фиксации K константно изоморфна группе автоморфизмов E над фиксированным полем H: fixingSubgroup(K) ≃* E ≃ₐ[K] E.

LaTeX

$$$\text{fixingSubgroup}(K) \cong_* (E \simeq_K E)$$$

Lean4

/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `E ≃ₐ[K] E`. -/
def fixingSubgroupEquiv : fixingSubgroup K ≃* E ≃ₐ[K] E
    where
  toFun ϕ := { AlgEquiv.toRingEquiv (ϕ : E ≃ₐ[F] E) with commutes' := ϕ.mem }
  invFun ϕ := ⟨ϕ.restrictScalars _, ϕ.commutes⟩
  map_mul' _ _ := by ext; rfl

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