internlm/Lean-Github huggingface dataset:
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
  RingHom.ker_eq_bot_iff_eq_zero]
Proof state after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Tactic:
intro x hx
Proof state after:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl x
Proof state after:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0
Tactic:
simp only [RingHom.algebraMap_toAlgebra, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
  mul_eq_zero, Subtype.exists, exists_prop] at hx ⊢
Proof state after:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : ∃ a ∈ algebraMapSubmonoid S p.primeCompl, a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
hx : ∃ a ∈ algebraMapSubmonoid S p.primeCompl, a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
Proof state after:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : (algebraMap R S) a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : (algebraMap R S) a = 0 ∨ (algebraMap R S) x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Tactic:
simp only [(injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
Proof state after:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : a = 0 ∨ x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x✝ : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝² : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
this✝ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : IsDomain Sₚ
x : R
s : ↥p.primeCompl
a : R
ha : a ∈ ↑p.primeCompl
H : a = 0 ∨ x = 0
⊢ ∃ a ∈ p.primeCompl, a = 0 ∨ x = 0
Tactic:
refine ⟨a, ha, H⟩
Proof state after:
no goals
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁵ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁴ : IsScalarTower R Rₚ Sₚ
this✝³ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝² : IsDomain Sₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
hp : p = ⊥
⊢ IsPrincipalIdealRing Rₚ
Tactic:
have : IsFractionRing R Rₚ := by
  delta IsFractionRing
  convert inferInstanceAs (IsLocalization p.primeCompl Rₚ)
  ext; simp [hp, Ideal.primeCompl, mem_nonZeroDivisors_iff_ne_zero]
Proof state after:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this : IsFractionRing R Rₚ
⊢ IsPrincipalIdealRing Rₚ
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this : IsFractionRing R Rₚ
⊢ IsPrincipalIdealRing Rₚ
Tactic:
letI : Field Rₚ := IsFractionRing.toField R
Proof state after:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this✝ : IsFractionRing R Rₚ
this : Field Rₚ := IsFractionRing.toField R
⊢ IsPrincipalIdealRing Rₚ
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case pos
R : Type u_1
S : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
p : Ideal R
inst✝¹⁷ : p.IsMaximal
Rₚ✝ : Type ?u.335608
Sₚ✝ : Type ?u.335611
inst✝¹⁶ : CommRing Rₚ✝
inst✝¹⁵ : CommRing Sₚ✝
inst✝¹⁴ : Algebra R Rₚ✝
inst✝¹³ : IsLocalization.AtPrime Rₚ✝ p
inst✝¹² : LocalRing Rₚ✝
inst✝¹¹ : CommRing Sₚ✝
inst✝¹⁰ : Algebra S Sₚ✝
inst✝⁹ : Algebra R Sₚ✝
inst✝⁸ : Algebra Rₚ✝ Sₚ✝
inst✝⁷ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
hp : p = ⊥
this✝ : IsFractionRing R Rₚ
this : Field Rₚ := IsFractionRing.toField R
⊢ IsPrincipalIdealRing Rₚ
Tactic:
infer_instance
Proof state after:
no goals