OAI/Algebra/Finitistic/Selected/SelectedTensorComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedTensorComparison.tensor line 14
2. def OAI.LittleFinitistic.SelectedTensorComparison.homotopyIso line 19

   Source documentation

   The chosen representative's actual tensor is the source evaluation object.

   def homotopyIso (D : SourceVerdier.K P) :
       (HomotopyCategory.quotient _ _).obj (tensor X D) ≅ (SourceEvaluation.evaluation X).obj D :=
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.K, OAI.LittleFinitistic.SelectedTensorComparison.tensor, OAI.LittleFinitistic.SourceEvaluation.evaluation

3. def OAI.LittleFinitistic.SelectedTensorComparison.finiteIso line 24
4. abbrev OAI.LittleFinitistic.SelectedTensorComparison.tensorMap line 28
5. lemma OAI.LittleFinitistic.SelectedTensorComparison.map_comparison line 34