English
If P ≤ M, Q ≤ N, S ≤ O, and e, f are linear equivalences with appropriate maps, then the composed quotient equivalence equals the composition of the two quotient equivalences.
Русский
Если P ≤ M, Q ≤ N, S ≤ O, и имеются линейные эквивалентности e, f с подходящими отображениями, то эквивалентность фактор‑модуля по составному отображению равна композиции двух факторных эквивалентностей.
LaTeX
$$$$ \\text{Quotient.equiv}(P, S, e.trans f) = \\text{Quotient.equiv}(P, Q, e) .\\text{trans} \\text{ Quotient.equiv}(Q, S, f). $$$$
Lean4
@[simp]
theorem equiv_trans {N O : Type*} [AddCommGroup N] [Module R N] [AddCommGroup O] [Module R O] (P : Submodule R M)
(Q : Submodule R N) (S : Submodule R O) (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] O) (he : P.map e = Q) (hf : Q.map f = S)
(hef : P.map (e.trans f) = S) :
Quotient.equiv P S (e.trans f) hef = (Quotient.equiv P Q e he).trans (Quotient.equiv Q S f hf) :=
by
ext
-- `simp` can deal with `hef` depending on `e` and `f`
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]
-- `rw` can deal with `mapQ_comp` needing extra hypotheses coming from the RHS
rw [mapQ_comp, LinearMap.comp_apply]
