ConcreteFixedDiagram.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ConcreteFixedDiagram.fixed_diagram line 20

Source documentation

The fixed odd-double diagram in the actual Kᵇ(proj-B) and its actual Verdier quotient. Every independent relation of the constructed path algebra is included.

theorem fixed_diagram {L : SourceVerdier.Q E.relations} (θ : R →ₐ[k] End L)
    (e : R) (he : e*e=e) (hec : ∀ r : R, e*r=r*e) (α : R →ₐ[k] R) :
    ∃ (V₀ : SourceVerdier.Q E.relations) (ρ₀ : R →ₐ[k] End V₀)
      (i : (toKaroubi (SourceVerdier.Q E.relations)).obj V₀ ≅
        summand θ e he ⊞ OddDouble.formalShift (summand θ e he) 3)
      (D₀ D₁ D₂ : SourceVerdier.K E.relations)
      (φ₀ : (SourceVerdier.q E.relations).obj D₀ ≅ V₀)
      (φ₁ : (SourceVerdier.q E.relations).obj D₁ ≅ V₀)
      (φ₂ : (SourceVerdier.q E.relations).obj D₂ ≅ V₀)
      (f : Fin (E.generators+1) → (D₀ ⟶ D₁))
      (g : Fin (E.generators+1) → (D₁ ⟶ D₂)),
      (∀ r : R, (toKaroubi (SourceVerdier.Q E.relations)).map (ρ₀ r) ≫ i.hom =
…

Mentions: OAI.LittleFinitistic.SourceVerdier.Q, OAI.LittleFinitistic.OddDouble.formalShift, OAI.LittleFinitistic.SourceVerdier.K, OAI.LittleFinitistic.SourceVerdier.q