hasInjectiveDimensionLT — Mathlib

English

If X is a retract of Y and HasInjectiveDimensionLT Y n, then HasInjectiveDimensionLT X n.

Русский

Если X является retract Y и HasInjectiveDimensionLT Y n, тогда HasInjectiveDimensionLT X n.

LaTeX

$$$\text{Retract}(X,Y) \Rightarrow (\text{HasInjectiveDimensionLT}(Y,n) \Rightarrow \text{HasInjectiveDimensionLT}(X,n))$$$

Lean4

theorem hasInjectiveDimensionLT {X Y : C} (h : Retract X Y) (n : ℕ) [HasInjectiveDimensionLT Y n] :
    HasInjectiveDimensionLT X n := by
  letI := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi T x
  rw [← x.comp_mk₀_id, ← h.retract, ← Ext.mk₀_comp_mk₀, ← Ext.comp_assoc_of_second_deg_zero,
    (x.comp (Ext.mk₀ h.i) (add_zero i)).eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

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