English
Over a Noetherian ring, finiteness of the cotangent space degree is bounded by 1 precisely when the maximal ideal is principal.
Русский
При Noetherian кольце finrank котантантного пространства не превышает единицы тогда и только тогда, когда максимальная идеальная является главной.
LaTeX
$$finrank (ResidueField R) (CotangentSpace R) ≤ 1 \iff (maximalIdeal R).IsPrincipal$$
Lean4
theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] :
finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ (maximalIdeal R).IsPrincipal :=
by
rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff, (maximalIdeal R).toCotangent_surjective.exists,
isPrincipal_iff]
simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff, ←
(map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton, Submodule.map_top,
range_subtype, eq_comm (a := maximalIdeal R)]
exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩
