internlm/Lean-Github huggingface dataset:
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra Rₘ K := f.toAlgebra
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
have : IsScalarTower R Rₘ K := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra Rₘ K := f.toAlgebra
this : IsScalarTower R Rₘ K
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra Rₘ K := f.toAlgebra
this : IsScalarTower R Rₘ K
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra Rₘ K := f.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra Rₘ K := f.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
let L := FractionRing 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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra Rₘ K := f.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra Rₘ K := f.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
let g : Sₘ →+* L := IsLocalization.map _ (M := Algebra.algebraMapSubmonoid S M) (T := S⁰)
    (RingHom.id S) (Submonoid.map_le_of_le_comap _ <| hM.trans
    (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
      (NoZeroSMulDivisors.algebraMap_injective _ _)))
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra Rₘ K := f.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra Rₘ K := f.toAlgebra
this✝ : IsScalarTower R Rₘ K
this : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
letI := g.toAlgebra
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝² : Algebra Rₘ K := f.toAlgebra
this✝¹ : IsScalarTower R Rₘ K
this✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this : Algebra Sₘ L := g.toAlgebra
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝² : Algebra Rₘ K := f.toAlgebra
this✝¹ : IsScalarTower R Rₘ K
this✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this : Algebra Sₘ L := g.toAlgebra
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝³ : Algebra Rₘ K := f.toAlgebra
this✝² : IsScalarTower R Rₘ K
this✝¹ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝ : Algebra Sₘ L := g.toAlgebra
this : IsScalarTower S Sₘ L
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝³ : Algebra Rₘ K := f.toAlgebra
this✝² : IsScalarTower R Rₘ K
this✝¹ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝ : Algebra Sₘ L := g.toAlgebra
this : IsScalarTower S Sₘ L
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
letI := ((algebraMap K L).comp f).toAlgebra
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁴ : Algebra Rₘ K := f.toAlgebra
this✝³ : IsScalarTower R Rₘ K
this✝² : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝¹ : Algebra Sₘ L := g.toAlgebra
this✝ : IsScalarTower S Sₘ L
this : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁴ : Algebra Rₘ K := f.toAlgebra
this✝³ : IsScalarTower R Rₘ K
this✝² : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝¹ : Algebra Sₘ L := g.toAlgebra
this✝ : IsScalarTower S Sₘ L
this : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
haveI : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' rfl
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁵ : Algebra Rₘ K := f.toAlgebra
this✝⁴ : IsScalarTower R Rₘ K
this✝³ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝² : Algebra Sₘ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₘ L
this✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₘ K L
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Theorem: Ideal.spanIntNorm_localization
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)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra Rₘ K := f.toAlgebra
⊢ algebraMap R K = (algebraMap Rₘ K).comp (algebraMap R Rₘ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
Proof state after:
no goals