hasProjectiveDimensionLT_X₃ — Mathlib

English

In a short exact sequence S, if X₁ has pdLT n and X₂ has pdLT (n+1), then X₃ has pdLT (n+1).

Русский

В короткой точной последовательности S, если X₁ имеет pdLT n, а X₂ — pdLT (n+1), то X₃ имеет pdLT (n+1).

LaTeX

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

Lean4

theorem hasProjectiveDimensionLT_X₃ (h₁ : HasProjectiveDimensionLT S.X₁ n)
    (h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)) : HasProjectiveDimensionLT S.X₃ (n + 1) :=
  by
  letI := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  rintro (_ | i) hi Y x₃
  · simp at hi
  · obtain ⟨x₁, rfl⟩ :=
      Ext.contravariant_sequence_exact₃ hS _ x₃ (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) hi) (add_comm _ _)
    rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by cutsat), Ext.comp_zero]

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