FixedDiagram.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.FixedDiagram.action_relations line 15

Source documentation

Algebra relations are the homogeneous quadratic diagram relations under any action.

theorem action_relations {X : Q} (ρ : R →ₐ[k] End X) (na nb nr : ℕ)
    (x : Fin na → R) (y : Fin nb → R) (c : Fin nr → Fin na → Fin nb → k)
    (hc : ∀ t, ∑ a, ∑ b, c t a b • (y b * x a) = 0) :
    ∀ t, ∑ a, ∑ b, c t a b • ((ρ (x a) : X ⟶ X) ≫ ρ (y b)) = 0 := by
…

theorem OAI.LittleFinitistic.FixedDiagram.fixed_diagram line 35

Source documentation

Fixed source-category objects and arrows, with every quadratic relation exact, represent the odd double of the selecting action in the localization.

theorem fixed_diagram {L : Q} (θ : R →ₐ[k] End L)
    (e : R) (he : e*e=e) (hec : ∀ r : R, e*r=r*e) (α : R →ₐ[k] R)
    (na nb nr : ℕ) (x : Fin na → R) (y : Fin nb → R)
    (c : Fin nr → Fin na → Fin nb → k)
    (hc : ∀ t, ∑ a, ∑ b, c t a b • (y b * x a) = 0) :
    ∃ (V₀ : Q) (ρ₀ : R →ₐ[k] End V₀)
      (i : (toKaroubi Q).obj V₀ ≅
        summand θ e he ⊞ OddDouble.formalShift (summand θ e he) 3)
      (D₀ D₁ D₂ : C) (φ₀ : q.obj D₀ ≅ V₀) (φ₁ : q.obj D₁ ≅ V₀)
      (φ₂ : q.obj D₂ ≅ V₀) (f : Fin na → (D₀ ⟶ D₁)) (g : Fin nb → (D₁ ⟶ D₂)),
      (∀ r : R, (toKaroubi Q).map (ρ₀ r) ≫ i.hom =
        i.hom ≫ oddDoubleAction θ e he hec α r) ∧
…

Mentions: OAI.LittleFinitistic.OddDouble.formalShift