case h
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (x ∈
      ⨅ (v : HeightOneSpectrum R),
        Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal) (_ : Ideal.primeCompl v.asIdeal ≤ R⁰)) ↔
    x ∈ ⊥
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
⊢ (⨅ (v : HeightOneSpectrum R),
      Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal) (_ : Ideal.primeCompl v.asIdeal ≤ R⁰)) =
    ⊥
ext x
case h
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) ↔
    x ∈ ⊥
case h
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (x ∈
      ⨅ (v : HeightOneSpectrum R),
        Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal) (_ : Ideal.primeCompl v.asIdeal ≤ R⁰)) ↔
    x ∈ ⊥
rw [Algebra.mem_iInf]
case h.mp
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥

case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
case h
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) ↔
    x ∈ ⊥
constructor
case pos
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥

case neg
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥

case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
case h.mp
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥

case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
by_cases hR : IsField R
case neg
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    ∀ (i : MaximalSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)

case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
case neg
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥

case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
all_goals rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
case pos.intro.intro
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
algebra_map_inv : ?m.940045 → R
left✝ : Function.LeftInverse algebra_map_inv ↑(algebraMap R ?m.940045)
algebra_map_right_inv : Function.RightInverse algebra_map_inv ↑(algebraMap R ?m.940045)
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥
case pos
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥
rcases Function.bijective_iff_has_inverse.mp
  (IsField.localization_map_bijective (flip nonZeroDivisors.ne_zero rfl : 0 ∉ R⁰) hR) with
  ⟨algebra_map_inv, _, algebra_map_right_inv⟩
no goals
case pos.intro.intro
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : IsField R
algebra_map_inv : ?m.940045 → R
left✝ : Function.LeftInverse algebra_map_inv ↑(algebraMap R ?m.940045)
algebra_map_right_inv : Function.RightInverse algebra_map_inv ↑(algebraMap R ?m.940045)
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    x ∈ ⊥
exact fun _ => Algebra.mem_bot.mpr ⟨algebra_map_inv x, algebra_map_right_inv x⟩
case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
no goals
case neg
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    ∀ (i : MaximalSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
exact fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)
no goals
case h.mpr
R : Type u_1
A : Type ?u.937974
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
v : HeightOneSpectrum R
inst✝ : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)) →
    ∀ (i : HeightOneSpectrum R),
      x ∈ Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal) (_ : Ideal.primeCompl i.asIdeal ≤ R⁰)
exact fun hx ⟨v, hv, hbot⟩ => hx ⟨v, dimensionLEOne v hbot hv⟩