subsingleton — Mathlib

English

If HasProjectiveDimensionLT X n holds, then for all i ≥ n and all Y, Ext^i(X,Y) is a subsingleton.

Русский

Если HasProjectiveDimensionLT X n выполнено, то для всех i ≥ n и для всех Y Ext^i(X,Y) образует подмножество с одним элементом.

LaTeX

$$$ \text{If } [\text{HasProjectiveDimensionLT } X n], \forall i \ge n, \forall Y, \operatorname{Subsingleton}(\operatorname{Ext}^i(X,Y)). $$$

Lean4

theorem subsingleton [hX : HasProjectiveDimensionLT X n] (i : ℕ) (hi : n ≤ i) (Y : C) : Subsingleton (Ext.{w} X Y i) :=
  by
  letI := HasExt.standard C
  have := hX.subsingleton' i hi
  exact Ext.chgUniv.{w, max u v}.symm.subsingleton

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