Theorems · Theorem · commutative algebra

Algebra.intNorm_eq_of_isLocalization

∀ {A : Type u_1} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {Aₘ : Type u_9}
  {Bₘ : Type u_10} [inst_3 : CommRing Aₘ] [inst_4 : CommRing Bₘ] [inst_5 : Algebra Aₘ Bₘ] [inst_6 : Algebra A Aₘ]
  [inst_7 : Algebra B Bₘ] [inst_8 : Algebra A Bₘ] [IsScalarTower A Aₘ Bₘ] [IsScalarTower A B Bₘ] (M : Submonoid A)
  [IsLocalization M Aₘ] [IsLocalization (Algebra.algebraMapSubmonoid B M) Bₘ] [inst_13 : IsIntegrallyClosed A]
  [inst_14 : IsDomain A] [inst_15 : IsDomain B] [inst_16 : IsIntegrallyClosed B] [inst_17 : Algebra.IsIntegral A B]
  [inst_18 : Module.IsTorsionFree A B] [inst_19 : IsDomain Aₘ] [inst_20 : IsIntegrallyClosed Aₘ] [inst_21 : IsDomain Bₘ]
  [inst_22 : IsIntegrallyClosed Bₘ] [inst_23 : Module.IsTorsionFree Aₘ Bₘ] [inst_24 : Algebra.IsIntegral Aₘ Bₘ]
  [FiniteDimensional (FractionRing A) (FractionRing B)] (x : B),
  (algebraMap A Aₘ) ((Algebra.intNorm A B) x) = (Algebra.intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Defined in

Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Cited by

1 results in Mathlib

Foundations

Depth 186 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsLocalizationIsLocalizationIsIntegrallyClosedIsDomainIsDomainIsIntegrallyClosedAlgebra.IsIntegralModule.IsTorsionFreeIsDomainIsIntegrallyClosedIsDomainIsIntegrallyClosedModule.IsTorsionFreeAlgebra.IsIntegralFiniteDimensional