NativeArrowBridge.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.vertex_eq line 14
Source documentation
The native and generic functors retain definitionally the same original fixed submodule.
```
theorem vertex_eq (e : B) : vertex k B e = LittleFinitistic.BimoduleVertex.functor k B e := rfl
…
```
Mentions: OAI.ExternalTensor.Section4.ArrowVertex.vertex, OAI.LittleFinitistic.BimoduleVertex.functor
theorem OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.total_eq line 24
Source documentation
The native P is exactly the total already used for actual arrow compatibility.
```
theorem total_eq : actualP s D₀ D₁ D₂ f g H =
    LittleFinitistic.InducedRectification.total s D₀ D₁ D₂ f g H := rfl
```
Mentions: OAI.ExternalTensor.Section4.ArrowVertex.actualP, OAI.LittleFinitistic.InducedRectification.total
theorem OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.inclusion_eq line 28
Source documentation
The native zero-column inclusion is exactly the one in the proved endpoints.
```
theorem inclusion_eq : LittleFinitistic.RectificationTotal.inclusion
    (p s D₀ D₁ D₂ f g) (q s D₀ D₁ D₂ f g) (nullHomotopy s D₀ D₁ D₂ f g H) =
      LittleFinitistic.InducedRectification.inclusion s D₀ D₁ D₂ f g H := rfl
```
Mentions: OAI.LittleFinitistic.RectificationTotal.inclusion, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.nullHomotopy, OAI.LittleFinitistic.InducedRectification.inclusion
abbrev OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.nativeVertex line 32
def OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.originalIota line 36
Source documentation
The direct original insertion in the native P and native fixed-submodule functor.
```
def originalIota (e : B) (he : e * e = e) (D : RightComplex B)
    (t : (columnComplex k B e).obj D ⟶ L0Prime s D₀ D₁ D₂ f g) :
    D ⟶ (nativeVertex e).obj (LittleFinitistic.InducedRectification.total s D₀ D₁ D₂ f g H) :=
…
```
Mentions: OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.columnComplex, OAI.ExternalTensor.Section4.L0Prime, OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.nativeVertex, OAI.LittleFinitistic.InducedRectification.total
theorem OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.iota_eq_original line 43
Source documentation
No comparison hypothesis is needed to identify the proved insertion with native maps.
```
theorem iota_eq_original (e : B) (he : e * e = e) (D : RightComplex B)
    (t : (columnComplex k B e).obj D ⟶ L0Prime s D₀ D₁ D₂ f g) :
    iota (p s D₀ D₁ D₂ f g) (q s D₀ D₁ D₂ f g)
      (nullHomotopy s D₀ D₁ D₂ f g H) e he D t =
      originalIota s D₀ D₁ D₂ f g H e he D t := by
…
```
Mentions: OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.columnComplex, OAI.ExternalTensor.Section4.L0Prime, OAI.ExternalTensor.Section4.ArrowVertex.iota, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.nullHomotopy, OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.originalIota
theorem OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.diagonal_eq_of_original line 52
Source documentation
The native original diagonal map is determined by its tensor formula.
```
theorem diagonal_eq_of_original (e : B) (he : e * e = e) (D : RightComplex B)
    (j : D ⟶ (nativeVertex e).obj ((columnComplex k B e).obj D))
    (hj : ∀ n x, ((j.f n) x).val = generator B e ⊗ₜ[k] x) :
    j = diagonalComplex k B e he D := by
…
```
Mentions: OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.nativeVertex, OAI.ExternalTensor.Section4.columnComplex, OAI.ExternalTensor.generator, OAI.ExternalTensor.Section4.ArrowVertex.diagonalComplex

def OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.nativeCompatibility01 line 61

Source documentation

Actual arrow-01 compatibility with the native P, vertex functors and inclusions.

def nativeCompatibility01 (h₀ : s.e₀ * s.e₀ = s.e₀) (h₁ : s.e₁ * s.e₁ = s.e₁)
    (a : A) (ha : s.e₁ * s.a a = s.a a) :
    Homotopy
      (originalIota s D₀ D₁ D₂ f g H s.e₀ h₀ D₀ (inducedData s D₀ D₁ D₂ f g).in₀ ≫
        arrowComplex k B s.e₀ s.e₁ (s.a a) ha
          (LittleFinitistic.InducedRectification.total s D₀ D₁ D₂ f g H))
      (f a ≫ originalIota s D₀ D₁ D₂ f g H s.e₁ h₁ D₁
        (inducedData s D₀ D₁ D₂ f g).in₁) := by
…

Mentions: OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.originalIota, OAI.ExternalTensor.Section4.inducedData, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex, OAI.LittleFinitistic.InducedRectification.total

def OAI.ExternalTensor.Section4.ArrowVertex.NativeBridge.nativeCompatibility12 line 76

Source documentation

Actual arrow-12 compatibility with the native P, vertex functors and inclusions.

def nativeCompatibility12 (h₁ : s.e₁ * s.e₁ = s.e₁) (h₂ : s.e₂ * s.e₂ = s.e₂)
    (b : J) (hb : s.e₂ * s.b b = s.b b) :
    Homotopy
      (originalIota s D₀ D₁ D₂ f g H s.e₁ h₁ D₁ (inducedData s D₀ D₁ D₂ f g).in₁ ≫
        arrowComplex k B s.e₁ s.e₂ (s.b b) hb
          (LittleFinitistic.InducedRectification.total s D₀ D₁ D₂ f g H))
      (g b ≫ originalIota s D₀ D₁ D₂ f g H s.e₂ h₂ D₂
        (inducedData s D₀ D₁ D₂ f g).in₂) := by
…