rankAtStalk_eq_zero_iff_subsingleton

English

Assume flat and finite; rankAtStalk M = 0 if and only if M is subsingleton.

Русский

Пусть M плоско и конечно; rankAtStalk M = 0 тогда и только тогда, когда M — подсистема (subsingleton).

LaTeX

$$$\\operatorname{rankAtStalk}(M) = 0 \\iff \\operatorname{Subsingleton} M$$$

Lean4

theorem rankAtStalk_eq_zero_iff_subsingleton : rankAtStalk (R := R) M = 0 ↔ Subsingleton M :=
  by
  refine ⟨fun h ↦ ?_, fun _ ↦ rankAtStalk_eq_zero_of_subsingleton⟩
  simp_rw [← support_eq_empty_iff (R := R), Set.eq_empty_iff_forall_notMem]
  intro p
  rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]

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