OAI/Algebra/Finitistic/Selected/SelectedOrdinaryAlgebra.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SelectedOrdinaryAlgebra.a line 14

   Source documentation

   A fixed support interval containing degree zero, chosen before any test module.

   def a : ℤ := min (SelectedWindow.lo-2) 0

   Mentions: OAI.LittleFinitistic.SelectedWindow.lo

2. def OAI.LittleFinitistic.SelectedOrdinaryAlgebra.b line 15
3. def OAI.LittleFinitistic.SelectedOrdinaryAlgebra.length line 16
4. theorem OAI.LittleFinitistic.SelectedOrdinaryAlgebra.a_le_zero line 18
5. theorem OAI.LittleFinitistic.SelectedOrdinaryAlgebra.b_nonneg line 19
6. theorem OAI.LittleFinitistic.SelectedOrdinaryAlgebra.endpoints line 20
7. theorem OAI.LittleFinitistic.SelectedOrdinaryAlgebra.support line 26
8. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.term_finite line 32
9. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.term_projective line 35
10. abbrev OAI.LittleFinitistic.SelectedOrdinaryAlgebra.D line 42

    Source documentation

    The actual finite-dimensional ordinary algebra and off-diagonal bimodule.

    abbrev D := AlgebraD ℂ length (B P)

    Mentions: OAI.LittleFinitistic.SelectedOrdinaryAlgebra.length

11. abbrev OAI.LittleFinitistic.SelectedOrdinaryAlgebra.O line 43
12. abbrev OAI.LittleFinitistic.SelectedOrdinaryAlgebra.X line 44
13. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.base_finite line 45
14. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.D_finite line 46
15. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.O_finite line 47
16. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.X_finite line 48
17. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.O_right_projective line 49
18. abbrev OAI.LittleFinitistic.SelectedOrdinaryAlgebra.A line 54

    Source documentation

    The manuscript's one fixed square-zero algebra. No projective-dimension conclusion is asserted here.

    abbrev A := TrivSqZeroExt D X

    Mentions: OAI.LittleFinitistic.SelectedOrdinaryAlgebra.D, OAI.LittleFinitistic.SelectedOrdinaryAlgebra.X

19. abbrev OAI.LittleFinitistic.SelectedOrdinaryAlgebra.augmentation line 55
20. instance OAI.LittleFinitistic.SelectedOrdinaryAlgebra.A_finite line 57