Evaluation of linear paths and its first-order deformation, over any ring

Given modules N_X over a commutative ring R and maps φ_a : N_y → N_x for the arrows of a translation quiver, a path evaluates to the composite of the arrow maps (evP), extended linearly to RQ (evL). Arrow corrections g_a give the ε-part δ of the evaluation of φ + εg (δp, δL), a derivation (δL_comp). When the mesh relations hold for φ (evL_ideal), and also to first order (δL_ideal), both kill the mesh ideal.

This is the ring-generic part of the proof of Proposition 7.6 (PsiInjective), used over ℤ/4 for Lemma 10.2 (integral-deformations.tex).

@[irreducible]

def MultiplicativeBasisDeformations.PathEval.evP {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} : Quiver.Path Y X → N Y →ₗ[R] N X

The evaluation of a path.

theorem MultiplicativeBasisDeformations.PathEval.evP_nil {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) (Y : V) : evP N (fun {y x : V} => φ) Quiver.Path.nil = LinearMap.id

theorem MultiplicativeBasisDeformations.PathEval.evP_cons {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X Z : V} (p : Quiver.Path Y X) (a : X ⟶ Z) : evP N (fun {y x : V} => φ) (p.cons a) = φ a ∘ₗ evP N (fun {y x : V} => φ) p

theorem MultiplicativeBasisDeformations.PathEval.evP_comp {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} (p : Quiver.Path Y X) {Z : V} (p' : Quiver.Path X Z) : evP N (fun {y x : V} => φ) (p.comp p') = evP N (fun {y x : V} => φ) p' ∘ₗ evP N (fun {y x : V} => φ) p

theorem MultiplicativeBasisDeformations.PathEval.evP_toPath {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} (a : Y ⟶ X) : evP N (fun {y x : V} => φ) a.toPath = φ a

noncomputable def MultiplicativeBasisDeformations.PathEval.evL {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} : (LinearPaths.obj Y ⟶ LinearPaths.obj X) →ₗ[R] N Y →ₗ[R] N X

The linear extension of evP to the morphisms of RQ.

theorem MultiplicativeBasisDeformations.PathEval.evL_path {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} (p : Quiver.Path Y X) : (evL N fun {y x : V} => φ) (LinearPaths.path p) = evP N (fun {y x : V} => φ) p

theorem MultiplicativeBasisDeformations.PathEval.evL_id {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) (Y : V) : (evL N fun {y x : V} => φ) (CategoryTheory.CategoryStruct.id (LinearPaths.obj Y)) = LinearMap.id

theorem MultiplicativeBasisDeformations.PathEval.rq_induction {R : Type u} [CommRing R] {V : Type} [Quiver V] {Y X : V} {P : (LinearPaths.obj Y ⟶ LinearPaths.obj X) → Prop} (h0 : P 0) (hadd : ∀ (F G : LinearPaths.obj Y ⟶ LinearPaths.obj X), P F → P G → P (F + G)) (hsmul : ∀ (t : R) (F : LinearPaths.obj Y ⟶ LinearPaths.obj X), P F → P (t • F)) (hpath : ∀ (p : Quiver.Path Y X), P (LinearPaths.path p)) (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : P F

theorem MultiplicativeBasisDeformations.PathEval.evL_comp {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X Z : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (G : LinearPaths.obj X ⟶ LinearPaths.obj Z) : (evL N fun {y x : V} => φ) (CategoryTheory.CategoryStruct.comp F G) = (evL N fun {y x : V} => φ) G ∘ₗ (evL N fun {y x : V} => φ) F

The mesh ideal

theorem MultiplicativeBasisDeformations.PathEval.evL_meshRelation {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients R Q) (x : ↑Q.nonprojective) : (evL N fun {y x : V} => φ) (meshRelation u x) = ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • φ a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd)

theorem MultiplicativeBasisDeformations.PathEval.mem_ideal_induction {R : Type u} [CommRing R] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (u : MeshCoefficients R Q) {Y X : V} {M : Type u_1} [AddCommGroup M] [Module R M] (T : (LinearPaths.obj Y ⟶ LinearPaths.obj X) →ₗ[R] M) (hT : ∀ (x : ↑Q.nonprojective) (a : LinearPaths.obj Y ⟶ LinearPaths.obj ↑(Q.tau x)) (b : LinearPaths.obj ↑x ⟶ LinearPaths.obj X), T (CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (meshRelation u x) b)) = 0) {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : F ∈ (CategoricalIdeal.HomIdeal.linearSpan R (meshRelations u)).hom (LinearPaths.obj Y) (LinearPaths.obj X)) : T F = 0

