VertexFunctor.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.VertexFunctor.restricted line 14
def OAI.LittleFinitistic.VertexFunctor.action line 17
Source documentation
The original vertex action is linear for the commuting right restriction.
```
def action (M : ModuleCat.{u} A) : restricted β M →ₗ[B] restricted β M where
…
```
Mentions: OAI.LittleFinitistic.VertexFunctor.restricted
def OAI.LittleFinitistic.VertexFunctor.fixed line 24
theorem OAI.LittleFinitistic.VertexFunctor.mem_fixed line 27
def OAI.LittleFinitistic.VertexFunctor.projection line 32
Source documentation
The genuine projection onto the vertex component.
```
def projection (M : ModuleCat.{u} A) : restricted β M →ₗ[B] fixed β e hc M :=
…
```
Mentions: OAI.LittleFinitistic.VertexFunctor.restricted, OAI.LittleFinitistic.VertexFunctor.fixed
def OAI.LittleFinitistic.VertexFunctor.inclusion line 39
theorem OAI.LittleFinitistic.VertexFunctor.projection_inclusion line 42
def OAI.LittleFinitistic.VertexFunctor.map line 50
Source documentation
Module maps restrict to the actual vertex fixed submodules.
```
def map {M N : ModuleCat.{u} A} (f : M ⟶ N) :
    fixed β e hc M →ₗ[B] fixed β e hc N where
…
```
Mentions: OAI.LittleFinitistic.VertexFunctor.fixed
def OAI.LittleFinitistic.VertexFunctor.functor line 63
Source documentation
The actual vertex-component functor; it retains the original right action.
```
def functor : ModuleCat.{u} A ⥤ ModuleCat.{u} B where
…
```
instance OAI.LittleFinitistic.VertexFunctor.additive line 77
theorem OAI.LittleFinitistic.VertexFunctor.projective line 87
Source documentation
Vertex components of right-projective modules are right-projective.
```
theorem projective (M : ModuleCat.{u} A) [Module.Projective B (restricted β M)] :
    Module.Projective B (fixed β e hc M) := by
…
```
Mentions: OAI.LittleFinitistic.VertexFunctor.restricted, OAI.LittleFinitistic.VertexFunctor.fixed
theorem OAI.LittleFinitistic.VertexFunctor.map_shortExact line 94
Source documentation
Applying a vertex component preserves actual short exact sequences.
```
theorem map_shortExact (S : ShortComplex (ModuleCat.{u} A)) (hS : S.ShortExact) :
    (S.map (functor β e hc)).ShortExact := by
…
```
Mentions: OAI.LittleFinitistic.VertexFunctor.functor