OAI/Algebra/Finitistic/Localization/ConcreteTensorEvaluation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ConcreteTensorEvaluation.idealEquiv line 15

   Source documentation

   Match the opposite-regular presentation of eB to the fixed-point presentation.

   def idealEquiv (e : B P) (he : e*e=e) :
       VertexProjectives.ideal e ≃ₗ[(B P)ᵐᵒᵖ] IdempotentTensor.rightIdeal e where
   …

   Mentions: OAI.LittleFinitistic.VertexProjectives.ideal, OAI.LittleFinitistic.IdempotentTensor.rightIdeal

2. def OAI.LittleFinitistic.ConcreteTensorEvaluation.tensorCongr line 35

   Source documentation

   Balanced tensor respects actual right-module equivalences.

   def tensorCongr (e : M ≃ₗ[Aᵐᵒᵖ] M') :
       BalancedTensor.Tensor k A M N ≃ₗ[k] BalancedTensor.Tensor k A M' N where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

3. abbrev OAI.LittleFinitistic.ConcreteTensorEvaluation.moduleEvaluation line 60

   Source documentation

   Actual tensor evaluation on projectives.

   abbrev moduleEvaluation : SourceVerdier.Proj P ⥤ ModuleCat.{u} k :=
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.Proj

4. instance OAI.LittleFinitistic.ConcreteTensorEvaluation.vertexScalarTower line 64
5. def OAI.LittleFinitistic.ConcreteTensorEvaluation.vertexIso line 69

   Source documentation

   The exact natural vertex identification E_i tensor_B M(Y) = Y.

   def vertexIso (i : Fin 3) : (moduleEvaluation X).obj (SourceVerdier.E P i) ≅ ModuleCat.of k Y :=
   …

   Mentions: OAI.LittleFinitistic.ConcreteTensorEvaluation.moduleEvaluation, OAI.LittleFinitistic.SourceVerdier.E

6. theorem OAI.LittleFinitistic.ConcreteTensorEvaluation.vertexIso_mk line 78
7. theorem OAI.LittleFinitistic.ConcreteTensorEvaluation.s_naturality line 84

   Source documentation

   The two actual identity-arrow tensor maps become identities on Y.

   theorem s_naturality :
       (moduleEvaluation X).map (SourceVerdier.arrow01 P 0) ≫ (vertexIso X 1).hom =
         (vertexIso X 0).hom := by
   …

   Mentions: OAI.LittleFinitistic.ConcreteTensorEvaluation.moduleEvaluation, OAI.LittleFinitistic.SourceVerdier.arrow01, OAI.LittleFinitistic.ConcreteTensorEvaluation.vertexIso

8. theorem OAI.LittleFinitistic.ConcreteTensorEvaluation.s'_naturality line 95
9. instance OAI.LittleFinitistic.ConcreteTensorEvaluation.s_inverted line 106
10. instance OAI.LittleFinitistic.ConcreteTensorEvaluation.s'_inverted line 112