hasProjectiveDimensionLT_of_iso — Mathlib

English

Let X and X′ be objects in an Abelian category that are isomorphic. If X has projective dimension less than n, then X′ also has projective dimension less than n.

Русский

Пусть X и X′ — объекты абелевой категории и изоморфны. Если проективная размерность X менее n, то и для X′ она менее n.

LaTeX

$$$\forall {\mathcal C}$ [Category(\mathcal C)] [Abelian(\mathcal C)] \{X, X' : \mathcal C\} (e : X \cong X') (n : \mathbb{N})\ [HasProjectiveDimensionLT(X, n)] \Rightarrow HasProjectiveDimensionLT(X', n)$$

Lean4

theorem hasProjectiveDimensionLT_of_iso {X X' : C} (e : X ≅ X') (n : ℕ) [HasProjectiveDimensionLT X n] :
    HasProjectiveDimensionLT X' n :=
  e.symm.retract.hasProjectiveDimensionLT n

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