internlm/Lean-Github huggingface dataset:
Theorem: comap_map_eq_map_of_isLocalization_algebraMapSubmonoid
Proof state before:
case intro.refine_1
R : Type u_3
S : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsMaximal
Rₚ : Type ?u.245679
Sₚ : Type u_2
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ (Ideal.Quotient.mk p) α ≠ 0
Tactic:
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
Proof state after:
no goals
Theorem: comap_map_eq_map_of_isLocalization_algebraMapSubmonoid
Proof state before:
case intro.refine_2
R : Type u_3
S : Type u_1
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsMaximal
Rₚ : Type ?u.245679
Sₚ : Type u_2
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
hx : x ∈ Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β : R
hβ : (Ideal.Quotient.mk p) β = ((Ideal.Quotient.mk p) α)⁻¹
⊢ β * α = 1 + (β * α - 1)
Tactic:
rw [add_sub_cancel]
Proof state after:
no goals
Theorem: trace_quotient_eq_trace_localization_quotient
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
⊢ (Algebra.trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))
Tactic:
have : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ) := by
  apply IsScalarTower.of_algebraMap_eq'
  rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
    ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (Algebra.trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))
Theorem: trace_quotient_eq_trace_localization_quotient
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (Algebra.trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))
Tactic:
rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdealOfIsLocalization p Rₚ)
  (quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)]
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ))
        ((quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ) ((Ideal.Quotient.mk pS) x))) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))

case he
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdealOfIsLocalization p Rₚ) =
    (↑(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))
Theorem: trace_quotient_eq_trace_localization_quotient
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
⊢ IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
Tactic:
apply IsScalarTower.of_algebraMap_eq'
Proof state after:
case h
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
⊢ algebraMap R (Sₚ ⧸ pSₚ) = (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ))
Theorem: trace_quotient_eq_trace_localization_quotient
Proof state before:
case h
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
⊢ algebraMap R (Sₚ ⧸ pSₚ) = (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ))
Tactic:
rw [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), IsScalarTower.algebraMap_eq R Rₚ (Sₚ ⧸ _),
  ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq Rₚ]
Proof state after:
no goals
Theorem: trace_quotient_eq_trace_localization_quotient
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ))
        ((quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ) ((Ideal.Quotient.mk pS) x))) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ).symm
      ((Algebra.trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))
Tactic:
congr
Proof state after:
no goals
Theorem: trace_quotient_eq_trace_localization_quotient
Proof state before:
case he
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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdealOfIsLocalization p Rₚ) =
    (↑(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))
Tactic:
ext x
Proof state after:
case he.h.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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdealOfIsLocalization p Rₚ)).comp
        (Ideal.Quotient.mk p))
      x =
    (((↑(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))).comp
        (Ideal.Quotient.mk p))
      x
Theorem: trace_quotient_eq_trace_localization_quotient
Proof state before:
case he.h.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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdealOfIsLocalization p Rₚ)).comp
        (Ideal.Quotient.mk p))
      x =
    (((↑(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))).comp
        (Ideal.Quotient.mk p))
      x
Tactic:
simp only [equivQuotMaximalIdealOfIsLocalization, RingHom.quotientKerEquivOfSurjective,
  RingEquiv.coe_ringHom_trans, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
  Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk,
  quotMapEquivQuotMapMaximalIdealOfIsLocalization,
  Ideal.Quotient.algebraMap_quotient_map_quotient]
Proof state after:
case he.h.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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) x) =
    (algebraMap S (Sₚ ⧸ pSₚ)) ((algebraMap R S) x)
Theorem: trace_quotient_eq_trace_localization_quotient
Proof state before:
case he.h.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_3
Sₚ : Type u_4
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 (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) x) =
    (algebraMap S (Sₚ ⧸ pSₚ)) ((algebraMap R S) x)
Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
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
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
let Rₚ := Localization.AtPrime p
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
⊢ (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
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
let Sₚ := Localization (Algebra.algebraMapSubmonoid 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)
⊢ (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)
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
letI : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
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
⊢ (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
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsScalarTower R Rₚ Sₚ := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq])
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ₚ
⊢ (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ₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Tactic:
haveI : IsLocalization (Submonoid.map (algebraMap R S) (Ideal.primeCompl p)) Sₚ :=
  inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ)
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ₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)