BinomialIteration.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExternalTensor.Binomial.branchIteration line 16

Source documentation

Apply the splitting independently at each object; no naturality in S is present.

def branchIteration (split : ∀ Y, Phi.obj (M Y) ≅ (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+d⟧)
    (j : ℕ) (Y : S) :
    (Phi.obj^[j]) (M Y) ≅
      ⨁ fun x : Branch j => (M ((H^[j]) Y))⟦(j : ℤ)*b + d*(weight x : ℤ)⟧ := by
…

Mentions: OAI.ExternalTensor.Binomial.Branch, OAI.ExternalTensor.Binomial.weight

def OAI.ExternalTensor.Binomial.binomialObject line 48
Source documentation
The manuscript's repeated finite biproduct, including the multiplicity index.
```
def binomialObject (j : ℕ) (X : C) : C :=
…
```
def OAI.ExternalTensor.Binomial.groupBiproduct line 53
Source documentation
Regroup by weight using the proved fiber cardinality, not an assumed decomposition.
```
def groupBiproduct (j : ℕ) (X : C) :
    (⨁ fun x : Branch j => X⟦(j : ℤ)*b + d*(weight x : ℤ)⟧) ≅
      binomialObject b d j X :=
…
```
Mentions: OAI.ExternalTensor.Binomial.Branch, OAI.ExternalTensor.Binomial.weight, OAI.ExternalTensor.Binomial.binomialObject

def OAI.ExternalTensor.Binomial.binomialIteration line 65

Source documentation

Categorical binomial iteration with a common shift offset.

def binomialIteration (split : ∀ Y, Phi.obj (M Y) ≅ (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+d⟧)
    (j : ℕ) (Y : S) :
    (Phi.obj^[j]) (M Y) ≅ binomialObject b d j (M ((H^[j]) Y)) :=
…

Mentions: OAI.ExternalTensor.Binomial.binomialObject

def OAI.ExternalTensor.Binomial.section4Iteration line 71

Source documentation

Section 4, final corollary, with only objectwise splitting isomorphisms.

def section4Iteration (split : ∀ Y, Phi.obj (M Y) ≅ M (H Y) ⊞ (M (H Y))⟦(3 : ℤ)⟧)
    (j : ℕ) (Y : S) :
    (Phi.obj^[j]) (M Y) ≅
      ⨁ fun q : Fin (j+1) => ⨁ fun _ : Fin (Nat.choose j q.val) =>
        (M ((H^[j]) Y))⟦(3 : ℤ)*(q.val : ℤ)⟧ := by
…