Lifted mesh sequences over a positive deformation (toward Corollary 12.1)

deformation-refinements.tex (cor:positive-deformation-completeness). Let B be a positive filtered deformation of A₀ and M_X^B the filtered lifts of the evaluated modules (Proposition 6.5). Lifting the mesh maps gives, at a nonprojective x, a surjection π : ⊕_a M_{y_a}^B → M_x^B whose leading term is the graded mesh map, with kernel the image of an injective B-linear map M_{τx}^B → ⊕_a M_{y_a}^B (the kernel is a filtered lift of M_{τx}, by uniqueness of lifts); at a projective x, π is injective. These are the lifted almost split sequences of ind(mod B).

structure MultiplicativeBasisDeformations.MeshWalk.Lifts {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)) {B : Type u} [Ring B] [Algebra k B] (P : PosFiltration (lenA0 D hfin) B) : Type u

Filtered lifts of all evaluated modules (Proposition 6.5(1)).

• L (X : V) : P.FLift ⋯ (gmodEv D hfin X)

theorem MultiplicativeBasisDeformations.MeshWalk.nonempty_lifts {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)] {B : Type u} [Ring B] [Algebra k B] (P : PosFiltration (lenA0 D hfin) B) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) : Nonempty (Lifts D hfin P)

The lifted mesh maps

theorem MultiplicativeBasisDeformations.MeshWalk.rs_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)] {X Y : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (rs D f) (((gmodEv D hfin X).act m) a) = ((gmodEv D hfin Y).act ((rs D f) m)) a

theorem MultiplicativeBasisDeformations.MeshWalk.exists_pLift {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (a : D.Mid x) : ∃ (g : CatAlg.Rep D.F0 (meshFam Q c (D.mid x a)) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)), (∀ (m : CatAlg.Rep D.F0 (meshFam Q c (D.mid x a))) (b : B), g (((Ls.L (D.mid x a)).act m) b) = ((Ls.L x).act (g m)) b) ∧ GExt.OrderGe (gmodEv D hfin (D.mid x a)) (gmodEv D hfin x) 1 g ∧ (gmodEv D hfin (D.mid x a)).gr.comp (gmodEv D hfin x).gr 1 g = rs D (D.p x a)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.pL {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (a : D.Mid x) : CatAlg.Rep D.F0 (meshFam Q c (D.mid x a)) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)

The lifted arrow maps p̃_a : M_{y_a}^B → M_x^B.

theorem MultiplicativeBasisDeformations.MeshWalk.pL_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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (a : D.Mid x) (m : CatAlg.Rep D.F0 (meshFam Q c (D.mid x a))) (b : B) : (pL Ls J h1 Vx x a) (((Ls.L (D.mid x a)).act m) b) = ((Ls.L x).act ((pL Ls J h1 Vx x a) m)) b

theorem MultiplicativeBasisDeformations.MeshWalk.pL_order {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (a : D.Mid x) : GExt.OrderGe (gmodEv D hfin (D.mid x a)) (gmodEv D hfin x) 1 (pL Ls J h1 Vx x a)

theorem MultiplicativeBasisDeformations.MeshWalk.pL_lead {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (a : D.Mid x) : (gmodEv D hfin (D.mid x a)).gr.comp (gmodEv D hfin x).gr 1 (pL Ls J h1 Vx x a) = rs D (D.p x a)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.LE {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)} {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (x : V) : P.FLift ⋯ (gE D hfin x)

The lift on the middle term ⊕_a M_{y_a}⟨1⟩.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.πB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) : Emid D x →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)

The lifted mesh map π = Σ_a p̃_a : ⊕_a M_{y_a}^B → M_x^B.

theorem MultiplicativeBasisDeformations.MeshWalk.πB_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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (m : Emid D x) (b : B) : (πB Ls J h1 Vx x) (((LE Ls x).act m) b) = ((Ls.L x).act ((πB Ls J h1 Vx x) m)) b

theorem MultiplicativeBasisDeformations.MeshWalk.πB_order {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) : GExt.OrderGe (gE D hfin x) (gmodEv D hfin x) 0 (πB Ls J h1 Vx x)

theorem MultiplicativeBasisDeformations.MeshWalk.πB_lead {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) : (gE D hfin x).gr.comp (gmodEv D hfin x).gr 0 (πB Ls J h1 Vx x) = ↑k (πE D x)

Exactness of the lifted mesh sequences

theorem MultiplicativeBasisDeformations.MeshWalk.πE_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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x : V) (hx : ¬D.proj x) : Function.Surjective ⇑(πE D x)

