OAI/Algebra/Finitistic/Rectification/CornerSpaces.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.CornerSpaces.corner line 17

   Source documentation

   The actual two-sided corner e_i B e_j as a vector subspace.

   def corner (i j : Fin 3) : Submodule k (ThreeVertexAlgebra μ) where
   …

   Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra

2. def OAI.LittleFinitistic.CornerSpaces.corner10Equiv line 34
3. def OAI.LittleFinitistic.CornerSpaces.corner21Equiv line 48
4. def OAI.LittleFinitistic.CornerSpaces.corner20Equiv line 62
5. def OAI.LittleFinitistic.CornerSpaces.diagonalEquiv line 77

   Source documentation

   A diagonal corner has only its scalar trivial path.

   noncomputable def diagonalEquiv (i : Fin 3) : corner μ i i ≃ₗ[k] k where
   …

   Mentions: OAI.LittleFinitistic.CornerSpaces.corner

6. theorem OAI.LittleFinitistic.CornerSpaces.corner_zero_of_lt line 95

   Source documentation

   No path points backwards in the actual algebra.

   theorem corner_zero_of_lt (i j : Fin 3) (hij : i < j) (x : corner μ i j) : x = 0 := by
   …

   Mentions: OAI.LittleFinitistic.CornerSpaces.corner