internlm/Lean-Github huggingface dataset:
Theorem: Ideal.spanIntNorm_mul
Proof state before:
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 J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
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 Sₚ
this✝⁴ : IsIntegrallyClosed Rₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
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)
⊢ IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
Tactic:
haveI : IsScalarTower R Rₚ (FractionRing R) := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.lift_comp])
Proof state after:
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 J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
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 Sₚ
this✝⁵ : IsIntegrallyClosed Rₚ
this✝⁴ : NoZeroSMulDivisors Rₚ Sₚ
this✝³ : Module.Finite Rₚ Sₚ
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 : IsScalarTower R Rₚ (FractionRing R)
⊢ IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
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 J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
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 Sₚ
this✝⁵ : IsIntegrallyClosed Rₚ
this✝⁴ : NoZeroSMulDivisors Rₚ Sₚ
this✝³ : Module.Finite Rₚ Sₚ
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 : IsScalarTower R Rₚ (FractionRing R)
⊢ IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
Tactic:
letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
  P.primeCompl Rₚ (FractionRing R)
Proof state after:
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 J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
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 Sₚ
this✝⁶ : IsIntegrallyClosed Rₚ
this✝⁵ : NoZeroSMulDivisors Rₚ Sₚ
this✝⁴ : Module.Finite Rₚ Sₚ
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✝ : IsScalarTower R Rₚ (FractionRing R)
this : IsFractionRing Rₚ (FractionRing R) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ (FractionRing R)
⊢ IsSeparable (FractionRing Rₚ) (FractionRing Sₚ)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case he.h.a
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 J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
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 Sₚ
this✝⁶ : IsIntegrallyClosed Rₚ
this✝⁵ : NoZeroSMulDivisors Rₚ Sₚ
this✝⁴ : Module.Finite Rₚ Sₚ
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✝ : IsScalarTower R Rₚ (FractionRing R)
this : IsFractionRing Rₚ (FractionRing R) :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P.primeCompl Rₚ (FractionRing R)
x✝ : R
⊢ (algebraMap (FractionRing Rₚ) (FractionRing Sₚ)) ((algebraMap R (FractionRing Rₚ)) x✝) =
    (algebraMap R (FractionRing Sₚ)) x✝
Tactic:
rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing Rₚ), ← IsScalarTower.algebraMap_apply Rₚ,
  ← IsScalarTower.algebraMap_apply]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul
Proof state before:
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 J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
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 Sₚ
this✝⁴ : IsIntegrallyClosed Rₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
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)
⊢ algebraMap R (FractionRing R) = (algebraMap Rₚ (FractionRing R)).comp (algebraMap R Rₚ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.lift_comp]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ spanIntNorm R (map (algebraMap R S) I) = I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S)
Tactic:
nontriviality R
Proof state after:
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
⊢ spanIntNorm R (map (algebraMap R S) I) = I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S)
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ spanIntNorm R (map (algebraMap R S) I) = I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S)
Tactic:
nontriviality S
Proof state after:
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
⊢ spanIntNorm R (map (algebraMap R S) I) = I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S)
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ spanIntNorm R (map (algebraMap R S) I) = I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S)
Tactic:
refine eq_of_localization_maximal ?_
Proof state after:
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) (x : P.IsMaximal),
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
      map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Theorem: Ideal.spanIntNorm_map
Proof state before:
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) (x : P.IsMaximal),
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
      map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
intro P hPd
Proof state after:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
let P' := Algebra.algebraMapSubmonoid S P.primeCompl
Proof state after:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
let Rₚ := Localization.AtPrime P
Proof state after:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
let Sₚ := Localization P'
Proof state after:
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'
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Theorem: Ideal.spanIntNorm_map
Proof state before:
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'
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
letI : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
Proof state after:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Theorem: Ideal.spanIntNorm_map
Proof state before:
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
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))
Tactic:
haveI : IsScalarTower R Rₚ Sₚ :=
  IsScalarTower.of_algebraMap_eq (fun x =>
    (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
Proof state after:
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ₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ FiniteDimensional.finrank (FractionRing R) (FractionRing S))