algebraMap_intNorm_of_isGalois — Mathlib

English

Equality of intNorm across a localization diagram, ensuring norms are coherent after localization.

Русский

Равенство intNorm в диаграмме локализации, обеспечивающее согласованность норм после локализации.

LaTeX

$$$[IsLocalization M A_m][IsLocalization (Algebra.algebraMapSubmonoid B M) B_m]\\Rightarrow algebraMap A A_m (intNorm A B x) = intNorm A_m B_m (algebraMap B B_m x)$$$

Lean4

theorem algebraMap_intNorm_of_isGalois [IsGalois (FractionRing A) (FractionRing B)] {x : B} :
    algebraMap A B (Algebra.intNorm A B x) = ∏ σ : B ≃ₐ[A] B, σ x :=
  by
  haveI : IsIntegralClosure B A (FractionRing B) := IsIntegralClosure.of_isIntegrallyClosed _ _ _
  haveI : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
  haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  rw [← (galRestrict A (FractionRing A) (FractionRing B) B).toEquiv.prod_comp]
  simp only [MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe]
  convert (prod_galRestrict_eq_norm A (FractionRing A) (FractionRing B) B x).symm

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