injectiveDimension_eq_of_iso — Mathlib

English

If X ≅ Y, then the injective dimension of X equals that of Y.

Русский

Если X изоморфно Y, то инъективная размерность X равна инъективной размерности Y.

LaTeX

$$$X \cong Y \Rightarrow \operatorname{injectiveDimension}(X) = \operatorname{injectiveDimension}(Y)$$$

Lean4

theorem injectiveDimension_eq_of_iso {X Y : C} (e : X ≅ Y) : injectiveDimension X = injectiveDimension Y :=
  by
  simp only [injectiveDimension]
  congr! 5
  exact ⟨fun h ↦ hasInjectiveDimensionLT_of_iso e _, fun h ↦ hasInjectiveDimensionLT_of_iso e.symm _⟩

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