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.

Русский

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

LaTeX

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

Lean4

theorem hasProjectiveDimensionLT_X₁ (h₂ : HasProjectiveDimensionLT S.X₂ n)
    (h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)) : 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₁ (add_comm _ _)
      (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) (by cutsat))
  rw [x₂.eq_zero_of_hasProjectiveDimensionLT n (by cutsat), Ext.comp_zero]

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