instDirectedSystemCoeLinearMapIdLTensor

English

The lTensor maps along i ≤ j form a directed system on M ⊗ G_i.

Русский

Отображения lTensor вдоль i ≤ j образуют направленную систему на M ⊗ G_i.

LaTeX

$$DirectedSystem (fun x => TensorProduct R M (G x)) (f i j h)$$

Lean4

instance : DirectedSystem (M ⊗[R] G ·) (M ◁ f)
    where
  map_self i x := by convert LinearMap.lTensor_id_apply M _ x; ext; apply DirectedSystem.map_self'
  map_map _ _ _ h₁ h₂
    x := by convert ← (LinearMap.lTensor_comp_apply M _ _ x).symm; ext; apply DirectedSystem.map_map' f

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