hasProjectiveDimensionLT — Mathlib

English

If X is a retract of Y and Y has HasProjectiveDimensionLT n, then X also has HasProjectiveDimensionLT n.

Русский

Если X является отобразимым через retract из Y, и Y имеет HasProjectiveDimensionLT n, то и X имеет HasProjectiveDimensionLT n.

LaTeX

$$$ (\text{Retract } X Y) \Rightarrow [\text{HasProjectiveDimensionLT } Y n] \Rightarrow [\text{HasProjectiveDimensionLT } X n]. $$$

Lean4

theorem hasProjectiveDimensionLT {X Y : C} (h : Retract X Y) (n : ℕ) [HasProjectiveDimensionLT Y n] :
    HasProjectiveDimensionLT X n := by
  letI := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  intro i hi T x
  rw [← x.mk₀_id_comp, ← h.retract, ← Ext.mk₀_comp_mk₀, Ext.comp_assoc_of_second_deg_zero,
    ((Ext.mk₀ h.r).comp x (zero_add i)).eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]

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