ObjectwiseSplitting.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExternalTensor.Binomial.Objectwise.section4_objectwise line 14

Source documentation

Exact generic Section 4 statement, assuming only existence of each objectwise split.

theorem section4_objectwise (Phi : C ⥤ C) [Phi.Additive] [Phi.CommShift ℤ]
    (M : S → C) (H : S → S)
    (split : ∀ Y, Nonempty (Phi.obj (M Y) ≅ M (H Y) ⊞ (M (H Y))⟦(3 : ℤ)⟧))
    (j : ℕ) (Y : S) :
    Nonempty ((Phi.obj^[j]) (M Y) ≅
      ⨁ fun q : Fin (j+1) => ⨁ fun _ : Fin (Nat.choose j q.val) =>
        (M ((H^[j]) Y))⟦(3 : ℤ)*(q.val : ℤ)⟧) :=
…

theorem OAI.ExternalTensor.Binomial.Objectwise.section6_objectwise line 24

Source documentation

Exact generic Section 6 formula, assuming only existence of each two-step split.

theorem section6_objectwise (F : C ⥤ C) [F.Additive] [F.CommShift ℤ]
    (M : S → C) (H : S → S) (b : ℤ)
    (split : ∀ Y, Nonempty (F.obj (F.obj (M Y)) ≅
      (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+3⟧))
    (j : ℕ) (Y : S) :
    Nonempty ((F.obj^[2*j]) (M Y) ≅
      ⨁ fun q : Fin (j+1) => ⨁ fun _ : Fin (Nat.choose j q.val) =>
        (M ((H^[j]) Y))⟦(j : ℤ)*b + 3*(q.val : ℤ)⟧) :=
…

theorem OAI.ExternalTensor.Binomial.Objectwise.section6_zero_detection line 35

Source documentation

Exact generic zero detection for the two-step formula, with all hypotheses exposed.

theorem section6_zero_detection (F : C ⥤ C) [F.Additive] [F.CommShift ℤ]
    (M : S → C) (H : S → S) (b : ℤ)
    (split : ∀ Y, Nonempty (F.obj (F.obj (M Y)) ≅
      (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+3⟧))
    (j : ℕ) (Y : S) :
    IsZero ((F.obj^[2*j]) (M Y)) ↔ IsZero (M ((H^[j]) Y)) :=
…