hasInjectiveDimensionLT_X₃ — Mathlib

English

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

Русский

В короткой точной последовательности, если X2 LT n, а X1 LT n+1, то X3 LT n.

LaTeX

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

Lean4

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

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