Theorem: Ideal.spanIntNorm_map
Proof state before:
case h
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsIntegrallyClosed R
inst✝¹² : IsDomain R
inst✝¹¹ : IsDomain S
inst✝¹⁰ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Finite R S
inst✝² : Module.Free R S
I : Ideal R
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝¹⁴ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝¹³ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝¹² : IsDomain Sₚ
this✝¹¹ : IsDedekindDomain Sₚ
this✝¹⁰ : IsPrincipalIdealRing Rₚ
this✝⁹ : IsIntegrallyClosed Rₚ
this✝⁸ : NoZeroSMulDivisors Rₚ Sₚ
this✝⁷ : Module.Finite Rₚ Sₚ
K : Type u_1 := FractionRing R
f : Rₚ →+* K := IsLocalization.map K (RingHom.id R) ⋯
this✝⁶ : Algebra Rₚ K := f.toAlgebra
this✝⁵ : IsScalarTower R Rₚ K
this✝⁴ : IsFractionRing Rₚ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ K
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝³ : Algebra Sₚ L := g.toAlgebra
this✝² : IsScalarTower S Sₚ (FractionRing S)
this✝¹ : IsFractionRing Sₚ (FractionRing S) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
this✝ : Algebra Rₚ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₚ K L
⊢ algebraMap Rₚ L = (algebraMap Sₚ L).comp (algebraMap Rₚ Sₚ)
Tactic:
apply IsLocalization.ringHom_ext P.primeCompl
Proof state after:
case h.h
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsIntegrallyClosed R
inst✝¹² : IsDomain R
inst✝¹¹ : IsDomain S
inst✝¹⁰ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Module.Finite R S
inst✝² : Module.Free R S
I : Ideal R
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_2 := Localization P'
this✝¹⁴ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝¹³ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝¹² : IsDomain Sₚ
this✝¹¹ : IsDedekindDomain Sₚ
this✝¹⁰ : IsPrincipalIdealRing Rₚ
this✝⁹ : IsIntegrallyClosed Rₚ
this✝⁸ : NoZeroSMulDivisors Rₚ Sₚ
this✝⁷ : Module.Finite Rₚ Sₚ
K : Type u_1 := FractionRing R
f : Rₚ →+* K := IsLocalization.map K (RingHom.id R) ⋯
this✝⁶ : Algebra Rₚ K := f.toAlgebra
this✝⁵ : IsScalarTower R Rₚ K
this✝⁴ : IsFractionRing Rₚ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ K
L : Type u_2 := FractionRing S
g : Sₚ →+* L := IsLocalization.map L (RingHom.id S) h
this✝³ : Algebra Sₚ L := g.toAlgebra
this✝² : IsScalarTower S Sₚ (FractionRing S)
this✝¹ : IsFractionRing Sₚ (FractionRing S) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
this✝ : Algebra Rₚ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₚ K L
⊢ (algebraMap Rₚ L).comp (algebraMap R Rₚ) = ((algebraMap Sₚ L).comp (algebraMap Rₚ Sₚ)).comp (algebraMap R Rₚ)