The lifted modules and arrows over ℤ/4 (Proposition 10.1)

integral-deformations.tex: "Lift the action matrices arbitrarily to free graded 𝒪-modules. […] Equation (prime-field-ext-vanishing) supplies a correction. […] The same bar calculation, using Ext¹, gives uniqueness and lifts all homogeneous maps of nonnegative degree."

Every evaluated module M_X of A⁽²⁾ lifts to a graded 𝒪P-module on Fin n_X → 𝒪 (exists_modLift), and every arrow map M_y → M_x lifts to a degree-one 𝒪P-linear map between the lifts (exists_arrowLift). These data are bundled in WData.

Linear lifts between free lifts

noncomputable def MultiplicativeBasisDeformations.WLift.linLift {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup N] [Module (ZMod 2) N] {ι : Type u_4} {κ : Type u_5} [Fintype ι] (β : Module.Basis ι (ZMod 2) M) (γ : Module.Basis κ (ZMod 2) N) (f : M →ₗ[ZMod 2] N) : (ι → ZMod 4) →ₗ[ZMod 4] κ → ZMod 4

The coordinatewise lift of a 𝔽₂-linear map between free lifts.

theorem MultiplicativeBasisDeformations.WLift.linLift_apply {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup N] [Module (ZMod 2) N] {ι : Type u_4} {κ : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (β : Module.Basis ι (ZMod 2) M) (γ : Module.Basis κ (ZMod 2) N) (f : M →ₗ[ZMod 2] N) (m : ι → ZMod 4) : (linLift β γ f) m = ∑ i : ι, m i • lv γ (f (β i))

theorem MultiplicativeBasisDeformations.WLift.ρF_linLift {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup N] [Module (ZMod 2) N] {ι : Type u_4} {κ : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (β : Module.Basis ι (ZMod 2) M) (γ : Module.Basis κ (ZMod 2) N) (f : M →ₗ[ZMod 2] N) (m : ι → ZMod 4) : (ρF γ) ((linLift β γ f) m) = f ((ρF β) m)

theorem MultiplicativeBasisDeformations.WLift.linLift_isHom {Λ : Type u_1} [Ring Λ] [Algebra (ZMod 2) Λ] {GΛ : GExt.GAlg Λ} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module (ZMod 2) M] [AddCommGroup N] [Module (ZMod 2) N] {ι : Type u_4} {κ : Type u_5} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (β : Module.Basis ι (ZMod 2) M) (γ : Module.Basis κ (ZMod 2) N) (dβ : ι → ℤ) (dγ : κ → ℤ) {MM : GExt.GMod GΛ M} {NN : GExt.GMod GΛ N} (hβ : ∀ (i : ι), MM.gr.IsHom (dβ i) (β i)) (hγ : ∀ (j : κ), NN.gr.IsHom (dγ j) (γ j)) (f : M →ₗ[ZMod 2] N) {d : ℤ} (hf : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + d) (f m)) {p : ℤ} {m : ι → ZMod 4} (hm : (grF dβ).IsHom p m) : (grF dγ).IsHom (p + d) ((linLift β γ f) m)

structure MultiplicativeBasisDeformations.MeshWalk.ModLift {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) (X : V) : Type

A lift of an evaluated module M_X to a free graded 𝒪P-module.

• 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β

theorem MultiplicativeBasisDeformations.MeshWalk.exists_modLift {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) (J : D.InjData) (h1 : DegOne D) (X : V) : Nonempty (ModLift T X)

Proposition 10.1, the module lifts (prop:fixed-integral-companion).

theorem MultiplicativeBasisDeformations.MeshWalk.exists_arrowLift {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) (J : D.InjData) (h1 : DegOne D) (N : (X : V) → ModLift T X) {y x : V} (a : y ⟶ x) : ∃ (φ : (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))), φ (((N y).MM.act m) b) = ((N x).MM.act (φ m)) b) ∧ (∀ (m : Fin (N y).n → ZMod 4), (WLift.ρF (N x).β) (φ 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) (φ m)

Proposition 10.1, the arrow lifts: the arrow maps lift to degree-one maps.

structure MultiplicativeBasisDeformations.MeshWalk.WData {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) : Type

The lifted modules and arrows.

• N (X : V) : ModLift T X
• φ {y x : V} : (y ⟶ x) → (Fin (self.N y).n → ZMod 4) →ₗ[ZMod 4] Fin (self.N x).n → ZMod 4
• φ_act {y x : V} (a : y ⟶ x) (m : Fin (self.N y).n → ZMod 4) (b : ↥(P.Lin (ZMod 4))) : (self.φ a) (((self.N y).MM.act m) b) = ((self.N x).MM.act ((self.φ a) m)) b
• φ_red {y x : V} (a : y ⟶ x) (m : Fin (self.N y).n → ZMod 4) : (WLift.ρF (self.N x).β) ((self.φ a) m) = (fA D a) ((WLift.ρF (self.N y).β) m)
• φ_deg {y x : V} (a : y ⟶ x) (p : ℤ) (m : Fin (self.N y).n → ZMod 4) : (self.N y).MM.gr.IsHom p m → (self.N x).MM.gr.IsHom (p + 1) ((self.φ a) m)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_wData {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) (J : D.InjData) (h1 : DegOne D) : Nonempty (WData T)