hasInjectiveDimensionLT_X₁ — Mathlib

English

In a short exact sequence S with X3 LT n and X2 LT n+1, then X1 LT n+1.

Русский

В последовательности S: если X3 имеет LT n, а X2 LT n+1, то X1 имеет LT n+1.

LaTeX

$$$S.ShortExact \Rightarrow (\text{HasInjectiveDimensionLT}(S.X_3,n) \land \text{HasInjectiveDimensionLT}(S.X_2,n+1)) \Rightarrow \text{HasInjectiveDimensionLT}(S.X_1,n+1)$$$

Lean4

theorem hasInjectiveDimensionLT_X₁ (h₁ : HasInjectiveDimensionLT S.X₃ n) (h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)) :
    HasInjectiveDimensionLT S.X₁ (n + 1) := by
  letI := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  rintro (_ | i) hi Y x₃
  · simp at hi
  · obtain ⟨x₁, rfl⟩ := Ext.covariant_sequence_exact₁ _ hS x₃ (Ext.eq_zero_of_hasInjectiveDimensionLT _ (n + 1) hi) rfl
    rw [x₁.eq_zero_of_hasInjectiveDimensionLT n (by cutsat), Ext.zero_comp]

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