OAI/Algebra/Finitistic/Rectification/ArrowCompatibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExternalTensor.Section4.ArrowVertex.iota line 14

   Source documentation

   Original insertion through the zero-column inclusion of the actual total.

   def iota {L₀ L₁ L₂ : BiComplex k B} (p : L₁ ⟶ L₀) (q : L₂ ⟶ L₁)
       (h : Homotopy (q ≫ p) 0) (e : B) (he : e * e = e)
       (D : RightComplex B) (t : (columnComplex k B e).obj D ⟶ L₀) :
       D ⟶ (vertexComplex k B e).obj (LittleFinitistic.RectificationTotal.total p q h) :=
   …

   Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.columnComplex, OAI.ExternalTensor.Section4.ArrowVertex.vertexComplex, OAI.LittleFinitistic.RectificationTotal.total

2. theorem OAI.ExternalTensor.Section4.ArrowVertex.iota_original line 22

   Source documentation

   The insertion has exactly the manuscript's diagonal tensor, before any coordinates.

   @[simp] theorem iota_original {L₀ L₁ L₂ : BiComplex k B}
       (p : L₁ ⟶ L₀) (q : L₂ ⟶ L₁) (h : Homotopy (q ≫ p) 0)
       (e : B) (he : e * e = e) (D : RightComplex B)
       (t : (columnComplex k B e).obj D ⟶ L₀) (n : ℤ) (x : D.X n) :
       (((iota p q h e he D t).f n) x).val =
         ((t ≫ LittleFinitistic.RectificationTotal.inclusion p q h).f n)
           (generator B e ⊗ₜ[k] x) := rfl

   Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.columnComplex, OAI.ExternalTensor.Section4.ArrowVertex.iota, OAI.LittleFinitistic.RectificationTotal.inclusion, OAI.ExternalTensor.generator

3. def OAI.ExternalTensor.Section4.ArrowVertex.compatibility line 31

   Source documentation

   The original p-boundary produces compatibility in the actual target vertex.

   def compatibility {L₀ L₁ L₂ : BiComplex k B} (p : L₁ ⟶ L₀) (q : L₂ ⟶ L₁)
       (h : Homotopy (q ≫ p) 0) (ei ej a : B) (hei : ei * ei = ei)
       (hej : ej * ej = ej) (hai : a * ei = a) (hja : ej * a = a)
       {D E : RightComplex B} (f : D ⟶ E)
       (t : (columnComplex k B ei).obj D ⟶ L₀)
       (u : (columnComplex k B ej).obj E ⟶ L₀)
       (w : (columnComplex k B ej).obj D ⟶ L₁)
       (hw : w ≫ p = path k B ei ej a hai D ≫ t - (columnComplex k B ej).map f ≫ u) :
       Homotopy
         (iota p q h ei hei D t ≫ arrowComplex k B ei ej a hja
           (LittleFinitistic.RectificationTotal.total p q h))
         (f ≫ iota p q h ej hej E u) := by
   …

   Mentions: OAI.ExternalTensor.Section4.BiComplex, OAI.ExternalTensor.Section4.p, OAI.ExternalTensor.Section4.q, OAI.ExternalTensor.Section4.h, OAI.ExternalTensor.Section4.RightComplex, OAI.ExternalTensor.Section4.columnComplex, OAI.ExternalTensor.Section4.path, OAI.ExternalTensor.map, OAI.ExternalTensor.Section4.ArrowVertex.iota, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex, OAI.LittleFinitistic.RectificationTotal.total

4. abbrev OAI.ExternalTensor.Section4.ArrowVertex.actualP line 76
5. abbrev OAI.ExternalTensor.Section4.ArrowVertex.iota0 line 79
6. abbrev OAI.ExternalTensor.Section4.ArrowVertex.iota1 line 82
7. abbrev OAI.ExternalTensor.Section4.ArrowVertex.iota2 line 85
8. def OAI.ExternalTensor.Section4.ArrowVertex.compatibility01 line 90

   Source documentation

   Compatibility of the actual original vertex-zero insertion with every 0-to-1 arrow.

   def compatibility01 (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 (iota0 s D₀ D₁ D₂ f g H h₀ ≫
         arrowComplex k B s.e₀ s.e₁ (s.a a) ha (actualP s D₀ D₁ D₂ f g H))
         (f a ≫ iota1 s D₀ D₁ D₂ f g H h₁) :=
   …

   Mentions: OAI.ExternalTensor.Section4.ArrowVertex.iota0, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex, OAI.ExternalTensor.Section4.ArrowVertex.actualP, OAI.ExternalTensor.Section4.ArrowVertex.iota1

9. def OAI.ExternalTensor.Section4.ArrowVertex.compatibility12 line 100

   Source documentation

   Compatibility of the actual original vertex-one insertion with every 1-to-2 arrow.

   def compatibility12 (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 (iota1 s D₀ D₁ D₂ f g H h₁ ≫
         arrowComplex k B s.e₁ s.e₂ (s.b b) hb (actualP s D₀ D₁ D₂ f g H))
         (g b ≫ iota2 s D₀ D₁ D₂ f g H h₂) :=
   …

   Mentions: OAI.ExternalTensor.Section4.ArrowVertex.iota1, OAI.ExternalTensor.Section4.ArrowVertex.arrowComplex, OAI.ExternalTensor.Section4.ArrowVertex.actualP, OAI.ExternalTensor.Section4.ArrowVertex.iota2