R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), FiniteDimensional.finrank (ResidueField R) (CotangentSpace R) = 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), FiniteDimensional.finrank (ResidueField R) (CotangentSpace R) = 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
have ne_bot := Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), FiniteDimensional.finrank (ResidueField R) (CotangentSpace R) = 1,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
rw [finrank_eq_one_iff']
case tfae_1_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
⊢ DiscreteValuationRing R → ValuationRing R

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 1 → 2
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
⊢ ValuationRing R → DiscreteValuationRing R

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 2 → 1
case tfae_1_to_4
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
⊢ DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 1 → 4
case tfae_4_to_3
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 4 → 3
case tfae_3_to_5
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
⊢ IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 3 → 5
case tfae_5_to_6
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 5 → 6
case tfae_6_to_5
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
⊢ (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 6 → 5
case tfae_5_to_7
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 5 → 7
case tfae_7_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → ValuationRing R

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
tfae_7_to_2 : (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → ValuationRing R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_have 7 → 2
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
tfae_7_to_2 : (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → ValuationRing R
⊢ List.TFAE
    [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P,
      Submodule.IsPrincipal (maximalIdeal R), ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w,
      ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n]
tfae_finish
case tfae_1_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
✝ : DiscreteValuationRing R
⊢ ValuationRing R
case tfae_1_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
⊢ DiscreteValuationRing R → ValuationRing R
intro
no goals
case tfae_1_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
✝ : DiscreteValuationRing R
⊢ ValuationRing R
infer_instance
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
⊢ DiscreteValuationRing R
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
⊢ ValuationRing R → DiscreteValuationRing R
intro
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this : GCDMonoid R
⊢ DiscreteValuationRing R
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
⊢ DiscreteValuationRing R
haveI := IsBezout.toGCDDomain R
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
⊢ DiscreteValuationRing R
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this : GCDMonoid R
⊢ DiscreteValuationRing R
haveI : UniqueFactorizationMonoid R := ufm_of_gcd_of_wfDvdMonoid
case tfae_2_to_1.h₁
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
⊢ ∃ p, Irreducible p

case tfae_2_to_1.h₂
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
⊢ ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
case tfae_2_to_1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
⊢ DiscreteValuationRing R
apply DiscreteValuationRing.of_ufd_of_unique_irreducible
case tfae_2_to_1.h₁.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
x : R
hx₁ : x ≠ 0
hx₂ : ¬IsUnit x
⊢ ∃ p, Irreducible p
case tfae_2_to_1.h₁
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
⊢ ∃ p, Irreducible p
obtain ⟨x, hx₁, hx₂⟩ := Ring.exists_not_isUnit_of_not_isField h
case tfae_2_to_1.h₁.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
x : R
hx₁ : x ≠ 0
hx₂ : ¬IsUnit x
p : R
hp₁ : Irreducible p
⊢ ∃ p, Irreducible p
case tfae_2_to_1.h₁.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
x : R
hx₁ : x ≠ 0
hx₂ : ¬IsUnit x
⊢ ∃ p, Irreducible p
obtain ⟨p, hp₁, -⟩ := WfDvdMonoid.exists_irreducible_factor hx₂ hx₁
no goals
case tfae_2_to_1.h₁.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
x : R
hx₁ : x ≠ 0
hx₂ : ¬IsUnit x
p : R
hp₁ : Irreducible p
⊢ ∃ p, Irreducible p
exact ⟨p, hp₁⟩
no goals
case tfae_2_to_1.h₂
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
✝ : ValuationRing R
this✝ : GCDMonoid R
this : UniqueFactorizationMonoid R
⊢ ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
exact ValuationRing.unique_irreducible
case tfae_1_to_4
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
H : DiscreteValuationRing R
⊢ IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
case tfae_1_to_4
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
⊢ DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
intro H
no goals
case tfae_1_to_4
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
H : DiscreteValuationRing R
⊢ IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
exact ⟨inferInstance, ((DiscreteValuationRing.iff_pid_with_one_nonzero_prime R).mp H).2⟩
case tfae_4_to_3.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
h₁ : IsIntegrallyClosed R
h₂ : ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ IsDedekindDomain R
case tfae_4_to_3
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
rintro ⟨h₁, h₂⟩
no goals
case tfae_4_to_3.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
h₁ : IsIntegrallyClosed R
h₂ : ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ IsDedekindDomain R
exact
  ⟨inferInstance, fun I hI hI' =>
    ExistsUnique.unique h₂ ⟨ne_bot, inferInstance⟩ ⟨hI, hI'⟩ ▸ maximalIdeal.isMaximal R, h₁⟩
case tfae_3_to_5
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
h : IsDedekindDomain R
⊢ Submodule.IsPrincipal (maximalIdeal R)
case tfae_3_to_5
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
⊢ IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
intro h
no goals
case tfae_3_to_5
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
h : IsDedekindDomain R
⊢ Submodule.IsPrincipal (maximalIdeal R)
exact maximalIdeal_isPrincipal_of_isDedekindDomain R
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
⊢ ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
case tfae_5_to_6
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
rintro ⟨x, hx⟩
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
⊢ ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
⊢ ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
have : x ∈ maximalIdeal R := by rw [hx]; exact Submodule.subset_span (Set.mem_singleton x)
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
⊢ ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
let x' : maximalIdeal R := ⟨x, this⟩
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∃ _n, ∀ (w : CotangentSpace R), ∃ c, c • Submodule.Quotient.mk x' = w
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
use Submodule.Quotient.mk x'
case tfae_5_to_6.mk.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∀ (w : CotangentSpace R), ∃ c, c • Submodule.Quotient.mk x' = w

case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ Submodule.Quotient.mk x' ≠ 0
case tfae_5_to_6.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∃ _n, ∀ (w : CotangentSpace R), ∃ c, c • Submodule.Quotient.mk x' = w
constructor
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ Submodule.Quotient.mk x' ≠ 0

case tfae_5_to_6.mk.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∀ (w : CotangentSpace R), ∃ c, c • Submodule.Quotient.mk x' = w
case tfae_5_to_6.mk.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∀ (w : CotangentSpace R), ∃ c, c • Submodule.Quotient.mk x' = w

case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ Submodule.Quotient.mk x' ≠ 0
swap
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
⊢ x ∈ Submodule.span R {x}
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
⊢ x ∈ maximalIdeal R
rw [hx]
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
⊢ x ∈ Submodule.span R {x}
exact Submodule.subset_span (Set.mem_singleton x)
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : Submodule.Quotient.mk x' = 0
⊢ False
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ Submodule.Quotient.mk x' ≠ 0
intro e
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ False
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : Submodule.Quotient.mk x' = 0
⊢ False
rw [Submodule.Quotient.mk_eq_zero] at e
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ maximalIdeal R = ⊥
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ False
apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
case tfae_5_to_6.mk.intro.w.hN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ Submodule.FG (maximalIdeal R)

case tfae_5_to_6.mk.intro.w.hIN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ maximalIdeal R ≤ maximalIdeal R • maximalIdeal R

case tfae_5_to_6.mk.intro.w.hIjac
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ maximalIdeal R ≤ Ideal.jacobson ⊥
case tfae_5_to_6.mk.intro.w
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ maximalIdeal R = ⊥
apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (maximalIdeal R)
no goals
case tfae_5_to_6.mk.intro.w.hN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ Submodule.FG (maximalIdeal R)
exact ⟨{x}, (Finset.coe_singleton x).symm ▸ hx.symm⟩
case tfae_5_to_6.mk.intro.w.hIN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ Submodule.span R {x} ≤ maximalIdeal R • maximalIdeal R
case tfae_5_to_6.mk.intro.w.hIN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ maximalIdeal R ≤ maximalIdeal R • maximalIdeal R
conv_lhs => rw [hx]
case tfae_5_to_6.mk.intro.w.hIN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : ↑x' ∈ maximalIdeal R • maximalIdeal R
⊢ Submodule.span R {x} ≤ maximalIdeal R • maximalIdeal R
case tfae_5_to_6.mk.intro.w.hIN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ Submodule.span R {x} ≤ maximalIdeal R • maximalIdeal R
rw [Submodule.mem_smul_top_iff] at e
no goals
case tfae_5_to_6.mk.intro.w.hIN
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : ↑x' ∈ maximalIdeal R • maximalIdeal R
⊢ Submodule.span R {x} ≤ maximalIdeal R • maximalIdeal R
rwa [Submodule.span_le, Set.singleton_subset_iff]
no goals
case tfae_5_to_6.mk.intro.w.hIjac
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
e : x' ∈ maximalIdeal R • ⊤
⊢ maximalIdeal R ≤ Ideal.jacobson ⊥
rw [LocalRing.jacobson_eq_maximalIdeal (⊥ : Ideal R) bot_ne_top]
case tfae_5_to_6.mk.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
y : { x // x ∈ maximalIdeal R }
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' y
case tfae_5_to_6.mk.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
⊢ ∀ (w : CotangentSpace R), ∃ c, c • Submodule.Quotient.mk x' = w
refine' fun w => Quotient.inductionOn' w fun y => _
case tfae_5_to_6.mk.intro.h.mk
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
y : R
hy : y ∈ maximalIdeal R
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' { val := y, property := hy }
case tfae_5_to_6.mk.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
y : { x // x ∈ maximalIdeal R }
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' y
obtain ⟨y, hy⟩ := y
case tfae_5_to_6.mk.intro.h.mk
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
y : R
hy✝ : y ∈ maximalIdeal R
hy : ∃ a, a • x = y
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' { val := y, property := hy✝ }
case tfae_5_to_6.mk.intro.h.mk
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
y : R
hy : y ∈ maximalIdeal R
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' { val := y, property := hy }
rw [hx, Submodule.mem_span_singleton] at hy
case tfae_5_to_6.mk.intro.h.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
a : R
hy : a • x ∈ maximalIdeal R
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' { val := a • x, property := hy }
case tfae_5_to_6.mk.intro.h.mk
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
y : R
hy✝ : y ∈ maximalIdeal R
hy : ∃ a, a • x = y
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' { val := y, property := hy✝ }
obtain ⟨a, rfl⟩ := hy
no goals
case tfae_5_to_6.mk.intro.h.mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
x : R
hx : maximalIdeal R = Submodule.span R {x}
this : x ∈ maximalIdeal R
x' : { x // x ∈ maximalIdeal R } := { val := x, property := this }
w : CotangentSpace R
a : R
hy : a • x ∈ maximalIdeal R
⊢ ∃ c, c • Submodule.Quotient.mk x' = Quotient.mk'' { val := a • x, property := hy }
exact ⟨Ideal.Quotient.mk _ a, rfl⟩
case tfae_6_to_5.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : CotangentSpace R
hx : x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • x = w
⊢ Submodule.IsPrincipal (maximalIdeal R)
case tfae_6_to_5
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
⊢ (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
rintro ⟨x, hx, hx'⟩
case tfae_6_to_5.intro.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Submodule.IsPrincipal (maximalIdeal R)
case tfae_6_to_5.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : CotangentSpace R
hx : x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • x = w
⊢ Submodule.IsPrincipal (maximalIdeal R)
induction x using Quotient.inductionOn' with | h x => ?_
case tfae_6_to_5.intro.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R = Submodule.span R {↑x}
case tfae_6_to_5.intro.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Submodule.IsPrincipal (maximalIdeal R)
use x
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R ≤ Submodule.span R {↑x}

case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Submodule.span R {↑x} ≤ maximalIdeal R
case tfae_6_to_5.intro.intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R = Submodule.span R {↑x}
apply le_antisymm
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Submodule.span R {↑x} ≤ maximalIdeal R

case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R ≤ Submodule.span R {↑x}

case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Submodule.span R {↑x} ≤ maximalIdeal R
swap
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
have h₂ : maximalIdeal R ≤ (⊥ : Ideal R).jacobson := by
  rw [LocalRing.jacobson_eq_maximalIdeal]
  exact bot_ne_top
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
this : Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R = Ideal.span {↑x} ⊔ ⊥ • maximalIdeal R
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
have :=
  Submodule.smul_sup_eq_smul_sup_of_le_smul_of_le_jacobson (IsNoetherian.noetherian _) h₂ h₁
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
this : Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R = Ideal.span {↑x}
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
this : Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R = Ideal.span {↑x} ⊔ ⊥ • maximalIdeal R
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
rw [Submodule.bot_smul, sup_bot_eq] at this
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
this : Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R = Ideal.span {↑x}
⊢ Submodule.span R {↑x} = Submodule.span R {↑x} ⊔ maximalIdeal R
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
this : Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R = Ideal.span {↑x}
⊢ maximalIdeal R ≤ Submodule.span R {↑x}
rw [← sup_eq_left, eq_comm]
no goals
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
h₂ : maximalIdeal R ≤ Ideal.jacobson ⊥
this : Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R = Ideal.span {↑x}
⊢ Submodule.span R {↑x} = Submodule.span R {↑x} ⊔ maximalIdeal R
exact le_sup_left.antisymm (h₁.trans <| le_of_eq this)
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ ↑x ∈ ↑(maximalIdeal R)
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Submodule.span R {↑x} ≤ maximalIdeal R
rw [Submodule.span_le, Set.singleton_subset_iff]
no goals
case tfae_6_to_5.intro.intro.h.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ ↑x ∈ ↑(maximalIdeal R)
exact x.prop
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
refine' sup_le le_sup_left _
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
⊢ m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
⊢ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
rintro m hm
case intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : ResidueField R
hc : c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
⊢ m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
obtain ⟨c, hc⟩ := hx' (Submodule.Quotient.mk ⟨m, hm⟩)
case intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
case intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : ResidueField R
hc : c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
induction c using Quotient.inductionOn' with | h c => ?_
case intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ c * ↑x - (c * ↑x - m) ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
case intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
rw [← sub_sub_cancel (c * x) m]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ c * ↑x ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R

R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ c * ↑x - m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
case intro.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ c * ↑x - (c * ↑x - m) ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
apply sub_mem _ _
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ c * ↑x ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
refine' Ideal.mem_sup_left (Ideal.mem_span_singleton'.mpr ⟨c, rfl⟩)
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
this : (fun x x_1 => x • x_1) c x - { val := m, property := hm } ∈ maximalIdeal R • ⊤
⊢ c * ↑x - m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
⊢ c * ↑x - m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
have := (Submodule.Quotient.eq _).mp hc
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
this : ↑((fun x x_1 => x • x_1) c x - { val := m, property := hm }) ∈ maximalIdeal R • maximalIdeal R
⊢ c * ↑x - m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
this : (fun x x_1 => x • x_1) c x - { val := m, property := hm } ∈ maximalIdeal R • ⊤
⊢ c * ↑x - m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
rw [Submodule.mem_smul_top_iff] at this
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
m : R
hm : m ∈ maximalIdeal R
c : R
hc : Quotient.mk'' c • Quotient.mk'' x = Submodule.Quotient.mk { val := m, property := hm }
this : ↑((fun x x_1 => x • x_1) c x - { val := m, property := hm }) ∈ maximalIdeal R • maximalIdeal R
⊢ c * ↑x - m ∈ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
exact Ideal.mem_sup_right this
case h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
⊢ ⊥ ≠ ⊤
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
⊢ maximalIdeal R ≤ Ideal.jacobson ⊥
rw [LocalRing.jacobson_eq_maximalIdeal]
no goals
case h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
x : { x // x ∈ maximalIdeal R }
hx : Quotient.mk'' x ≠ 0
hx' : ∀ (w : CotangentSpace R), ∃ c, c • Quotient.mk'' x = w
h₁ : Ideal.span {↑x} ⊔ maximalIdeal R ≤ Ideal.span {↑x} ⊔ maximalIdeal R • maximalIdeal R
⊢ ⊥ ≠ ⊤
exact bot_ne_top
no goals
case tfae_5_to_7
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
exact exists_maximalIdeal_pow_eq_of_principal R h
case tfae_7_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → IsTotal (Ideal R) fun x x_1 => x ≤ x_1
case tfae_7_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → ValuationRing R
rw [ValuationRing.iff_ideal_total]
case tfae_7_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
case tfae_7_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ (∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n) → IsTotal (Ideal R) fun x x_1 => x ≤ x_1
intro H
case tfae_7_to_2.total
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ ∀ (a b : Ideal R), a ≤ b ∨ b ≤ a
case tfae_7_to_2
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
constructor
case tfae_7_to_2.total
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
⊢ I ≤ J ∨ J ≤ I
case tfae_7_to_2.total
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
⊢ ∀ (a b : Ideal R), a ≤ b ∨ b ≤ a
intro I J
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : I = ⊥
⊢ I ≤ J ∨ J ≤ I

case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
⊢ I ≤ J ∨ J ≤ I
case tfae_7_to_2.total
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
⊢ I ≤ J ∨ J ≤ I
by_cases hI : I = ⊥
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
hJ : J = ⊥
⊢ I ≤ J ∨ J ≤ I

case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
hJ : ¬J = ⊥
⊢ I ≤ J ∨ J ≤ I
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
⊢ I ≤ J ∨ J ≤ I
by_cases hJ : J = ⊥
case neg.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
hJ : ¬J = ⊥
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
⊢ maximalIdeal R ^ n ≤ J ∨ J ≤ maximalIdeal R ^ n
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
hJ : ¬J = ⊥
⊢ I ≤ J ∨ J ≤ I
obtain ⟨n, rfl⟩ := H I hI
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m ∨ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
case neg.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
hJ : ¬J = ⊥
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
⊢ maximalIdeal R ^ n ≤ J ∨ J ≤ maximalIdeal R ^ n
obtain ⟨m, rfl⟩ := H J hJ
case neg.intro.intro.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : m ≤ n
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m ∨ maximalIdeal R ^ m ≤ maximalIdeal R ^ n

case neg.intro.intro.inr
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : n ≤ m
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m ∨ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m ∨ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
cases' le_total m n with h' h'
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
⊢ ⊥ ≤ J ∨ J ≤ ⊥
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : I = ⊥
⊢ I ≤ J ∨ J ≤ I
subst hI
case pos.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
⊢ ⊥ ≤ J
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
⊢ ⊥ ≤ J ∨ J ≤ ⊥
left
no goals
case pos.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
⊢ ⊥ ≤ J
exact bot_le
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I : Ideal R
hI : ¬I = ⊥
⊢ I ≤ ⊥ ∨ ⊥ ≤ I
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : ¬I = ⊥
hJ : J = ⊥
⊢ I ≤ J ∨ J ≤ I
subst hJ
case pos.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I : Ideal R
hI : ¬I = ⊥
⊢ ⊥ ≤ I
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I : Ideal R
hI : ¬I = ⊥
⊢ I ≤ ⊥ ∨ ⊥ ≤ I
right
no goals
case pos.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I : Ideal R
hI : ¬I = ⊥
⊢ ⊥ ≤ I
exact bot_le
case neg.intro.intro.inl.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : m ≤ n
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m
case neg.intro.intro.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : m ≤ n
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m ∨ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
left
no goals
case neg.intro.intro.inl.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : m ≤ n
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m
exact Ideal.pow_le_pow h'
case neg.intro.intro.inr.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : n ≤ m
⊢ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
case neg.intro.intro.inr
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : n ≤ m
⊢ maximalIdeal R ^ n ≤ maximalIdeal R ^ m ∨ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
right
no goals
case neg.intro.intro.inr.h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.224397
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
ne_bot : maximalIdeal R ≠ ⊥
tfae_1_to_2 : DiscreteValuationRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → DiscreteValuationRing R
tfae_1_to_4 : DiscreteValuationRing R → IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_6 : Submodule.IsPrincipal (maximalIdeal R) → ∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w
tfae_6_to_5 : (∃ v _n, ∀ (w : CotangentSpace R), ∃ c, c • v = w) → Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
n : ℕ
hI : ¬maximalIdeal R ^ n = ⊥
m : ℕ
hJ : ¬maximalIdeal R ^ m = ⊥
h' : n ≤ m
⊢ maximalIdeal R ^ m ≤ maximalIdeal R ^ n
exact Ideal.pow_le_pow h'