instDirectedSystemCoeLinearMapIdRTensor

English

The family of maps G_i → G_j along i ≤ j induces a directed system on the tensor products with M.

Русский

Пусть система отображений G_i → G_j порождает направленную систему на тензорные произведения с M.

LaTeX

$$DirectedSystem (G · ⊗_R M) (f ▷ M)$$

Lean4

instance : DirectedSystem (G · ⊗[R] M) (f ▷ M)
    where
  map_self i x := by convert LinearMap.rTensor_id_apply M (G i) x; ext; apply DirectedSystem.map_self'
  map_map _ _ _ _ _ x := by convert ← (LinearMap.rTensor_comp_apply M _ _ x).symm; ext; apply DirectedSystem.map_map' f

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