The mesh presentation of every fibre (Proposition 12.8, presentations) #
deformation-refinements.tex: "Let ℬ be that mesh presentation with a path cutoff
above the top degree of C. Its arrow map to ℳ is surjective by degree induction. Leading
relations give surjections C ⊗ K → gr ℬ → gr ℳ = C ⊗ K whose composite fixes every arrow and
object, hence is the identity. Both maps are isomorphisms."
At each fibre t, the twisted lifted arrows realize kQ onto the morphisms of the lifted modules
(realize_tw_surjective, by degree induction on leading terms).
Twisting, orders and leading terms #
theorem
MultiplicativeBasisDeformations.MeshWalk.twl_orderGe
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{coords : Wt →+ I → ℤ}
[Infinite k]
{y x : V}
(t : I → k)
(ρ : Wt)
{r : ℤ}
{u : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(hu : GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r u)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.comp_twl
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{coords : Wt →+ I → ℤ}
[Infinite k]
{y x : V}
(t : I → k)
(ρ : Wt)
(r : ℤ)
(u : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.twl_of_shift
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{coords : Wt →+ I → ℤ}
{y x : V}
(t : I → k)
{ρ : Wt}
{f : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(hf : (grEv W hfin D y).Shift (grEv W hfin D x) ρ f)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.pathR_tw_props
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
(p : Quiver.Path y x)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑p.length) (toLin (PathReal.pathR (fun {y x : V} => twArrow A t) p)) ∧ (gmodEv D hfin y).gr.comp (gmodEv D hfin x).gr (↑p.length) (toLin (PathReal.pathR (fun {y x : V} => twArrow A t) p)) = rs D (ScalarMeshCategory.pathMor c p)
Twisted paths: order and leading term.
theorem
MultiplicativeBasisDeformations.MeshWalk.realize_tw_props
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
{r : ℕ}
{F : LinearPaths.obj y ⟶ LinearPaths.obj x}
(hF : F ∈ LinearPaths.degreePart r y x)
:
Twisted realizations of homogeneous morphisms of kQ: order and leading term.
Surjectivity #
theorem
MultiplicativeBasisDeformations.MeshWalk.realize_tw_surjective
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
(f : FB (famLifts H W hχ J h1 hco t) y ⟶ FB (famLifts H W hχ J h1 hco t) x)
:
∃ (F : LinearPaths.obj y ⟶ LinearPaths.obj x), (PathReal.realizeR k (fun {y x : V} => twArrow A t) y x) F = f
The twisted arrows generate: every morphism of the lifted modules of the fibre t is
realized by a morphism of kQ.
The kernel: the perturbed mesh ideal #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.ftp
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{I : Type}
[Fintype I]
(Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(lam t : I → k)
(x : V)
(tt : (FlatPert.meshPres c).T x)
:
FlatPert.Hm k ((FlatPert.meshPres c).src x tt) x
The retained perturbation at the fibre t: f_x = Σ_i λ_i t_i R_i.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.ftp_mem
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(hlen : ∀ (i : I), (Rw i).snd.length = qd i + 2)
(hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i)
(lam t : I → k)
(x : V)
(tt : (FlatPert.meshPres c).T x)
:
ftp Rw lam t x tt ∈ FlatPert.geSpan k ((FlatPert.meshPres c).deg x tt + 1) ((FlatPert.meshPres c).src x tt) x
theorem
MultiplicativeBasisDeformations.MeshWalk.ker_img
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(y x : V)
:
(CategoryTheory.Functor.mapLinearMap k (RelationCategory.functor k (meshRelations c))).ker = FlatPert.ctxSpan (FlatPert.meshPres c) (FlatPert.meshPres c).r y x
The kernel of kQ → C is the mesh ideal.
theorem
MultiplicativeBasisDeformations.MeshWalk.finrank_idealC
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
(y x : V)
:
Module.finrank k (FlatPert.Q (FlatPert.idealC (FlatPert.meshPres c)) y x) = Module.finrank k (ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c x)
theorem
MultiplicativeBasisDeformations.MeshWalk.realize_tw_ker
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{c : MeshCoefficients k Q}
{L : CatAlg.LocalFamily (meshFam Q c)}
{D : CatAlg.MeshData (meshFam Q c) L}
{hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
{qd : I → ℕ}
{H : FamHyp D hfin μ qd}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{coords : Wt →+ I → ℤ}
{hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)}
{J : D.InjData}
{h1 : DegOne D}
{hco : ∀ (i : I), coords (χ i) = Pi.single i 1}
[Infinite k]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(hlen : ∀ (i : I), (Rw i).snd.length = qd i + 2)
(hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i)
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
(hA : ∀ (x : ↑Q.nonprojective), errE Rw A lam x = 0)
(t : I → k)
(N : ℕ)
(hN1 : Nb hfin ≤ N)
(hN2 : ∀ (X Y : V), GExt.degBound (gmodEv D hfin X).gr + GExt.degBound (gmodEv D hfin Y).gr < N + 1)
{y x : V}
(F : FlatPert.Hm k y x)
:
(PathReal.realizeR k (fun {y x : V} => twArrow A t) y x) F = 0 ↔ F ∈ (FlatPert.idealB (FlatPert.meshPres c) (ftp Rw lam t) ⋯ N).I y x
The presentation of each fibre: the realization by the twisted arrows has kernel exactly
(𝔪^{N+1}, r_x − Σ_i λ_i t_i R_i) (N beyond the degrees).