free_shortExact — Mathlib

English

If X1 and X3 in a short exact sequence are free, then X2 is free.

Русский

Если X1 и X3 в короткой точной последовательности свободны, тогда и X2 свободен.

LaTeX

$$$\text{Module.Free } R S.X_1 \quad \land \quad \text{Module.Free } R S.X_3 \Rightarrow \text{Module.Free } R S.X_2$$$

Lean4

/-- In a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, if `X₁` and `X₃` are free,
then `X₂` is free. -/
theorem free_shortExact [Module.Free R S.X₁] [Module.Free R S.X₃] : Module.Free R S.X₂ :=
  Module.Free.of_basis (Basis.ofShortExact hS' (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))

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