linear_of_iso — Mathlib

English

If F and G are isomorphic functors and F is R-linear, then G inherits an R-linear structure; in particular, the linear structure on G is obtained by transporting F’s linearity along the isomorphism.

Русский

Если существуют изоморфизмы между функтороми F и G и F является R-линейным, то G наследует R-линейную структуру; линейность G переносится вдоль изоморфизма.

LaTeX

$$$\\text{If } e: F \\cong G \\text{ with } [F\\text{ Linear }R],\\ \\, G \\text{ is } R\\text{-linear with linear structure transported along } e.$$$

Lean4

theorem linear_of_iso {G : C ⥤ D} (e : F ≅ G) [F.Linear R] : G.Linear R := by
  exact
    {
      map_smul := fun f r => by
        simp only [← NatIso.naturality_1 e (r • f), F.map_smul, Linear.smul_comp, NatTrans.naturality, Linear.comp_smul,
          Iso.inv_hom_id_app_assoc] }

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