English
Under stronger assumptions, the bottom subalgebra has rank equal to 1.
Русский
При более строгих предположениях нижняя подалгебра имеет ранг 1.
LaTeX
$$$\operatorname{Module.rank}_F(\bot_{\text{Subalgebra}}) = 1$$$
Lean4
/-- This is mostly an auxiliary lemma for `Submodule.rank_sup_add_rank_inf_eq`. -/
theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂) (ce : V₁ →ₗ[K] V₃)
(hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb) (hgd : ker cd = ⊥) (eq : db.comp cd = eb.comp ce)
(eq₂ : ∀ d e, db d = eb e → ∃ c, cd c = d ∧ ce c = e) :
Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃ :=
by
have hf : Surjective (coprod db eb) := by rwa [← range_eq_top, range_coprod, eq_top_iff]
conv =>
rhs
rw [← rank_prod', rank_eq_of_surjective hf]
congr 1
apply LinearEquiv.rank_eq
let L : V₁ →ₗ[K] ker (coprod db eb) :=
LinearMap.codRestrict _ (prod cd (-ce)) <| by simpa [add_eq_zero_iff_eq_neg] using LinearMap.ext_iff.1 eq
refine LinearEquiv.ofBijective L ⟨?_, ?_⟩
· rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
· rw [← range_eq_top, eq_top_iff, range_codRestrict, ← map_le_iff_le_comap, Submodule.map_top, range_subtype]
rintro ⟨d, e⟩
have h := eq₂ d (-e)
simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker, Prod.mk_inj, coprod_apply, map_neg, neg_apply,
LinearMap.mem_range, Pi.prod] at h ⊢
grind
