hasInjectiveDimensionLT_X₂ — Mathlib

English

In a short exact sequence 0 → X1 → X2 → X3 → 0, if X1 and X3 have HasInjectiveDimensionLT at n, then X2 has HasInjectiveDimensionLT at n.

Русский

В коротком точном разделе 0→X1→X2→X3→0, если X1 и X3 имеют HasInjectiveDimensionLT при n, то X2 имеет HasInjectiveDimensionLT при n.

LaTeX

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

Lean4

theorem hasInjectiveDimensionLT_X₂ (h₁ : HasInjectiveDimensionLT S.X₁ n) (h₃ : HasInjectiveDimensionLT S.X₃ n) :
    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₂ (Ext.eq_zero_of_hasInjectiveDimensionLT _ n hi)
  rw [x₃.eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

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