OAI/Algebra/Finitistic/Bar/LeadingSupportedComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.mapIso_trans_congr line 11
2. def OAI.DerivedBar.ParityBridge.supportedLeadingIso line 38
3. theorem OAI.DerivedBar.ParityBridge.iso_mpr_source line 47
4. theorem OAI.DerivedBar.ParityBridge.leadingSummandIso_explicit line 52
5. theorem OAI.DerivedBar.ParityBridge.supportedLeadingIso_eq line 67
6. theorem OAI.DerivedBar.ParityBridge.supportedLeading_length line 89
7. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_supported_comp line 94
8. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_on_summand line 114
9. theorem OAI.DerivedBar.ParityBridge.supportedLeadingIso_apply line 134
10. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_of_pattern line 150
11. theorem OAI.DerivedBar.ParityBridge.outerBarSuffix_supported line 170
12. theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_supported line 197

    Source documentation

    The leading total embedding on every surviving recursive summand is the original literal tensor inclusion under the previously constructed coordinates.

    theorem leadingTotalEmbedding_supported (r n i q : ℕ) (hq : i+q=n) (t : Index r q)
        (h : inputDegree r t=0)
        (v : summand (leadingBarSequence k D X r) Z (r+1) n ⟨⟨⟨i,q⟩,hq⟩,t⟩) :
        ((inclusion (leadingBarSequence k D X r) Z (r+1) n ⟨⟨⟨i,q⟩,hq⟩,t⟩ ≫
          eqToHom (congrArg (fun W => W.X n) (leadingIter_total k D X N r)) ≫
          leadingTotalEmbedding k D X N r n).hom v) =
        outerCast k D X N (supportedLeading_length r n ⟨⟨⟨i,q⟩,hq⟩,t⟩ h)
          (AlgebraTensorModule.lTensor D D (embed k D X N (List.replicate i false ++ innerPattern r t))
            ((supportedLeadingIso k D X N r n ⟨⟨⟨i,q⟩,hq⟩,t⟩ h).hom.hom v)) := by
    …

    Mentions: OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.ParityBridge.leadingIter_total, OAI.DerivedBar.ParityBridge.leadingTotalEmbedding, OAI.DerivedBar.ParityBridge.outerCast, OAI.DerivedBar.ParityBridge.supportedLeading_length, OAI.DerivedBar.ParityBridge.supportedLeadingIso