OAI/Algebra/Finitistic/Bar/SuffixParityFaces.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.ParityBridge.termCast line 16

   Source documentation

   Explicit degree transport; it changes no tensor factor or action.

   def termCast {a b : ℕ} (h : a=b) : term k A N a →ₗ[k] term k A N b := by
   …

   Mentions: OAI.DerivedBar.term

2. theorem OAI.DerivedBar.ParityBridge.termCast_refl line 20
3. theorem OAI.DerivedBar.ParityBridge.termCast_tmul line 23
4. def OAI.DerivedBar.ParityBridge.suffixEmbed line 33

   Source documentation

   Insert any D block before an arbitrary linear suffix, preserving its tensor order.

   def suffixEmbed (s : ℕ) (e : M →ₗ[k] term k A N s) :
       (n : ℕ) → term k D M n →ₗ[k] term k A N (s+n)
     | 0 => e
     | n+1 => TensorProduct.map (inlAlgHom k D X).toLinearMap (suffixEmbed s e n)
   
   omit [Module D M] [IsScalarTower k D M] in

   Mentions: OAI.DerivedBar.term

5. theorem OAI.DerivedBar.ParityBridge.suffixEmbed_tmul line 39
6. theorem OAI.DerivedBar.ParityBridge.suffixEmbed_smul line 47
7. theorem OAI.DerivedBar.ParityBridge.parity_suffixEmbed line 63

   Source documentation

   General D-block comparison, including the differential of an arbitrary positive-length suffix. The second term is the totalization sign, not zero.

   theorem parity_suffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N (s+1))
       (he : ∀ (d : D) (v : M), e (d • v) = (inl d : A) • e v)
       (v : term k D M (n+1)) :
       SquareZero.multibarAugmentedDifferential k D X N ((s+1)+n)
         (suffixEmbed k D X N M (s+1) e (n+1) v) =
       suffixEmbed k D X N M (s+1) e n (DerivedBar.differential k D M n v) +
         (-1 : k)^(n+1) • termCast k D X N (show s+(n+1)=(s+1)+n by omega)
           (suffixEmbed k D X N M s
             ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) (n+1) v) := by
   …

   Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.suffixEmbed, OAI.DerivedBar.differential, OAI.DerivedBar.ParityBridge.termCast

8. def OAI.DerivedBar.ParityBridge.idealSuffixEmbed line 108

   Source documentation

   Literal X coefficient followed by any D block and any recursive suffix.

   def idealSuffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N s) :
       X ⊗[k] term k D M n →ₗ[k] term k A N ((s+n)+1) :=
   …

   Mentions: OAI.DerivedBar.term

9. theorem OAI.DerivedBar.ParityBridge.idealSuffixEmbed_tmul line 113
10. theorem OAI.DerivedBar.ParityBridge.ideal_action_suffixEmbed line 120

    Source documentation

    The original right D action supplies the first face for every suffix.

    theorem ideal_action_suffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N s)
        (x : X) (v : term k D M (n+1)) :
        (inr x : A) • suffixEmbed k D X N M s e (n+1) v =
          idealSuffixEmbed k D X N M s n e
            (BimoduleTensor.collapse k D X (term k D M n) (x ⊗ₜ[k] v)) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.ParityBridge.suffixEmbed, OAI.DerivedBar.ParityBridge.idealSuffixEmbed, OAI.DerivedBar.BimoduleTensor.collapse

11. theorem OAI.DerivedBar.ParityBridge.parity_idealSuffixEmbed line 134

    Source documentation

    General two-sided X-bar comparison. Both horizontal and signed suffix faces are retained; the right D action is the bimodule's original action.

    theorem parity_idealSuffixEmbed (s n : ℕ) (e : M →ₗ[k] term k A N (s+1))
        (he : ∀ (d : D) (v : M), e (d • v) = (inl d : A) • e v)
        (v : X ⊗[k] term k D M (n+1)) :
        SquareZero.multibarAugmentedDifferential k D X N (((s+1)+n)+1)
          (idealSuffixEmbed k D X N M (s+1) (n+1) e v) =
        -idealSuffixEmbed k D X N M (s+1) n e (BimoduleTensor.barDifferential k D X M n v) +
          (-1 : k)^(n+1) • termCast k D X N (show (s+(n+1))+1=((s+1)+n)+1 by omega)
            (idealSuffixEmbed k D X N M s (n+1)
              ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) v) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.idealSuffixEmbed, OAI.DerivedBar.BimoduleTensor.barDifferential, OAI.DerivedBar.ParityBridge.termCast

12. theorem OAI.DerivedBar.ParityBridge.parity_idealSuffixEmbed_zero line 159

    Source documentation

    At an empty D block the ideal endpoint vanishes, leaving all suffix faces.

    theorem parity_idealSuffixEmbed_zero (s : ℕ) (e : M →ₗ[k] term k A N (s+1))
        (he : ∀ (x : X) (v : M), (inr x : A) • e v = 0)
        (v : X ⊗[k] M) :
        SquareZero.multibarAugmentedDifferential k D X N (s+1)
          (idealSuffixEmbed k D X N M (s+1) 0 e v) =
        idealSuffixEmbed k D X N M s 0
          ((SquareZero.multibarAugmentedDifferential k D X N s).comp e) v := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.idealSuffixEmbed