[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
⊢ ∀ {p : Ideal Rₘ}, p ≠ ⊥ → Ideal.IsPrime p → Ideal.IsMaximal p
[PROOFSTEP]
intro p hp0 hpp
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
⊢ Ideal.IsMaximal p
[PROOFSTEP]
refine' Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => _⟩
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
⊢ False
[PROOFSTEP]
have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
hpP' : { val := p, property := hpp } < { val := P, property := (_ : Ideal.IsPrime P) }
⊢ False
[PROOFSTEP]
rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
hpP' :
  ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := p, property := hpp } <
    ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := P, property := (_ : Ideal.IsPrime P) }
⊢ False
[PROOFSTEP]
haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p) := ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩).2.1
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
hpP' :
  ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := p, property := hpp } <
    ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := P, property := (_ : Ideal.IsPrime P) }
this : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p)
⊢ False
[PROOFSTEP]
haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P) := ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
hpP' :
  ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := p, property := hpp } <
    ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := P, property := (_ : Ideal.IsPrime P) }
this✝ : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p)
this : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P)
⊢ False
[PROOFSTEP]
have _ : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
hpP' :
  ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := p, property := hpp } <
    ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := P, property := (_ : Ideal.IsPrime P) }
this✝ : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p)
this : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P)
x✝ : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P
⊢ False
[PROOFSTEP]
refine' h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨_, hpP'⟩
[GOAL]
R✝ : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
R : Type u_4
Rₘ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : Ideal.IsPrime p
P : Ideal Rₘ
hpP : p < P
hPm : Ideal.IsMaximal P
hpP' :
  ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := p, property := hpp } <
    ↑(IsLocalization.orderIsoOfPrime M Rₘ) { val := P, property := (_ : Ideal.IsPrime P) }
this✝ : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p)
this : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P)
x✝ : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P
⊢ ⊥ < Ideal.comap (algebraMap R Rₘ) ↑{ val := p, property := hpp }
[PROOFSTEP]
exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
⊢ IsDedekindDomain Aₘ
[PROOFSTEP]
have h : ∀ y : M, IsUnit (algebraMap A (FractionRing A) y) :=
  by
  rintro ⟨y, hy⟩
  exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
⊢ ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
y : A
hy : y ∈ M
⊢ IsUnit (↑(algebraMap A (FractionRing A)) ↑{ val := y, property := hy })
[PROOFSTEP]
exact IsUnit.mk0 _ (mt IsFractionRing.to_map_eq_zero_iff.mp (nonZeroDivisors.ne_zero (hM hy)))
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
⊢ IsDedekindDomain Aₘ
[PROOFSTEP]
letI : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (IsLocalization.lift h)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
⊢ IsDedekindDomain Aₘ
[PROOFSTEP]
haveI : IsScalarTower A Aₘ (FractionRing A) := IsScalarTower.of_algebraMap_eq fun x => (IsLocalization.lift_eq h x).symm
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this : IsScalarTower A Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
[PROOFSTEP]
haveI : IsFractionRing Aₘ (FractionRing A) := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M _ _
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsDedekindDomain Aₘ
[PROOFSTEP]
refine' (isDedekindDomain_iff _ (FractionRing A)).mpr ⟨_, _, _, _⟩
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsDomain Aₘ
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsNoetherianRing Aₘ
[PROOFSTEP]
exact IsLocalization.isNoetherianRing M _ (by infer_instance)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ IsNoetherianRing A
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ Ring.DimensionLEOne Aₘ
[PROOFSTEP]
exact Ring.DimensionLEOne.localization Aₘ hM
[GOAL]
case refine'_4
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
⊢ ∀ {x : FractionRing A}, IsIntegral Aₘ x → ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_4
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
[PROOFSTEP]
obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
[GOAL]
case refine'_4.intro.mk
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
[PROOFSTEP]
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindDomain.toIsIntegrallyClosed hy
[GOAL]
case refine'_4.intro.mk.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ ∃ y, ↑(algebraMap Aₘ (FractionRing A)) y = x
[PROOFSTEP]
refine' ⟨IsLocalization.mk' Aₘ z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr _⟩
[GOAL]
case refine'_4.intro.mk.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ ↑(algebraMap A (FractionRing A)) z = ↑(algebraMap A (FractionRing A)) ↑{ val := y, property := y_mem } * x
[PROOFSTEP]
rw [hz, ← Algebra.smul_def]
[GOAL]
case refine'_4.intro.mk.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : { x // x ∈ M }), IsUnit (↑(algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := RingHom.toAlgebra (lift h)
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A ({ val := y, property := y_mem } • x)
z : A
hz : ↑(algebraMap A (FractionRing A)) z = { val := y, property := y_mem } • x
⊢ { val := y, property := y_mem } • x = ↑{ val := y, property := y_mem } • x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ ¬IsField Aₘ
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
⊢ False
[PROOFSTEP]
letI := h.toField
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := IsField.toField h
⊢ False
[PROOFSTEP]
obtain ⟨x, x_mem, x_ne⟩ := P.ne_bot_iff.mp hP
[GOAL]
case intro.intro
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝² : CommRing Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
h : IsField Aₘ
this : Field Aₘ := IsField.toField h
x : A
x_mem : x ∈ P
x_ne : x ≠ 0
⊢ False
[PROOFSTEP]
exact
  (LocalRing.maximalIdeal.isMaximal _).ne_top
    (Ideal.eq_top_of_isUnit_mem _ ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
      (isUnit_iff_ne_zero.mpr
        ((map_ne_zero_iff (algebraMap A Aₘ) (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr x_ne)))
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ DiscreteValuationRing Aₘ
[PROOFSTEP]
classical
letI : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindDomain.toIsNoetherian
letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
exact ((DiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr (IsLocalization.AtPrime.isDedekindDomain A P _)
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ DiscreteValuationRing Aₘ
[PROOFSTEP]
letI : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindDomain.toIsNoetherian
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.toIsNoetherian
⊢ DiscreteValuationRing Aₘ
[PROOFSTEP]
letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.toIsNoetherian
this : LocalRing Aₘ := localRing Aₘ P
⊢ DiscreteValuationRing Aₘ
[PROOFSTEP]
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
[GOAL]
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_4
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.toIsNoetherian
this : LocalRing Aₘ := localRing Aₘ P
hnf : ¬IsField Aₘ
⊢ DiscreteValuationRing Aₘ
[PROOFSTEP]
exact ((DiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr (IsLocalization.AtPrime.isDedekindDomain A P _)