internlm/Lean-Github huggingface dataset:
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inr.inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ ⊤
Tactic:
exact le_top
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inl
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Tactic:
rw [hI, spanIntNorm_eq_bot_iff.mp hI, bot_mul, spanIntNorm_bot]
Proof state after:
case inl
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inl
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanIntNorm R J
Tactic:
exact bot_le
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inr.inl
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Tactic:
rw [hJ, spanIntNorm_eq_bot_iff.mp hJ, mul_bot, spanIntNorm_bot]
Proof state after:
no goals
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
have e : Algebra.algebraMapSubmonoid S M ≤ 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✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ NoZeroSMulDivisors Rₚ Sₚ
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
haveI : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors S e
Proof state after:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ NoZeroSMulDivisors Rₚ Sₚ
Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
  (algebraMap R S) (Submonoid.le_comap_map M) := by
  apply IsLocalization.ringHom_ext M
  simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_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✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ NoZeroSMulDivisors Rₚ Sₚ
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R 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
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Tactic:
intro x hx
Proof state after:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Rₚ
hx : (algebraMap Rₚ Sₚ) x = 0
⊢ x = 0
Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x
Proof state after:
case intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ x s) = 0
⊢ IsLocalization.mk' Rₚ x s = 0
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
case intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
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,
  Subtype.exists, exists_prop, this] at hx ⊢
Proof state after:
case intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : ∃ a ∈ Algebra.algebraMapSubmonoid S M, a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
case intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
hx : ∃ a ∈ Algebra.algebraMapSubmonoid S M, a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0
Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
Proof state after:
case intro.intro.intro.intro.intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0