ArrowVertex.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExternalTensor.Section4.ArrowVertex.left line 13
Source documentation
Left multiplication on a bimodule, regarded as a right-linear map.
```
def left (a : B) (N : ModuleCat.{u} (Enveloping k B)) :
    (forgetRight k B).obj N →ₗ[Bᵐᵒᵖ] (forgetRight k B).obj N where
…
```
Mentions: OAI.ExternalTensor.Section4.Enveloping, OAI.ExternalTensor.Section4.forgetRight
theorem OAI.ExternalTensor.Section4.ArrowVertex.left_mul line 23
theorem OAI.ExternalTensor.Section4.ArrowVertex.map_left line 30
def OAI.ExternalTensor.Section4.ArrowVertex.space line 36
Source documentation
The actual fixed submodule eN, for an idempotent e.
```
def space (e : B) (N : ModuleCat.{u} (Enveloping k B)) :
    Submodule Bᵐᵒᵖ ((forgetRight k B).obj N) :=
…
```
Mentions: OAI.ExternalTensor.Section4.Enveloping, OAI.ExternalTensor.Section4.forgetRight
theorem OAI.ExternalTensor.Section4.ArrowVertex.mem_space line 40
theorem OAI.ExternalTensor.Section4.ArrowVertex.space_eq_range line 45
Source documentation
For idempotents the fixed submodule is exactly the image eN.
```
theorem space_eq_range (e : B) (he : e * e = e)
    (N : ModuleCat.{u} (Enveloping k B)) :
    space k B e N = (left k B e N).range := by
…
```
Mentions: OAI.ExternalTensor.Section4.Enveloping, OAI.ExternalTensor.Section4.ArrowVertex.space, OAI.ExternalTensor.Section4.ArrowVertex.left
def OAI.ExternalTensor.Section4.ArrowVertex.vertex line 57
Source documentation
Vertex restriction retains the original elements, rather than chosen coordinates.
```
def vertex (e : B) : ModuleCat.{u} (Enveloping k B) ⥤ ModuleCat.{u} Bᵐᵒᵖ where
…
```
Mentions: OAI.ExternalTensor.Section4.Enveloping
instance OAI.ExternalTensor.Section4.ArrowVertex.vertex_additive line 66
abbrev OAI.ExternalTensor.Section4.ArrowVertex.vertexComplex line 69
def OAI.ExternalTensor.Section4.ArrowVertex.arrow line 73
Source documentation
The intervertex map is precisely left multiplication by a.
```
def arrow (ei ej a : B) (hja : ej * a = a) : vertex k B ei ⟶ vertex k B ej where
…
```
Mentions: OAI.ExternalTensor.Section4.ArrowVertex.vertex
abbrev OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex line 81
theorem OAI.ExternalTensor.Section4.ArrowVertex.arrow_original line 85

theorem OAI.ExternalTensor.Section4.ArrowVertex.arrow_comp line 91

Source documentation

Composition uses multiplication in B in the original arrow order.

@[reassoc] theorem arrow_comp (ei ej el a b : B) (hja : ej * a = a)
    (hlb : el * b = b) (hlba : el * (b * a) = b * a) (P : BiComplex k B) :
    arrowComplex k B ei ej a hja P ≫ arrowComplex k B ej el b hlb P =
      arrowComplex k B ei el (b * a) hlba P := by
…

Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex

theorem OAI.ExternalTensor.Section4.ArrowVertex.arrow_id line 100
Source documentation
The trivial path acts as the identity on its vertex.
```
@[simp] theorem arrow_id (e : B) (he : e * e = e) (P : BiComplex k B) :
    arrowComplex k B e e e he P = 𝟙 ((vertexComplex k B e).obj P) := by
…
```
Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex, OAI.ExternalTensor.Section4.ArrowVertex.vertexComplex
def OAI.ExternalTensor.Section4.ArrowVertex.diagonal line 107
Source documentation
The original diagonal tensor e tensor n in its actual fixed submodule.
```
def diagonal (e : B) (he : e * e = e) :
    𝟭 (ModuleCat.{u} Bᵐᵒᵖ) ⟶ columnFunctor k B e ⋙ vertex k B e where
…
```
Mentions: OAI.ExternalTensor.Section4.columnFunctor, OAI.ExternalTensor.Section4.ArrowVertex.vertex
def OAI.ExternalTensor.Section4.ArrowVertex.diagonalComplex line 125
Source documentation
Original insertion into a single induced column, degree by degree.
```
def diagonalComplex (e : B) (he : e * e = e) (D : RightComplex B) :
    D ⟶ (vertexComplex k B e).obj ((columnComplex k B e).obj D) where
…
```
Mentions: OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.ArrowVertex.vertexComplex, OAI.ExternalTensor.Section4.columnComplex
theorem OAI.ExternalTensor.Section4.ArrowVertex.diagonal_naturality line 130
theorem OAI.ExternalTensor.Section4.ArrowVertex.diagonal_path line 138
Source documentation
Right multiplication in p at e_j agrees with left arrow action at e_i.
```
@[reassoc] theorem diagonal_path (ei ej a : B) (hei : ei * ei = ei)
    (hej : ej * ej = ej) (hai : a * ei = a) (hja : ej * a = a)
    (D : RightComplex B) :
    diagonalComplex k B ej hej D ≫ (vertexComplex k B ej).map (path k B ei ej a hai D) =
      diagonalComplex k B ei hei D ≫
        arrowComplex k B ei ej a hja ((columnComplex k B ei).obj D) := by
…
```
Mentions: OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.ArrowVertex.diagonalComplex, OAI.ExternalTensor.Section4.ArrowVertex.vertexComplex, OAI.ExternalTensor.map, OAI.ExternalTensor.Section4.path, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex, OAI.ExternalTensor.Section4.columnComplex
theorem OAI.ExternalTensor.Section4.ArrowVertex.arrow_naturality line 153