OAI/Algebra/Finitistic/Bar/ExplicitSignedDifferential.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.SquareZero.slotParity line 17

   Source documentation

   The parity operator is +1 on a D slot and -1 on an X slot.

   def slotParity : Module.End k A := baseProjection k D X - idealProjection k D X

   Mentions: OAI.DerivedBar.SquareZero.baseProjection, OAI.DerivedBar.SquareZero.idealProjection

2. theorem OAI.DerivedBar.SquareZero.slotParity_base line 19
3. theorem OAI.DerivedBar.SquareZero.slotParity_ideal line 22
4. def OAI.DerivedBar.SquareZero.multibarAugmentedDifferential line 27

   Source documentation

   Explicit bar faces with a sign change on crossing a D slot and no sign change on crossing an X slot. This is defined independently of count transport.

   def multibarAugmentedDifferential : (n : ℕ) → term k A N (n+1) →ₗ[k] term k A N n
     | 0 => ((action k A N).restrictScalars k).comp
         (TensorProduct.map (slotParity k D X) LinearMap.id)
     | n+1 => (((action k A (term k A N (n+1))).restrictScalars k) -
         TensorProduct.map LinearMap.id (multibarAugmentedDifferential n)).comp
           (TensorProduct.map (slotParity k D X) LinearMap.id)

   Mentions: OAI.DerivedBar.term, OAI.DerivedBar.action, OAI.DerivedBar.SquareZero.slotParity

5. theorem OAI.DerivedBar.SquareZero.multibarAugmentedDifferential_zero line 34
6. theorem OAI.DerivedBar.SquareZero.multibarAugmentedDifferential_succ line 37
7. def OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential line 44

   Source documentation

   The independent two-sided differential. The first face uses D's right A-action by projection. All remaining faces use the explicit slot parity recursion.

   def multibarTwoSidedDifferential (n : ℕ) :
       D ⊗[k] term k A N (n+1) →ₗ[D] D ⊗[k] term k A N n :=
   …

   Mentions: OAI.DerivedBar.term

8. theorem OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential_tmul line 52

   Source documentation

   Literal endpoint-minus-tail formula; no signed assembly occurs in the definition.

   theorem multibarTwoSidedDifferential_tmul (n : ℕ) (d : D) (v : term k A N (n+1)) :
       multibarTwoSidedDifferential k D X N n (d ⊗ₜ[k] v) =
         d • FreeBaseChange.coefficient (fstHom k D X) (term k A N n) v -
           d ⊗ₜ[k] multibarAugmentedDifferential k D X N n v := rfl

   Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential

9. theorem OAI.DerivedBar.SquareZero.multibarAugmented_empty_block line 60

   Source documentation

   A zero-length internal D block has no multiplication face: X squared is zero. The displayed surviving term consists only of the later blocks' faces.

   theorem multibarAugmented_empty_block (n : ℕ) (x y : X) (v : term k A N n) :
       multibarAugmentedDifferential k D X N (n+1)
         ((inr x : A) ⊗ₜ[k] ((inr y : A) ⊗ₜ[k] v)) =
       (inr x : A) ⊗ₜ[k] multibarAugmentedDifferential k D X N n
         ((inr y : A) ⊗ₜ[k] v) := by
   …

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

10. theorem OAI.DerivedBar.SquareZero.multibarAugmented_ideal_endpoint line 72

    Source documentation

    At the inflated module endpoint, an X action vanishes.

    theorem multibarAugmented_ideal_endpoint
        (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = (0 : N))
        (x : X) (v : N) :
        multibarAugmentedDifferential k D X N 0 ((inr x : A) ⊗ₜ[k] v) = 0 := by
    …

    Mentions: OAI.DerivedBar.SquareZero.multibarAugmentedDifferential

11. theorem OAI.DerivedBar.SquareZero.signedProjection_base_action_word line 80

    Source documentation

    Rescaling commutes with the D-action on each word.

    theorem signedProjection_base_action_word {n r : ℕ} {v : term k A N n}
        (hv : Word k D X N n r v) (d : D) :
        signedProjection k D X N n r ((inl d : A) • v) =
          (inl d : A) • signedProjection k D X N n r v := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.signedProjection

12. theorem OAI.DerivedBar.SquareZero.signedProjection_ideal_action_word line 101

    Source documentation

    Multiplying a D slot by X removes its r inversions with the remaining X slots.

    theorem signedProjection_ideal_action_word
        (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = (0 : N)) {n r : ℕ} {v : term k A N n}
        (hv : Word k D X N n r v) (x : X) :
        signedProjection k D X N n (r+1) ((inr x : A) • v) =
          (-1 : k)^r • ((inr x : A) • signedProjection k D X N n r v) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.signedProjection

13. theorem OAI.DerivedBar.SquareZero.multibarAugmented_sign_word line 121

    Source documentation

    Exact sign identity between the literal augmented faces and the ordinary bar on every homogeneous word. The differential was defined independently above.

    theorem multibarAugmented_sign_word
        (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = (0 : N)) (n r : ℕ) (v : term k A N (n+1))
        (hv : Word k D X N (n+1) r v) :
        multibarAugmentedDifferential k D X N n (signedProjection k D X N (n+1) r v) =
          (-1 : k)^r • signedProjection k D X N n r (differential k A N n v) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.SquareZero.signedProjection, OAI.DerivedBar.differential

14. theorem OAI.DerivedBar.SquareZero.coefficient_signed_word line 156

    Source documentation

    The leading endpoint has the same prescribed rescaling.

    theorem coefficient_signed_word (n r : ℕ) (v : term k A N (n+1))
        (hv : Word k D X N (n+1) r v) :
        FreeBaseChange.coefficient (fstHom k D X) (term k A N n)
            (signedProjection k D X N (n+1) r v) =
          (-1 : k)^r • twoSidedSignedProjection k D X N n r
            (FreeBaseChange.coefficient (fstHom k D X) (term k A N n) v) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.SquareZero.signedProjection, OAI.DerivedBar.SquareZero.twoSidedSignedProjection

15. theorem OAI.DerivedBar.SquareZero.multibarTwoSided_sign_word line 174

    Source documentation

    Equality of the independently defined two-sided faces and the shifted signed ordinary bar differential, on every homogeneous pure tensor.

    theorem multibarTwoSided_sign_word
        (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = (0 : N))
        (n r : ℕ) (d : D) (v : term k A N (n+1))
        (hv : Word k D X N (n+1) r v) :
        multibarTwoSidedDifferential k D X N n
            (twoSidedSignedProjection k D X N (n+1) r (d ⊗ₜ[k] v)) =
          (-1 : k)^r • twoSidedSignedProjection k D X N n r
            (twoSidedDifferential k A D N (fstHom k D X) n (d ⊗ₜ[k] v)) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.SquareZero.twoSidedSignedProjection, OAI.DerivedBar.twoSidedDifferential

16. theorem OAI.DerivedBar.SquareZero.multibarTwoSided_sign line 191

    Source documentation

    The sign comparison extends to the whole count submodule by linearity.

    theorem multibarTwoSided_sign
        (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = (0 : N))
        (n r : ℕ) {z : D ⊗[k] term k A N (n+1)}
        (hz : z ∈ twoSidedWeight k D X N (n+1) r) :
        multibarTwoSidedDifferential k D X N n (twoSidedSignedProjection k D X N (n+1) r z) =
          (-1 : k)^r • twoSidedSignedProjection k D X N n r
            (twoSidedDifferential k A D N (fstHom k D X) n z) := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.twoSidedWeight, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.SquareZero.twoSidedSignedProjection, OAI.DerivedBar.twoSidedDifferential