conj_exact_iff_exact — Mathlib

English

If e: N ≃ N' is a linear equivalence, then Exact(f,k) holds for the transformed pair (e ∘ f, g ∘ e^{-1}) if and only if Exact(f,g) holds.

Русский

Если e: N ≃ N' — линейное равенство, то точность сохраняется при переходе к пары (e ∘ f, g ∘ e^{-1}).

LaTeX

$$$$ \\operatorname{Exact}(e \\circ f, g \\circ e^{-1}) \\iff \\operatorname{Exact}(f, g). $$$$

Lean4

theorem conj_exact_iff_exact (e : N ≃ₗ[R] N') : Function.Exact (e ∘ₗ f) (g ∘ₗ (e.symm : N' →ₗ[R] N)) ↔ Exact f g :=
  by
  simp_rw [LinearMap.exact_iff, LinearMap.ker_comp, ← Submodule.map_equiv_eq_comap_symm, LinearMap.range_comp]
  exact (Submodule.map_injective_of_injective e.injective).eq_iff

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