OAI/Algebra/Finitistic/Ordinary/OrdinaryRetainedCongruence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.RetainedBimodule.congr line 16

   Source documentation

   An actual right-linear, left-equivariant equivalence retains both actions.

   def congr (f : M ≃ₗ[Aᵐᵒᵖ] N) (hf : ∀ (s : S) x, f (s • x) = s • f x) :
       RetainedBimodule k S A M ≃ₗ[S ⊗[k] Aᵐᵒᵖ] RetainedBimodule k S A N where
   …

   Mentions: OAI.LittleFinitistic.RetainedBimodule

2. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.congr line 29