hasProjectiveDimensionLT_X₂ — Mathlib

English

In a short exact sequence S, if the outer terms X₁ and X₃ have projective dimension less than n, then the middle term X₂ also has projective dimension less than n.

Русский

В короткой точной последовательности S, если X₁ и X₃ имеют проективную размерность < n, то и X₂ имеет её < n.

LaTeX

$$$\forall {S : ShortComplex C}, S.ShortExact \Rightarrow \forall n \in \mathbb{N}, HasProjectiveDimensionLT(S.X_1, n) \rightarrow HasProjectiveDimensionLT(S.X_3, n) \rightarrow HasProjectiveDimensionLT(S.X_2, n)$$$

Lean4

theorem hasProjectiveDimensionLT_X₂ (h₁ : HasProjectiveDimensionLT S.X₁ n) (h₃ : HasProjectiveDimensionLT S.X₃ n) :
    HasProjectiveDimensionLT S.X₂ n := by
  letI := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  intro i hi Y x₂
  obtain ⟨x₃, rfl⟩ := Ext.contravariant_sequence_exact₂ hS _ x₂ (Ext.eq_zero_of_hasProjectiveDimensionLT _ n hi)
  rw [x₃.eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]

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