Weight-homogeneous lifts of the evaluated modules (Proposition 10.1)

integral-deformations.tex: "All these constructions can be chosen to preserve the simultaneous integer weights: lifting a basis of H_ℤ to mesh weights by Lemma 7.4 gives the modules M_i⁽²⁾ compatible weight gradings, and the corrections can be chosen in each weight component."

A mesh weight W of C⁽²⁾ with values in an abelian group M grades A⁽²⁾ and the evaluated modules (grA0, grEv, WeightEv.lean). When it lifts the ray weights hv of the table P (the rays Θ(b_r) are homogeneous of weight hv r, hΘ), each integer coordinate φ : M →+ ℤ grades A⁽²⁾ (galgW), A⁽⁴⁾ = 𝒪P (galgOW, by the ray weights) and the modules (gwEv), compatibly with the reduction (isRedW), the actions (actW), the degree and each other. Then the module lifts and arrow lifts of Proposition 10.1 can be chosen homogeneous for any finite family of coordinates (exists_modLiftW, exists_arrowLiftW), by exists_liftMod_weights and exists_liftHom_weights.

theorem MultiplicativeBasisDeformations.MeshWalk.zrepr_eq_zero {k : Type u_1} [Field k] {N : Type u_2} [AddCommGroup N] [Module k N] (g : GExt.ZGr N) {ι : Type u_3} [Fintype ι] (β : Module.Basis ι k N) (d : ι → ℤ) (hβ : ∀ (i : ι), g.IsHom (d i) (β i)) {p : ℤ} {m : N} (hm : g.IsHom p m) {i : ι} (hi : d i ≠ p) : (β.repr m) i = 0

The weight gradings of A⁽²⁾ and of the evaluated modules

theorem MultiplicativeBasisDeformations.MeshWalk.grA0_one {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) : (grA0 W ⋯ D).IsHom 0 1

noncomputable def MultiplicativeBasisDeformations.MeshWalk.galgW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (φ : M →+ ℤ) : GExt.GAlg (CatAlg.Alg D.F0)ᵐᵒᵖ

