quotEquivOfEquiv — Mathlib

English

Given isomorphic subspaces p, q of V and V₂, if p ≃ q, then the quotients V/p and V₂/q are isomorphic.

Русский

Если подпространства p и q из V и V₂ изоморфны, то их факторпространства V/p и V₂/q изоморфны.

LaTeX

$$If p ≃ q and V ≃ V₂, then (V ⧸ p) ≃ (V₂ ⧸ q)$$

Lean4

/-- Given isomorphic subspaces `p q` of vector spaces `V` and `V₁` respectively,
  `p.quotient` is isomorphic to `q.quotient`. -/
noncomputable def quotEquivOfEquiv {p : Subspace K V} {q : Subspace K V₂} (f₁ : p ≃ₗ[K] q) (f₂ : V ≃ₗ[K] V₂) :
    (V ⧸ p) ≃ₗ[K] V₂ ⧸ q :=
  LinearEquiv.ofFinrankEq _ _
    (by
      rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank, LinearEquiv.finrank_eq f₂])
      -- TODO: generalize to the case where one of `p` and `q` is finite-dimensional.

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