Homogeneous lifts of morphisms at t = 1 (Proposition 12.8, morphisms)

deformation-refinements.tex: "after lifting a homogeneous map of degree r ≥ 0 through correction degrees less than q, its next linearity defect is a one-cocycle of degree r + q. The positive Ext¹ vanishing removes it with the chosen right inverse."

At the fibre t = 1 a morphism φ of C of degree r and weight ρ lifts to a morphism of the lifted modules of order r, with leading term φ, all of whose components have relative weights in the cone, and whose component of relative weight 0 is φ itself (exists_liftHom).

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.Ls1 {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] {μ : 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] : Lifts D hfin (famPF H 1)

The lifted modules at the fibre t = 1.

theorem MultiplicativeBasisDeformations.MeshWalk.famAct_one_ν {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] {μ : 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] (X : V) (n : ℕ) : (famAct H W hχ J h1 hco 1 X).ν n = (act1 H W hχ J h1 hco X).ν n

theorem MultiplicativeBasisDeformations.MeshWalk.famAct_one_tot {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] {μ : 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] (X : V) : (famAct H W hχ J h1 hco 1 X).tot = (act1 H W hχ J h1 hco X).tot

theorem MultiplicativeBasisDeformations.MeshWalk.Ls1_act {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] {μ : 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] (X : V) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (x : Fib (famAM H 1)) : (((Ls1 H W hχ J h1 hco).L X).act m) x = ((act1 H W hχ J h1 hco X).tot m) ((Fib.toΛ (famAM H 1)) x)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_liftHom {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] {μ : 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] {y x : V} (r : ℕ) (ρ : Wt) (φ : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c x) (hφd : φ ∈ ScalarMeshCategory.degreePart c r y x) (hφw : φ ∈ wP c W ρ y x) : ∃ (g : FB (Ls1 H W hχ J h1 hco) y ⟶ FB (Ls1 H W hχ J h1 hco) x), GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑r) (toLin g) ∧ (gmodEv D hfin y).gr.comp (gmodEv D hfin x).gr (↑r) (toLin g) = rs D φ ∧ MGr.ConeLin ρ (toLin g) ∧ MGr.clin ⊥ (grEv W hfin D y) (grEv W hfin D x) ρ (toLin g) = rs D φ

A homogeneous morphism of C lifts at t = 1 with homogeneous corrections.