inverseLinear — Mathlib

English

If G is isomorphic to F and F is linear, then G inherits a linear structure; the inverse functor respects scalar multiplication.

Русский

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

LaTeX

$$$\\text{If } F \\cong G \\text{ and } F \\text{ is } R\\text{-linear, then } G \\text{ is } R\\text{-linear.}$$$

Lean4

instance inverseLinear (e : C ≌ D) [e.functor.Linear R] : e.inverse.Linear R where
  map_smul r
    f := by
    apply e.functor.map_injective
    simp

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