finrank_CotangentSpace_eq_one_iff

English

For a Noetherian local domain R, finrank of the cotangent space equals 1 if and only if R is a discrete valuation ring.

Русский

Для локального Noetherian кольца R r, размерность cotangent пространства равна 1 тогда и только тогда, когда R является дискретным оценочным кольцом.

LaTeX

$$finrank(ResidueField(R))(CotangentSpace(R)) = 1 \\iff IsDiscreteValuationRing(R)$$

Lean4

theorem finrank_CotangentSpace_eq_one_iff [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] :
    finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R :=
  by
  by_cases hR : IsField R
  · letI := hR.toField
    simp only [finrank_cotangentSpace_eq_zero, zero_ne_one, false_iff]
    exact fun h ↦ h.3 maximalIdeal_eq_bot
  · exact (IsDiscreteValuationRing.TFAE R hR).out 5 0

Похожие утверждения