relNorm_map_algEquiv — Mathlib

English

If σ is a base change algebra equivalence, relNorm_R(I.map σ) equals relNorm_R(I).

Русский

Если σ — алгебраическая эквивалентная смена базы, то relNorm_R(I.map σ) = relNorm_R(I).

LaTeX

$$$\mathrm{relNorm}_R(\mathrm{I.map}(\sigma)) = \mathrm{relNorm}_R(I)$$$

Lean4

@[simp]
theorem relNorm_map_algEquiv {T : Type*} [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T] [Algebra R T]
    [Module.Finite R T] [NoZeroSMulDivisors R T] (σ : S ≃ₐ[R] T) (I : Ideal S) : relNorm R (I.map σ) = relNorm R I :=
  by
  refine le_antisymm (relNorm_map_algEquiv_aux σ I) ?_
  convert relNorm_map_algEquiv_aux σ.symm (I.map σ)
  change I = map σ.symm.toAlgHom (map σ.toAlgHom I)
  simp [map_mapₐ]

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