algHomEquivAut — Mathlib

English

If F and K are fields with an integral extension, the restricted trace from K to F equals the trace in the intermediate field after restriction.

Русский

Если F и K — поля, и есть целочисленное расширение, то ограниченный трейс из K в F равен трейсу в промежуточном поле после ограничения.

LaTeX

$$$\text{normalizedTrace } F K = \text{trace } F K$ after restriction to intermediate fields$$

Lean4

/-- If `K₁/E/F` is a tower of fields with `E/F` normal then `AlgHom.restrictNormal'` is an
equivalence. -/
@[simps, stacks 0BR4]
def algHomEquivAut [Normal F E] : (E →ₐ[F] K₁) ≃ E ≃ₐ[F] E
    where
  toFun σ := AlgHom.restrictNormal' σ E
  invFun σ := (IsScalarTower.toAlgHom F E K₁).comp σ.toAlgHom
  left_inv
    σ := by
    ext
    simp [AlgHom.restrictNormal']
  right_inv
    σ := by
    ext
    simp only [AlgHom.restrictNormal', AlgEquiv.toAlgHom_eq_coe, AlgEquiv.coe_ofBijective]
    apply FaithfulSMul.algebraMap_injective E K₁
    rw [AlgHom.restrictNormal_commutes]
    simp

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