The ideal induction for the mesh ideal: a linear map killing the sandwiches of the mesh relations kills the mesh ideal.

theorem MultiplicativeBasisDeformations.PathEval.evL_ideal {R : Type u} [CommRing R] {V : Type} [Quiver V] {N : V → Type v} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] {φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {u : MeshCoefficients R Q} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • φ a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd) = 0) {Y X : V} {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : F ∈ (CategoricalIdeal.HomIdeal.linearSpan R (meshRelations u)).hom (LinearPaths.obj Y) (LinearPaths.obj X)) : (evL N fun {y x : V} => φ) F = 0

When the mesh relations hold, the evaluation kills the mesh ideal.

The first-order part

@[irreducible]

def MultiplicativeBasisDeformations.PathEval.δp {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} : Quiver.Path Y X → N Y →ₗ[R] N X

The ε-part of the evaluation of φ + εg on a path: δ(p a) = φ_a δ(p) + g_a ev(p).

theorem MultiplicativeBasisDeformations.PathEval.δp_nil {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) (Y : V) : δp N (fun {y x : V} => φ) (fun {y x : V} => g) Quiver.Path.nil = 0

theorem MultiplicativeBasisDeformations.PathEval.δp_cons {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X Z : V} (p : Quiver.Path Y X) (a : X ⟶ Z) : δp N (fun {y x : V} => φ) (fun {y x : V} => g) (p.cons a) = φ a ∘ₗ δp N (fun {y x : V} => φ) (fun {y x : V} => g) p + g a ∘ₗ evP N (fun {y x : V} => φ) p

theorem MultiplicativeBasisDeformations.PathEval.δp_comp {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} (p : Quiver.Path Y X) {Z : V} (p' : Quiver.Path X Z) : δp N (fun {y x : V} => φ) (fun {y x : V} => g) (p.comp p') = evP N (fun {y x : V} => φ) p' ∘ₗ δp N (fun {y x : V} => φ) (fun {y x : V} => g) p + δp N (fun {y x : V} => φ) (fun {y x : V} => g) p' ∘ₗ evP N (fun {y x : V} => φ) p

theorem MultiplicativeBasisDeformations.PathEval.δp_toPath {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} (a : Y ⟶ X) : δp N (fun {y x : V} => φ) (fun {y x : V} => g) a.toPath = g a

noncomputable def MultiplicativeBasisDeformations.PathEval.δL {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} : (LinearPaths.obj Y ⟶ LinearPaths.obj X) →ₗ[R] N Y →ₗ[R] N X

The linear extension of δp.

theorem MultiplicativeBasisDeformations.PathEval.δL_path {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X : V} (p : Quiver.Path Y X) : (δL N (fun {y x : V} => φ) fun {y x : V} => g) (LinearPaths.path p) = δp N (fun {y x : V} => φ) (fun {y x : V} => g) p

theorem MultiplicativeBasisDeformations.PathEval.δL_id {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) (Y : V) : (δL N (fun {y x : V} => φ) fun {y x : V} => g) (CategoryTheory.CategoryStruct.id (LinearPaths.obj Y)) = 0

theorem MultiplicativeBasisDeformations.PathEval.δL_comp {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Y X Z : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) (G : LinearPaths.obj X ⟶ LinearPaths.obj Z) : (δL N (fun {y x : V} => φ) fun {y x : V} => g) (CategoryTheory.CategoryStruct.comp F G) = (evL N fun {y x : V} => φ) G ∘ₗ (δL N (fun {y x : V} => φ) fun {y x : V} => g) F + (δL N (fun {y x : V} => φ) fun {y x : V} => g) G ∘ₗ (evL N fun {y x : V} => φ) F

δ is a derivation.

