Documentation

TauCeti.LinearAlgebra.Graded.Shift

Shifted gradings and the suspension of graded operations #

This file shifts a family of graded pieces, records what the shift does to the degree of a homogeneous linear or multilinear map, and defines the sign acquired when a multilinear operation is suspended.

The shift of a family ๐’œ by c is the regrading Graded.shift ๐’œ c whose degree-p piece is ๐’œ (p + c); this is the cochain shift X[c]แต– = X^{p + c}, and at c = 1 it is the suspension sA of the Aโˆž conventions. Suspension does not move any element: the canonical map s : A โŸถ sA and its inverse are the two directions of Graded.shiftEquiv, the identity equivalence of the underlying module. All of their content is in the degrees recorded by LinearMap.isHomogeneous_shiftEquiv and LinearMap.isHomogeneous_shiftEquiv_symm.

The degree translation for multilinear maps says that a map of degree q after shifting the i-th input grading by c i and the target grading by r has degree q + r - โˆ‘ i, c i in the original gradings. Its specialisation TauCeti.MultilinearMap.isHomogeneous_suspension_iff is the degree half of the commuting square

(sA)^โŠ—n  --bโ‚™--> sA
    โ†‘s^โŠ—n           โ†‘s
 A^โŠ—n     --mโ‚™-->  A

that defines the suspended operations of an Aโˆž algebra: an arity-n operation is homogeneous of degree one for the suspended grading exactly when it is homogeneous of degree 2 - n for the original one. The tensor power of suspension is not constructed here; MultilinearMap.suspend adopts its Koszul sign as the evaluation-level definition of the suspended operation.

Main definitions #

Main results #

References #

source
def TauCeti.Graded.shift {ฮน : Type uฮน} {ฯƒM : Type u_1} [Add ฮน] (๐’œ : ฮน โ†’ ฯƒM) (c : ฮน) :
ฮน โ†’ ฯƒM

The shift of a family of graded pieces by c: the degree-p piece of Graded.shift ๐’œ c is the degree-(p + c) piece of ๐’œ. This is the cochain regrading X[c]แต– = X^{p + c}; the case c = 1 is the suspension sA of the Aโˆž conventions.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Graded.shift_apply {ฮน : Type uฮน} {ฯƒM : Type u_1} [Add ฮน] (๐’œ : ฮน โ†’ ฯƒM) (c p : ฮน) :
    shift ๐’œ c p = ๐’œ (p + c)
    source
    @[simp]
    theorem TauCeti.Graded.shift_zero {ฮน : Type uฮน} {ฯƒM : Type u_1} [AddZeroClass ฮน] (๐’œ : ฮน โ†’ ฯƒM) :
    shift ๐’œ 0 = ๐’œ
    source
    @[simp]
    theorem TauCeti.Graded.shift_shift {ฮน : Type uฮน} {ฯƒM : Type u_1} [AddSemigroup ฮน] (๐’œ : ฮน โ†’ ฯƒM) (c d : ฮน) :
    shift (shift ๐’œ c) d = shift ๐’œ (d + c)

    Shifting twice shifts by the sum of the two amounts.

    source
    def TauCeti.Graded.shiftEquiv (R : Type uR) (M : Type uM) [Semiring R] [AddCommMonoid M] [Module R M] :
    M โ‰ƒโ‚—[R] M

    The canonical equivalence on the underlying module of a grading and its shift. At a shift by one, its forward map is suspension and its inverse is unsuspension; the grading change and their respective degrees are recorded by LinearMap.isHomogeneous_shiftEquiv and LinearMap.isHomogeneous_shiftEquiv_symm.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Graded.shiftEquiv_apply (R : Type uR) (M : Type uM) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
      (shiftEquiv R M) x = x
      source
      @[simp]
      theorem TauCeti.Graded.shiftEquiv_symm_apply (R : Type uR) (M : Type uM) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
      (shiftEquiv R M).symm x = x
      source
      @[simp]
      theorem TauCeti.LinearMap.isHomogeneous_shift_target_iff {R : Type uR} {ฮน : Type uฮน} {M : Type uM} {N : Type uN} {ฯƒM : Type u_1} {ฯƒN : Type u_2} [Semiring R] [AddMonoid ฮน] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike ฯƒM M] [SetLike ฯƒN N] {f : M โ†’โ‚—[R] N} {๐’œ : ฮน โ†’ ฯƒM} {โ„ฌ : ฮน โ†’ ฯƒN} {q c : ฮน} :
      IsHomogeneous f ๐’œ (Graded.shift โ„ฌ c) q โ†” IsHomogeneous f ๐’œ โ„ฌ (q + c)

      Shifting the target grading by c lowers the degree of a homogeneous linear map by c.

      source
      theorem TauCeti.LinearMap.isHomogeneous_shiftEquiv_symm {R : Type uR} {ฮน : Type uฮน} {M : Type uM} {ฯƒM : Type u_1} [Semiring R] [AddMonoid ฮน] [AddCommMonoid M] [Module R M] [SetLike ฯƒM M] (๐’œ : ฮน โ†’ ฯƒM) (c : ฮน) :
      IsHomogeneous (โ†‘(Graded.shiftEquiv R M).symm) (Graded.shift ๐’œ c) ๐’œ c

      The inverse of Graded.shiftEquiv, viewed as the inverse of the shift by c, is homogeneous of degree c. At c = 1 this is unsuspension.

      source
      @[simp]
      theorem TauCeti.LinearMap.isHomogeneous_shift_source_iff {R : Type uR} {ฮน : Type uฮน} {M : Type uM} {N : Type uN} {ฯƒM : Type u_1} {ฯƒN : Type u_2} [Semiring R] [AddCommGroup ฮน] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike ฯƒM M] [SetLike ฯƒN N] {f : M โ†’โ‚—[R] N} {๐’œ : ฮน โ†’ ฯƒM} {โ„ฌ : ฮน โ†’ ฯƒN} {q c : ฮน} :
      IsHomogeneous f (Graded.shift ๐’œ c) โ„ฌ q โ†” IsHomogeneous f ๐’œ โ„ฌ (q - c)

      Shifting the source grading by c raises the degree of a homogeneous linear map by c.

      source
      theorem TauCeti.LinearMap.isHomogeneous_shift_iff {R : Type uR} {ฮน : Type uฮน} {M : Type uM} {N : Type uN} {ฯƒM : Type u_1} {ฯƒN : Type u_2} [Semiring R] [AddCommGroup ฮน] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike ฯƒM M] [SetLike ฯƒN N] {f : M โ†’โ‚—[R] N} {๐’œ : ฮน โ†’ ฯƒM} {โ„ฌ : ฮน โ†’ ฯƒN} {q c : ฮน} :
      IsHomogeneous f (Graded.shift ๐’œ c) (Graded.shift โ„ฌ c) q โ†” IsHomogeneous f ๐’œ โ„ฌ q

      Shifting the source and the target grading by the same amount leaves the degree of a homogeneous linear map unchanged.

      source
      theorem TauCeti.LinearMap.isHomogeneous_shiftEquiv {R : Type uR} {ฮน : Type uฮน} {M : Type uM} {ฯƒM : Type u_1} [Semiring R] [AddGroup ฮน] [AddCommMonoid M] [Module R M] [SetLike ฯƒM M] (๐’œ : ฮน โ†’ ฯƒM) (c : ฮน) :
      IsHomogeneous (โ†‘(Graded.shiftEquiv R M)) ๐’œ (Graded.shift ๐’œ c) (-c)

      The forward map of Graded.shiftEquiv, viewed as the shift by c, is homogeneous of degree -c. At c = 1 this is the degree -1 suspension map of the Aโˆž conventions.

      source
      @[simp]
      theorem TauCeti.LinearMap.homogeneousSubmodule_shift_target {R : Type uR} {S : Type u_1} {ฮน : Type uฮน} {M : Type uM} {N : Type uN} {ฯƒM : Type u_2} {ฯƒN : Type u_3} [Semiring R] [AddMonoid ฮน] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [SetLike ฯƒM M] [SetLike ฯƒN N] [Semiring S] [Module S N] [SMulCommClass R S N] [AddSubmonoidClass ฯƒN N] [SMulMemClass ฯƒN S N] (๐’œ : ฮน โ†’ ฯƒM) (โ„ฌ : ฮน โ†’ ฯƒN) (q c : ฮน) :
      homogeneousSubmodule ๐’œ (Graded.shift โ„ฌ c) q = homogeneousSubmodule ๐’œ โ„ฌ (q + c)

      Shifting the target grading by c shifts the submodule of homogeneous linear maps of degree q to the one of degree q + c.

      source
      @[simp]
      theorem TauCeti.MultilinearMap.isHomogeneous_shift_iff {R : Type uR} {ฮน : Type uฮน} {ฮบ : Type uฮบ} {M : ฮบ โ†’ Type uM} {N : Type uN} {ฯƒM : ฮบ โ†’ Type u_1} {ฯƒN : Type u_2} [Semiring R] [AddCommGroup ฮน] [Fintype ฮบ] [(i : ฮบ) โ†’ AddCommMonoid (M i)] [AddCommMonoid N] [(i : ฮบ) โ†’ Module R (M i)] [Module R N] [(i : ฮบ) โ†’ SetLike (ฯƒM i) (M i)] [SetLike ฯƒN N] {f : MultilinearMap R M N} {๐’œ : (i : ฮบ) โ†’ ฮน โ†’ ฯƒM i} {โ„ฌ : ฮน โ†’ ฯƒN} {q r : ฮน} {c : ฮบ โ†’ ฮน} :
      IsHomogeneous f (fun (i : ฮบ) => Graded.shift (๐’œ i) (c i)) (Graded.shift โ„ฌ r) q โ†” IsHomogeneous f ๐’œ โ„ฌ (q + r - โˆ‘ i : ฮบ, c i)

      A multilinear map of degree q after shifting the i-th input grading by c i and the target grading by r has degree q + r - โˆ‘ i, c i in the original gradings.

      source
      theorem TauCeti.MultilinearMap.isHomogeneous_shift_const_iff {R : Type uR} {ฮน : Type uฮน} {ฮบ : Type uฮบ} {M : ฮบ โ†’ Type uM} {N : Type uN} {ฯƒM : ฮบ โ†’ Type u_1} {ฯƒN : Type u_2} [Semiring R] [AddCommGroup ฮน] [Fintype ฮบ] [(i : ฮบ) โ†’ AddCommMonoid (M i)] [AddCommMonoid N] [(i : ฮบ) โ†’ Module R (M i)] [Module R N] [(i : ฮบ) โ†’ SetLike (ฯƒM i) (M i)] [SetLike ฯƒN N] {f : MultilinearMap R M N} {๐’œ : (i : ฮบ) โ†’ ฮน โ†’ ฯƒM i} {โ„ฌ : ฮน โ†’ ฯƒN} {q c : ฮน} :
      IsHomogeneous f (fun (i : ฮบ) => Graded.shift (๐’œ i) c) (Graded.shift โ„ฌ c) q โ†” IsHomogeneous f ๐’œ โ„ฌ (q + c - Fintype.card ฮบ โ€ข c)

      Shifting every input grading and the target grading by the same amount c changes the degree of an arity-Fintype.card ฮบ operation by c - Fintype.card ฮบ โ€ข c.

      source
      theorem TauCeti.MultilinearMap.isHomogeneous_suspension_iff {R : Type uR} {ฮบ : Type uฮบ} {M : Type uM} {ฯƒM : Type u_1} [Semiring R] [Fintype ฮบ] [AddCommMonoid M] [Module R M] [SetLike ฯƒM M] {f : MultilinearMap R (fun (x : ฮบ) => M) M} {๐’œ : โ„ค โ†’ ฯƒM} :
      IsHomogeneous f (fun (x : ฮบ) => Graded.shift ๐’œ 1) (Graded.shift ๐’œ 1) 1 โ†” IsHomogeneous f (fun (x : ฮบ) => ๐’œ) ๐’œ (2 - โ†‘(Fintype.card ฮบ))

      The suspension degree bridge. An arity-n operation is homogeneous of degree one for the suspended grading sA exactly when it is homogeneous of degree 2 - n for the original grading. This is the degree content of the square defining the suspended operations bโ‚™ of an Aโˆž algebra from its operations mโ‚™.

      source
      theorem TauCeti.MultilinearMap.isHomogeneous_suspension_fin_iff {R : Type uR} {M : Type uM} {ฯƒM : Type u_1} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike ฯƒM M] {n : โ„•} {f : MultilinearMap R (fun (x : Fin n) => M) M} {๐’œ : โ„ค โ†’ ฯƒM} :
      IsHomogeneous f (fun (x : Fin n) => Graded.shift ๐’œ 1) (Graded.shift ๐’œ 1) 1 โ†” IsHomogeneous f (fun (x : Fin n) => ๐’œ) ๐’œ (2 - โ†‘n)

      The suspension degree bridge for an operation of arity n. Reading off n = 1, 2, 3 gives the familiar degrees 1, 0 and -1 of the differential, the multiplication and the first higher product of an Aโˆž algebra.

      source
      def MultilinearMap.suspExp (k : โ„•) (d : โ„• โ†’ โ„ค) :
      โ„ค

      The exponent of the sign prescribed by the Koszul rule for suspending a tuple of inputs with degrees d. The suspension map has degree -1, so input i contributes its degree once for every input to its right.

      Equations
      Instances For
        source
        theorem MultilinearMap.suspExp_def (k : โ„•) (d : โ„• โ†’ โ„ค) :
        suspExp k d = โˆ‘ i โˆˆ Finset.range k, (โ†‘k - 1 - โ†‘i) * d i

        The defining sum for the suspension exponent.

        source
        @[simp]
        theorem MultilinearMap.suspExp_zero (d : โ„• โ†’ โ„ค) :
        suspExp 0 d = 0
        source
        @[simp]
        theorem MultilinearMap.suspExp_one (d : โ„• โ†’ โ„ค) :
        suspExp 1 d = 0
        source
        theorem MultilinearMap.suspExp_congr {k : โ„•} {d e : โ„• โ†’ โ„ค} (h : โˆ€ i < k, d i = e i) :
        suspExp k d = suspExp k e

        The suspension exponent only reads the first k degrees.

        source
        theorem MultilinearMap.suspExp_add (a b : โ„•) (d : โ„• โ†’ โ„ค) :
        suspExp (a + b) d = โˆ‘ i โˆˆ Finset.range a, (โ†‘a + โ†‘b - 1 - โ†‘i) * d i + โˆ‘ j โˆˆ Finset.range b, (โ†‘b - 1 - โ†‘j) * d (a + j)

        Split the suspension exponent between an initial block and the block following it.

        source
        theorem MultilinearMap.suspExp_add3 (a b c : โ„•) (d : โ„• โ†’ โ„ค) :
        suspExp (a + b + c) d = โˆ‘ i โˆˆ Finset.range a, (โ†‘a + โ†‘b + โ†‘c - 1 - โ†‘i) * d i + โˆ‘ j โˆˆ Finset.range b, (โ†‘c + โ†‘b - 1 - โ†‘j) * d (a + j) + โˆ‘ j โˆˆ Finset.range c, (โ†‘c - 1 - โ†‘j) * d (a + b + j)

        Split the suspension exponent into a prefix, a middle block, and a suffix.

        source
        def MultilinearMap.suspend {R : Type uR} [CommRing R] {k : โ„•} {M : Fin k โ†’ Type uM} {N : Type uN} [(i : Fin k) โ†’ AddCommMonoid (M i)] [(i : Fin k) โ†’ Module R (M i)] [AddCommMonoid N] [Module R N] (d : โ„• โ†’ โ„ค) (f : MultilinearMap R M N) :
        MultilinearMap R M N

        The signed operation prescribed by the suspension square. The tensor power of the suspension map is not formalized here; this adopts its Koszul sign as the definition.

        Equations
        Instances For
          source
          theorem MultilinearMap.suspend_eq_smul {R : Type uR} [CommRing R] {k : โ„•} {M : Fin k โ†’ Type uM} {N : Type uN} [(i : Fin k) โ†’ AddCommMonoid (M i)] [(i : Fin k) โ†’ Module R (M i)] [AddCommMonoid N] [Module R N] (d : โ„• โ†’ โ„ค) (f : MultilinearMap R M N) :
          suspend d f = TauCeti.negOnePowCast R (suspExp k d) โ€ข f

          Suspension scales an operation by the Koszul sign of the supplied degrees.

          source
          @[simp]
          theorem MultilinearMap.suspend_apply {R : Type uR} [CommRing R] {k : โ„•} {M : Fin k โ†’ Type uM} {N : Type uN} [(i : Fin k) โ†’ AddCommMonoid (M i)] [(i : Fin k) โ†’ Module R (M i)] [AddCommMonoid N] [Module R N] (d : โ„• โ†’ โ„ค) (f : MultilinearMap R M N) (x : (i : Fin k) โ†’ M i) :
          (suspend d f) x = TauCeti.negOnePowCast R (suspExp k d) โ€ข f x

          Evaluation of a suspended multilinear operation.

          source
          @[simp]
          theorem MultilinearMap.suspend_suspend {R : Type uR} [CommRing R] {k : โ„•} {M : Fin k โ†’ Type uM} {N : Type uN} [(i : Fin k) โ†’ AddCommMonoid (M i)] [(i : Fin k) โ†’ Module R (M i)] [AddCommMonoid N] [Module R N] (d : โ„• โ†’ โ„ค) (f : MultilinearMap R M N) :
          suspend d (suspend d f) = f

          Suspension for a fixed degree family is an involution, so suspend d also computes unsuspension.

          source
          theorem TauCeti.MultilinearMap.isHomogeneous_suspend_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {ฯƒ : Type u_1} [SetLike ฯƒ M] [SMulMemClass ฯƒ R M] {k : โ„•} {๐’œ : โ„ค โ†’ ฯƒ} {d : โ„• โ†’ โ„ค} {f : MultilinearMap R (fun (x : Fin k) => M) M} :
          IsHomogeneous (MultilinearMap.suspend d f) (fun (x : Fin k) => Graded.shift ๐’œ 1) (Graded.shift ๐’œ 1) 1 โ†” IsHomogeneous f (fun (x : Fin k) => ๐’œ) ๐’œ (2 - โ†‘k)

          Suspension gives an equivalence between the degree conditions on suspended and unsuspended operations.

          source
          theorem TauCeti.MultilinearMap.IsHomogeneous.suspend {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {ฯƒ : Type u_1} [SetLike ฯƒ M] [SMulMemClass ฯƒ R M] {k : โ„•} {๐’œ : โ„ค โ†’ ฯƒ} {d : โ„• โ†’ โ„ค} {f : MultilinearMap R (fun (x : Fin k) => M) M} (hf : IsHomogeneous f (fun (x : Fin k) => ๐’œ) ๐’œ (2 - โ†‘k)) :
          IsHomogeneous (MultilinearMap.suspend d f) (fun (x : Fin k) => Graded.shift ๐’œ 1) (Graded.shift ๐’œ 1) 1

          Suspending a homogeneous arity-k operation of degree 2 - k produces one of degree one.