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ₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
have e : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
  Submonoid.map_le_of_le_comap _ <| p.primeCompl_le_nonZeroDivisors.trans
    (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
      (NoZeroSMulDivisors.algebraMap_injective _ _))
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⁰
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
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⁰
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e
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ₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
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ₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : NoZeroSMulDivisors Rₚ Sₚ := by
  rw [NoZeroSMulDivisors.iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
    RingHom.ker_eq_bot_iff_eq_zero]
  intro x hx
  obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl x
  simp only [RingHom.algebraMap_toAlgebra, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    mul_eq_zero, Subtype.exists, exists_prop] at hx ⊢
  obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
  simp only [(injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
  refine ⟨a, ha, H⟩
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ₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
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ₚ
this : NoZeroSMulDivisors Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : Module.Finite Rₚ Sₚ := Module.Finite_of_isLocalization R S _ _ p.primeCompl
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ₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
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ₚ
this✝ : NoZeroSMulDivisors Rₚ Sₚ
this : Module.Finite Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsIntegrallyClosed Sₚ := isIntegrallyClosed_of_isLocalization _ e _
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ₚ
this✝¹ : NoZeroSMulDivisors Rₚ Sₚ
this✝ : Module.Finite Rₚ Sₚ
this : IsIntegrallyClosed Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
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ₚ
this✝² : NoZeroSMulDivisors Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
this : IsPrincipalIdealRing Rₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'
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ₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
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ₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
apply (equivQuotMaximalIdealOfIsLocalization p Rₚ).injective
Proof state after:
case a
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ₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x)) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case a
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ₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x)) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Tactic:
rw [trace_quotient_eq_trace_localization_quotient S p Rₚ Sₚ, IsScalarTower.algebraMap_eq S Sₚ,
  RingHom.comp_apply, Ideal.Quotient.algebraMap_eq, Algebra.trace_quotient_mk,
  RingEquiv.apply_symm_apply, ← Algebra.intTrace_eq_trace,
  ← Algebra.intTrace_eq_of_isLocalization R S p.primeCompl (Aₘ := Rₚ) (Bₘ := Sₚ) x,
  ← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
Proof state after:
case a
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ₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Theorem: Algebra.trace_quotient_eq_of_isDedekindDomain
Proof state before:
case a
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ₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Tactic:
simp only [equivQuotMaximalIdealOfIsLocalization, RingHom.quotientKerEquivOfSurjective,
  RingEquiv.coe_trans, Function.comp_apply, Ideal.quotEquivOfEq_mk,
  RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk]
Proof state after:
no goals
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
⊢ algebraMap R Sₚ = (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
Proof state after:
no goals