theorem MultiplicativeBasisDeformations.PathEval.δL_meshRelation {R : Type u} [CommRing R] {V : Type} [Quiver V] (N : V → Type v) [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] (φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {u : MeshCoefficients R Q} (g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x) (x : ↑Q.nonprojective) : (δL N (fun {y x : V} => φ) fun {y x : V} => g) (meshRelation u x) = ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • (φ a.snd ∘ₗ g ((Q.mate x a.fst) a.snd) + g a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd))

theorem MultiplicativeBasisDeformations.PathEval.δL_ideal {R : Type u} [CommRing R] {V : Type} [Quiver V] {N : V → Type v} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] {φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {u : MeshCoefficients R Q} {g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} (hmesh : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • φ a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd) = 0) (hz : ∀ (x : ↑Q.nonprojective), ∑ a : (y : V) × (y ⟶ ↑x), ↑(u x a.fst a.snd) • (φ a.snd ∘ₗ g ((Q.mate x a.fst) a.snd) + g a.snd ∘ₗ φ ((Q.mate x a.fst) a.snd)) = 0) {Y X : V} {F : LinearPaths.obj Y ⟶ LinearPaths.obj X} (hF : F ∈ (CategoricalIdeal.HomIdeal.linearSpan R (meshRelations u)).hom (LinearPaths.obj Y) (LinearPaths.obj X)) : (δL N (fun {y x : V} => φ) fun {y x : V} => g) F = 0

When the mesh relations hold to first order, δ kills the mesh ideal.

Lifted maps

theorem MultiplicativeBasisDeformations.PathEval.isLiftHom_id' {R : Type u} [CommRing R] {V : Type} [Quiver V] {N : V → Type v} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Λ : Type u_1} [Ring Λ] [Algebra R Λ] {GΛ : GExt.GAlg Λ} {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : (X : V) → GExt.GMod GΛ (N X)} (Lf : (X : V) → GExt.ActLift μ q (MM X)) (Y : V) : GExt.IsLiftHom (Lf Y) (Lf Y) LinearMap.id 0

theorem MultiplicativeBasisDeformations.PathEval.isLiftHom_zero' {R : Type u} [CommRing R] {V : Type} [Quiver V] {N : V → Type v} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Λ : Type u_1} [Ring Λ] [Algebra R Λ] {GΛ : GExt.GAlg Λ} {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : (X : V) → GExt.GMod GΛ (N X)} (Lf : (X : V) → GExt.ActLift μ q (MM X)) {Y X : V} : GExt.IsLiftHom (Lf Y) (Lf X) 0 0

theorem MultiplicativeBasisDeformations.PathEval.δp_lift {R : Type u} [CommRing R] {V : Type} [Quiver V] {N : V → Type v} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] {φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} {Λ : Type u_1} [Ring Λ] [Algebra R Λ] {GΛ : GExt.GAlg Λ} {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : (X : V) → GExt.GMod GΛ (N X)} {Lf : (X : V) → GExt.ActLift μ q (MM X)} (hφ : ∀ {y x : V} (a : y ⟶ x), GExt.IsLiftHom (Lf y) (Lf x) (φ a) (g a)) {Y X : V} (p : Quiver.Path Y X) : GExt.IsLiftHom (Lf Y) (Lf X) (evP N (fun {y x : V} => φ) p) (δp N (fun {y x : V} => φ) (fun {y x : V} => g) p)

theorem MultiplicativeBasisDeformations.PathEval.δL_lift {R : Type u} [CommRing R] {V : Type} [Quiver V] {N : V → Type v} [(X : V) → AddCommGroup (N X)] [(X : V) → Module R (N X)] {φ : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {g : {y x : V} → (y ⟶ x) → N y →ₗ[R] N x} {Λ : Type u_1} [Ring Λ] [Algebra R Λ] {GΛ : GExt.GAlg Λ} {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} {MM : (X : V) → GExt.GMod GΛ (N X)} {Lf : (X : V) → GExt.ActLift μ q (MM X)} (hφ : ∀ {y x : V} (a : y ⟶ x), GExt.IsLiftHom (Lf y) (Lf x) (φ a) (g a)) {Y X : V} (F : LinearPaths.obj Y ⟶ LinearPaths.obj X) : GExt.IsLiftHom (Lf Y) (Lf X) ((evL N fun {y x : V} => φ) F) ((δL N (fun {y x : V} => φ) fun {y x : V} => g) F)