OAI/Algebra/Finitistic/Ordinary/OrdinaryOffDiagonalMaps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.map line 14

   Source documentation

   Actual component maps of the off-diagonal right product-ring module.

   def map (f : O →ₗ[Lᵐᵒᵖ] O') (g : T →ₗ[Rᵐᵒᵖ] T') :
       OffDiagonal O T →ₗ[(L × R)ᵐᵒᵖ] OffDiagonal O' T' where
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal

2. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.map_left line 22

   Source documentation

   The same map retains the two prescribed left product-ring actions.

   theorem map_left (f : O →ₗ[Lᵐᵒᵖ] O') (hf : ∀ (r : R) x, f (r • x) = r • f x)
       (g : T →ₗ[Rᵐᵒᵖ] T') (hg : ∀ (s : L) x, g (s • x) = s • g x)
       (d : L × R) (x : OffDiagonal O T) :
       map f g (d • x) = d • map f g x :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal, OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.map