The graded mesh map is onto at a nonprojective label.

theorem MultiplicativeBasisDeformations.MeshWalk.πB_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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (hx : ¬D.proj x) : Function.Surjective ⇑(πB Ls J h1 Vx x)

theorem MultiplicativeBasisDeformations.MeshWalk.πB_injective {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (hx : D.proj x) : Function.Injective ⇑(πB Ls J h1 Vx x)

theorem MultiplicativeBasisDeformations.MeshWalk.finrank_graded {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x : V) (hx : ¬D.proj x) : Module.finrank k (CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx))) + Module.finrank k (CatAlg.Rep D.F0 (meshFam Q c x)) = Module.finrank k (Emid D x)

The graded dimension count dim M_{τx} + dim M_x = dim ⊕_a M_{y_a}.

structure MultiplicativeBasisDeformations.MeshWalk.KerData {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (hx : ¬D.proj x) : Type u

The lifted kernel: M_{τx}^B as the kernel of the lifted mesh map.

• q : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx)) →ₗ[k] Emid D x
• act (m : CatAlg.Rep D.F0 (meshFam Q c (D.tau x hx))) (b : B) : self.q (((Ls.L (D.tau x hx)).act m) b) = ((LE Ls x).act (self.q m)) b
• inj : Function.Injective ⇑self.q
• range : self.q.range = (πB Ls J h1 Vx x).ker

theorem MultiplicativeBasisDeformations.MeshWalk.nonempty_kerData {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (x : V) (hx : ¬D.proj x) : Nonempty (KerData Ls J h1 Vx x hx)

Radical maps factor through the lifted arrows

theorem MultiplicativeBasisDeformations.MeshWalk.orderGe_eq_zero_of_large {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)] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {MM : GExt.GMod (galgA0 D hfin) M} {NN : GExt.GMod (galgA0 D hfin) N} {r : ℤ} {g : M →ₗ[k] N} (hg : GExt.OrderGe MM NN r g) (hr : ↑(GExt.degBound MM.gr) + ↑(GExt.degBound NN.gr) < r) : g = 0

theorem MultiplicativeBasisDeformations.MeshWalk.degProj_comp_right' {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} {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)] {p r : ℕ} {x y z : V} (f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y) {h : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c z} (hh : h ∈ ScalarMeshCategory.degreePart c p y z) : (ScalarMeshCategory.degProj c (r + p) x z) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((ScalarMeshCategory.degProj c r x y) f) h

theorem MultiplicativeBasisDeformations.MeshWalk.exists_factor_πB {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)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (J : D.InjData) (h1 : DegOne D) (Vx : (lenA0 D hfin).Vertices) (hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y) (w x : V) (f : CatAlg.Rep D.F0 (meshFam Q c w) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)) (hf : ∀ (m : CatAlg.Rep D.F0 (meshFam Q c w)) (b : B), f (((Ls.L w).act m) b) = ((Ls.L x).act (f m)) b) (hord : GExt.OrderGe (gmodEv D hfin w) (gmodEv D hfin x) 1 f) : ∃ (g : (a : D.Mid x) → CatAlg.Rep D.F0 (meshFam Q c w) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c (D.mid x a))), (∀ (a : D.Mid x) (m : CatAlg.Rep D.F0 (meshFam Q c w)) (b : B), (g a) (((Ls.L w).act m) b) = ((Ls.L (D.mid x a)).act ((g a) m)) b) ∧ f = ∑ a : D.Mid x, pL Ls J h1 Vx x a ∘ₗ g a

Radical maps into a lift factor through the lifted arrows (the lifted form of MeshData.image, by induction along the finite filtration).