SupportedInnerCoordinates.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.canonicalLinear line 32

Source documentation

Re-express a supplied k-linear map using the canonical scalars of ModuleCat D.

def canonicalLinear (V : Type u) [AddCommGroup V] [Module k V] [Module D V]
    [IsScalarTower k D V] (s : ℕ) (e : V →ₗ[k] term k A N s) :
    letI : Module k V := BimoduleTensor.scalarModule k D (ModuleCat.of D V)
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.BimoduleTensor.scalarModule

theorem OAI.DerivedBar.ParityBridge.canonicalLinear_apply line 40

theorem OAI.DerivedBar.ParityBridge.barSuffix_canonicalLinear line 48

Source documentation

Prefixing a canonically re-expressed map recovers the supplied-scalars literal formula.

theorem barSuffix_canonicalLinear (V : Type u) [AddCommGroup V] [Module k V]
    [Module D V] [IsScalarTower k D V] (s i : ℕ) (e : V →ₗ[k] term k A N s)
    (v : ((XB).obj (ModuleCat.of D V)).X i) :
    barSuffix k D X N (ModuleCat.of D V) s i (canonicalLinear k D X N V s e) v =
      idealSuffixEmbed k D X N V s i e ((twoSidedBarObjIso k D X V i).hom.hom v) := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.barSuffix, OAI.DerivedBar.ParityBridge.canonicalLinear, OAI.DerivedBar.ParityBridge.idealSuffixEmbed

def OAI.DerivedBar.ParityBridge.supportedInnerIso line 58

Source documentation

The same literal inner coordinates, with the proved degree-zero input made explicit.

def supportedInnerIso : (r n : ℕ) → (t : Index r n) → (h : inputDegree r t=0) →
    summand B Z r n t ≅ ModuleCat.of D (patternTerm k D X N (innerPattern r t))
  | 0, n, t, h => by
      change n=0 at h
      subst n
      exact Iso.refl _
  | r+1, _, ⟨p,t⟩, h =>
      (XB ⋙ HomologicalComplex.eval _ c p.val.1).mapIso (supportedInnerIso r p.val.2 t h) ≪≫
        twoSidedBarPatternIso k D X N p.val.1 (innerPattern r t)

/-- Transport of the terminal input along an equality of D-modules commutes
with the genuine categorical bar pattern coordinates. -/

theorem OAI.DerivedBar.ParityBridge.twoSidedBarPatternIso_eqToIso line 70

Source documentation

Transport of the terminal input along an equality of D-modules commutes with the genuine categorical bar pattern coordinates.

theorem twoSidedBarPatternIso_eqToIso (V W : ModuleCat.{u} D) (h : V=W)
    (i : ℕ) (p : List Bool) :
    (XB ⋙ HomologicalComplex.eval _ c i).mapIso
      (eqToIso (congrArg (fun V : ModuleCat D => ModuleCat.of D (patternTerm k D X V p)) h)) ≪≫
        twoSidedBarPatternIso k D X W i p =
    twoSidedBarPatternIso k D X V i p ≪≫
      eqToIso (congrArg (fun V : ModuleCat D =>
        ModuleCat.of D (patternTerm k D X V (true :: (List.replicate i false ++ p)))) h) := by
…

theorem OAI.DerivedBar.ParityBridge.supportedInnerIso_eq line 83

Source documentation

The supported recursion equals the already existing innerSummandIso, followed only by the forced zero-degree input transport.

theorem supportedInnerIso_eq (r n : ℕ) (t : Index r n) (h : inputDegree r t=0) :
    supportedInnerIso k D X N r n t h =
      innerSummandIso k D X Z r n t ≪≫ eqToIso
        (congrArg (fun V : ModuleCat D => ModuleCat.of D (patternTerm k D X V (innerPattern r t)))
          (show (Z).X (inputDegree r t)=N by rw [h]; rfl)) := by
…

Mentions: OAI.DerivedBar.ParityBridge.supportedInnerIso

theorem OAI.DerivedBar.ParityBridge.supportedInner_length line 109
Source documentation
Every surviving summand has exactly r+n literal internal slots.
```
theorem supportedInner_length (r n : ℕ) (t : Index r n) (h : inputDegree r t=0) :
    (innerPattern r t).length = r+n := by
…
```
def OAI.DerivedBar.ParityBridge.canonicalRestrict line 114
theorem OAI.DerivedBar.ParityBridge.canonicalRestrict_apply line 117
theorem OAI.DerivedBar.ParityBridge.innerEmbedding_supported line 122
Source documentation
The canonical recursive embedding agrees with the original literal word embedding on every supported summand, through the actual bar coordinate maps.
```
theorem innerEmbedding_supported (r n : ℕ) (t : Index r n) (h : inputDegree r t=0)
    (v : summand B Z r n t) :
    innerEmbedding k D X N r n ((lof B Z r n t).hom v) =
      termCast k D X N (supportedInner_length r n t h)
        (embed k D X N (innerPattern r t) ((supportedInnerIso k D X N r n t h).hom.hom v)) := by
…
```
Mentions: OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.ParityBridge.supportedInner_length, OAI.DerivedBar.ParityBridge.supportedInnerIso