English
Under strong rank condition, rank(X2) = rank(X1) + rank(X3) for a short exact sequence with X1, X3 free.
Русский
При условии сильного базового ранга, ранги равны: rank(X2) = rank(X1) + rank(X3).
LaTeX
$$$\text{Module.rank } R S.X_2 = \text{Module.rank } R S.X_1 + \text{Module.rank } R S.X_3$$$
Lean4
theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃] [StrongRankCondition R] :
Module.rank R S.X₂ = Module.rank R S.X₁ + Module.rank R S.X₃ :=
by
haveI := free_shortExact hS'
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,
Module.Free.rank_eq_card_chooseBasisIndex R S.X₃, Cardinal.add_def, Cardinal.eq]
exact
⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂)
(Basis.ofShortExact hS' (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩
