Multiplicative bases

MultiplicativeBasisDeformations.Foundations.CoordGrading

Coordinates of a simultaneous integer grading #

A grading by an abelian group (for simultaneous integer weights, ℤʳ) gives an integer grading for each coordinate M →+ ℤ (MGr.coord); their projections preserve each other's homogeneous elements and those of any grading commuting with the ℤʳ-grading (coord_preserve). A ℤ-grading and a commuting grading by an abelian group combine into one grading (MGr.comb), and a finite-dimensional space has a basis homogeneous for both (exists_homBasis_comb).

source
def MultiplicativeBasisDeformations.MGr.coord {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) (i : M →+ ℤ) :
GExt.ZGr N

The grading by a coordinate φ : M → ℤ of the weight.

Instances For
    source
    theorem MultiplicativeBasisDeformations.MGr.coord_proj {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) (i : M →+ ℤ) (n : ℤ) (x : N) :
    ((G.coord i).proj n) x = ∑ g ∈ G.supp with i g = n, (G.proj g) x
    source
    theorem MultiplicativeBasisDeformations.MGr.coord_isHom {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) {g : M} {x : N} (h : G.IsHom g x) (i : M →+ ℤ) :
    (G.coord i).IsHom (i g) x
    source
    theorem MultiplicativeBasisDeformations.MGr.coord_preserve {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) {P : N → Prop} (h0 : ∀ (x y : N), P x → P y → P (x + y)) (hz : P 0) (hG : ∀ (g : M) (x : N), P x → P ((G.proj g) x)) (i : M →+ ℤ) (n : ℤ) {x : N} (hx : P x) :
    P (((G.coord i).proj n) x)

    Coordinate projections preserve what the projections of G preserve.

    source
    theorem MultiplicativeBasisDeformations.MGr.coord_proj_proj {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) (j : M →+ ℤ) (p : ℤ) (g : M) (y : N) :
    ((G.coord j).proj p) ((G.proj g) y) = if g ∈ G.supp ∧ j g = p then (G.proj g) y else 0
    source
    theorem MultiplicativeBasisDeformations.MGr.proj_coord {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) (j : M →+ ℤ) (p : ℤ) (g : M) {y : N} (hy : (G.coord j).IsHom p y) :
    (G.coord j).IsHom p ((G.proj g) y)

    The projections of G preserve the homogeneous elements of the coordinates.

    source
    theorem MultiplicativeBasisDeformations.MGr.coord_coord {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (G : MGr R M N) (i j : M →+ ℤ) (n p : ℤ) {x : N} (hx : (G.coord j).IsHom p x) :
    (G.coord j).IsHom p (((G.coord i).proj n) x)

    The coordinate projections preserve the homogeneous elements of the other coordinates.

    Homogeneous bases #

    source
    @[reducible, inline]
    abbrev MultiplicativeBasisDeformations.MGr.homPart {k : Type u_3} [Field k] {M : Type u_4} [DecidableEq M] {N' : Type u_5} [AddCommGroup N'] [Module k N'] (G : MGr k M N') (g : ↥G.supp) :
    Submodule k N'

    The homogeneous component of weight g, indexed by the support.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.MGr.proj_homPart {k : Type u_3} [Field k] {M : Type u_4} [AddCommGroup M] [DecidableEq M] {N' : Type u_5} [AddCommGroup N'] [Module k N'] (G : MGr k M N') {g : M} {h : ↥G.supp} {x : N'} (hx : x ∈ G.homPart h) :
      (G.proj g) x = if ↑h = g then x else 0
      source
      theorem MultiplicativeBasisDeformations.MGr.isInternal_homPart {k : Type u_3} [Field k] {M : Type u_4} [AddCommGroup M] [DecidableEq M] {N' : Type u_5} [AddCommGroup N'] [Module k N'] (G : MGr k M N') :
      DirectSum.IsInternal G.homPart
      source
      theorem MultiplicativeBasisDeformations.MGr.exists_homBasis {k : Type u_3} [Field k] {M : Type u_4} [AddCommGroup M] [DecidableEq M] {N' : Type u_5} [AddCommGroup N'] [Module k N'] (G : MGr k M N') [FiniteDimensional k N'] :
      ∃ (n : ℕ) (β : Module.Basis (Fin n) k N') (w : Fin n → M), ∀ (i : Fin n), G.IsHom (w i) (β i)

      Homogeneous bases for a grading by an abelian group.

      Degree and weight together #

      source
      def MultiplicativeBasisDeformations.MGr.comb {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [DecidableEq M] (o : GExt.ZGr N) (G : MGr R M N) (hc : ∀ (p : ℤ) (g : M) (x : N), (o.proj p) ((G.proj g) x) = (G.proj g) ((o.proj p) x)) :
      MGr R (ℤ × M) N

      The combined grading by degree and weight.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.MGr.comb_isHom {R : Type u_1} [CommRing R] {N : Type u_2} [AddCommGroup N] [Module R N] {M : Type u_3} [AddCommGroup M] [DecidableEq M] (o : GExt.ZGr N) (G : MGr R M N) (hc : ∀ (p : ℤ) (g : M) (x : N), (o.proj p) ((G.proj g) x) = (G.proj g) ((o.proj p) x)) {p : ℤ} {g : M} {x : N} (h : (comb o G hc).IsHom (p, g) x) :
        o.IsHom p x ∧ G.IsHom g x