projectiveDimension_le — Mathlib

English

If X retracts from Y in an Abelian category, then the projective dimension of X is bounded above by that of Y.

Русский

Если X есть ретракт Y в абелевой категории, то pd(X) ≤ pd(Y).

LaTeX

$$$\forall h:\Retract X Y,\operatorname{projectiveDimension} X \le \operatorname{projectiveDimension} Y$$$

Lean4

theorem projectiveDimension_le {X Y : C} (h : Retract X Y) : projectiveDimension X ≤ projectiveDimension Y :=
  sInf_le_sInf_of_subset_insert_top
    (fun n hn ↦
      by
      simp only [Set.mem_setOf_eq, not_top_lt, IsEmpty.forall_iff, implies_true, Set.insert_eq_of_mem] at hn ⊢
      intro i hi
      have := hn i hi
      exact h.hasProjectiveDimensionLT i)

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