A⁽²⁾ graded by a coordinate φ of the mesh weight.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.gwEv {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (X : V) (φ : M →+ ℤ) : GExt.ZGr (CatAlg.Rep D.F0 (meshFam Q c X))

The evaluated module graded by a coordinate.

theorem MultiplicativeBasisDeformations.MeshWalk.coord_sum {M : Type} [AddCommGroup M] {N : Type u_1} [AddCommGroup N] [Module (ZMod 2) N] (G : MGr (ZMod 2) M N) (φ : M →+ ℤ) {p : ℤ} {x : N} (hx : (G.coord φ).IsHom p x) : ∑ g ∈ G.supp with φ g = p, (G.proj g) x = x

theorem MultiplicativeBasisDeformations.MeshWalk.actW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (φ : M →+ ℤ) (X : V) (p q : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (hm : (gwEv D W X φ).IsHom p m) (ha : (galgW D W φ).gr.IsHom q a) : (gwEv D W X φ).IsHom (p + q) (((gmodEv D ⋯ X).act m) a)

The action shifts the coordinate weights.

The ray weights of 𝒪P and the reduction

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.galgOW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} {M : Type} [AddCommGroup M] (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (φ : M →+ ℤ) : GExt.GAlg ↥(P.Lin (ZMod 4))

𝒪P graded by a coordinate of the ray weights.

theorem MultiplicativeBasisDeformations.MeshWalk.repr_Θ_symm_eq_zero_w {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) (φ : M →+ ℤ) {n : ℤ} {a : (CatAlg.Alg D.F0)ᵐᵒᵖ} (ha : (galgW D W φ).gr.IsHom n a) (r : R) (hr : φ (hv r) ≠ n) : ((P.basis (ZMod 2)).repr (T.Θ.symm a)) r = 0

theorem MultiplicativeBasisDeformations.MeshWalk.isRedW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) (φ : M →+ ℤ) : WLift.IsRed (galgOW hv hv_mul hv_e φ) (galgW D W φ) (πO T)

The reduction 𝒪P → A⁽²⁾ respects the coordinate weights.

Commutation of the gradings

theorem MultiplicativeBasisDeformations.MeshWalk.galgW_zgr {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (φ : M →+ ℤ) (v p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (ha : (galgA0 D ⋯).gr.IsHom p a) : (galgA0 D ⋯).gr.IsHom p (((galgW D W φ).gr.proj v) a)

theorem MultiplicativeBasisDeformations.MeshWalk.gwEv_zgr {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (X : V) (φ : M →+ ℤ) (u p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (hm : (zgrEv D ⋯ X).IsHom p m) : (zgrEv D ⋯ X).IsHom p (((gwEv D W X φ).proj u) m)

theorem MultiplicativeBasisDeformations.MeshWalk.comm_ev {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (X : V) (p : ℤ) (g : M) (m : CatAlg.Rep D.F0 (meshFam Q c X)) : ((zgrEv D ⋯ X).proj p) (((grEv W ⋯ D X).proj g) m) = ((grEv W ⋯ D X).proj g) (((zgrEv D ⋯ X).proj p) m)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_homBasis_w {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) (X : V) : ∃ (n : ℕ) (β : Module.Basis (Fin n) (ZMod 2) (CatAlg.Rep D.F0 (meshFam Q c X))) (dβ : Fin n → ℤ) (wβ : Fin n → M), ∀ (j : Fin n), (zgrEv D ⋯ X).IsHom (dβ j) (β j) ∧ (grEv W ⋯ D X).IsHom (wβ j) (β j)

A basis of M_X homogeneous for the degree and the mesh weight.

The arrow maps shift the coordinate weights

theorem MultiplicativeBasisDeformations.MeshWalk.fA_shiftW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {M : Type} [AddCommGroup M] (W : MeshWt Q M) {y x : V} (a : y ⟶ x) (φ : M →+ ℤ) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c y)) (hm : (gwEv D W y φ).IsHom p m) : (gwEv D W x φ).IsHom (p + φ (W.w a)) ((fA D a) m)

Weight-homogeneous lifts

structure MultiplicativeBasisDeformations.MeshWalk.ModLiftW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) {r : ℕ} (φ : Fin r → M →+ ℤ) (X : V) extends MultiplicativeBasisDeformations.MeshWalk.ModLift T X : Type

A lift of an evaluated module, homogeneous for the coordinate weights.

• n : ℕ
• β : Module.Basis (Fin self.n) (ZMod 2) (CatAlg.Rep D.F0 (meshFam Q c X))
• dβ : Fin self.n → ℤ
• hβ (i : Fin self.n) : (zgrEv D ⋯ X).IsHom (self.dβ i) (self.β i)
• MM : GExt.GMod (galgO T) (Fin self.n → ZMod 4)
• lift : WLift.IsLift self.MM (gmodEv D ⋯ X) (πO T) (WLift.ρF self.β)
• gr : self.MM.gr = WLift.grF self.dβ
• wβ : Fin r → Fin self.n → ℤ
• hβw (i : Fin r) (j : Fin self.n) : (gwEv D W X (φ i)).IsHom (self.wβ i j) (self.β j)
• act_w (i : Fin r) (p q : ℤ) (m : Fin self.n → ZMod 4) (b : ↥(P.Lin (ZMod 4))) : (WLift.grF (self.wβ i)).IsHom p m → (galgOW hv hv_mul hv_e (φ i)).gr.IsHom q b → (WLift.grF (self.wβ i)).IsHom (p + q) ((self.MM.act m) b)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_modLiftW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) {r : ℕ} (φ : Fin r → M →+ ℤ) (J : D.InjData) (h1 : DegOne D) (X : V) : Nonempty (ModLiftW T W hv hv_mul hv_e φ X)

Proposition 10.1, the module lifts, weight-homogeneous: for a mesh weight lifting the ray weights, every evaluated module lifts with an action homogeneous for the degree and for every coordinate of the weight.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_arrowLiftW {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R : Type} [Fintype R] [DecidableEq R] {P : RaySys.Mult D.PV R} (T : TabIso D P) {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hv : R → M) (hv_mul : ∀ (a b t : R), P.mul a b = some t → hv t = hv a + hv b) (hv_e : ∀ (x : D.PV), hv (P.e x) = 0) (hΘ : ∀ (a : R), (grA0 W ⋯ D).IsHom (hv a) (T.Θ (P.b (ZMod 2) a))) {r : ℕ} (φ : Fin r → M →+ ℤ) (J : D.InjData) (h1 : DegOne D) (N : (X : V) → ModLiftW T W hv hv_mul hv_e φ X) {y x : V} (a : y ⟶ x) : ∃ (f : (Fin (N y).n → ZMod 4) →ₗ[ZMod 4] Fin (N x).n → ZMod 4), (∀ (m : Fin (N y).n → ZMod 4) (b : ↥(P.Lin (ZMod 4))), f (((N y).MM.act m) b) = ((N x).MM.act (f m)) b) ∧ (∀ (m : Fin (N y).n → ZMod 4), (WLift.ρF (N x).β) (f m) = (fA D a) ((WLift.ρF (N y).β) m)) ∧ (∀ (p : ℤ) (m : Fin (N y).n → ZMod 4), (N y).MM.gr.IsHom p m → (N x).MM.gr.IsHom (p + 1) (f m)) ∧ ∀ (i : Fin r) (p : ℤ) (m : Fin (N y).n → ZMod 4), (WLift.grF ((N y).wβ i)).IsHom p m → (WLift.grF ((N x).wβ i)).IsHom (p + (φ i) (W.w a)) (f m)

Proposition 10.1, the arrow lifts, weight-homogeneous: the arrow maps lift to maps of degree one, homogeneous of the weight of the arrow for every coordinate.