Lemma 4.8: evaluation of lifted objects is fully faithful

lem:lifted-projective-evaluation (scalar-normalization.tex). For a lifted object X̃ put V_X̃(z) = C̃(P_z, X̃) on the lifted projective vertices z. "By eq:walk-hom-sum, for each projective label x, C(P_x, X) = ⊕_g V_X̃(g x̃). Thus ev(X) is the direct sum of the components of V_X̃ […]. A map φ : V_X̃ → V_Ỹ of L-modules therefore defines an A₀-module map ev(X) → ev(Y) […]. By Proposition 2.10, this map is ev(f) for a unique f ∈ C(X, Y). […] write f = Σ_g f̄_g […] ev(f̄_g) maps the component at z̃ to the component at g⁻¹ z̃. The deck action is free, so for g ≠ 1 these blocks are off the diagonal, where ev(f) vanishes. Hence ev(f̄_g) = 0 for g ≠ 1. Faithfulness of ev gives f̄_g = 0 […]. Thus f = f̄_1 […]; this proves fullness. If the evaluation of f ∈ C̃(X̃, Ỹ) is zero, then the image of f in C(X, Y) is killed by ev; the same two facts give f = 0, proving faithfulness."

Here the cover is the graded covering category of a G-graded family with mesh data: a lifted object is (X, h), a lifted projective vertex is z = (p, g) with p projective, and V_X̃(z) is the degree g⁻¹h part of C(P_p, X). A map V_X̃ → V_Ỹ of modules over the lifted projectives is a natural family (NatFam); the deck degree g of f̄_g is relative to the sheets of X̃ and Ỹ.

noncomputable def MultiplicativeBasisDeformations.CatAlg.HomGrading.degs {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (Dg : HomGrading F G) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] : Finset G

All degrees occurring between labels.

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.proj_eq_zero_of_not_mem {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (Dg : HomGrading F G) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {g : G} (hg : g ∉ Dg.degs) {x y : ι} (f : F x ⟶ F y) : (Dg.proj g x y) f = 0

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.eq_zero_of_not_mem {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (Dg : HomGrading F G) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {g : G} (hg : g ∉ Dg.degs) {x y : ι} {f : F x ⟶ F y} (hf : Dg.IsHom g f) : f = 0

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.eq_sum_degs {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (Dg : HomGrading F G) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {x y : ι} (f : F x ⟶ F y) : f = ∑ g ∈ Dg.degs, (Dg.proj g x y) f

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.proj_comp_left {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (Dg : HomGrading F G) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {a c : G} {x y z : ι} {m : F x ⟶ F y} (hm : Dg.IsHom a m) (f : F y ⟶ F z) : (Dg.proj c x z) (CategoryTheory.CategoryStruct.comp m f) = CategoryTheory.CategoryStruct.comp m ((Dg.proj (a⁻¹ * c) y z) f)

Projection after a homogeneous morphism.

structure MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} (D : MeshData F L) (Dg : HomGrading F G) (X Y : ι × G) : Type w

A map V_X̃ → V_Ỹ of modules over the lifted projectives: a natural family of maps C̃(P_z, X̃) → C̃(P_z, Ỹ), z = (p, g).

• φ (z : D.PV × G) : (F ↑z.1 ⟶ F X.1) →ₗ[k] F ↑z.1 ⟶ F Y.1
• mem (z : D.PV × G) (m : F ↑z.1 ⟶ F X.1) : m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1 → (self.φ z) m ∈ Dg.part (z.2⁻¹ * Y.2) (↑z.1) Y.1
• nat (z z' : D.PV × G) (u : F ↑z'.1 ⟶ F ↑z.1) (m : F ↑z.1 ⟶ F X.1) : u ∈ Dg.part (z'.2⁻¹ * z.2) ↑z'.1 ↑z.1 → m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1 → (self.φ z') (CategoryTheory.CategoryStruct.comp u m) = CategoryTheory.CategoryStruct.comp u ((self.φ z) m)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam.term {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} {D : MeshData F L} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Dg : HomGrading F G} {X Y : ι × G} (N : D.NatFam Dg X Y) (p q : D.PV) (a b : G) (μ : F ↑p ⟶ F ↑q) (m : F ↑q ⟶ F X.1) : ∑ e ∈ Dg.degs, (N.φ (p, X.2 * e⁻¹)) ((Dg.proj e (↑p) X.1) (CategoryTheory.CategoryStruct.comp ((Dg.proj a ↑p ↑q) μ) ((Dg.proj b (↑q) X.1) m))) = CategoryTheory.CategoryStruct.comp ((Dg.proj a ↑p ↑q) μ) ((N.φ (q, X.2 * b⁻¹)) ((Dg.proj b (↑q) X.1) m))

The term identity behind the module map.

noncomputable def MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam.Ψ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} {D : MeshData F L} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Dg : HomGrading F G} {X Y : ι × G} (N : D.NatFam Dg X Y) : Rep D.F0 (F X.1) →ₗ[Alg D.F0] Rep D.F0 (F Y.1)

The A₀-module map ev(X) → ev(Y) assembled from the components.

def MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam.single {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} {L : LocalFamily F} {D : MeshData F L} {X : ι × G} (p : D.PV) (m : F ↑p ⟶ F X.1) : Rep D.F0 (F X.1)

A morphism concentrated at one label.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam.Ψ_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} {D : MeshData F L} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Dg : HomGrading F G} {X Y : ι × G} (N : D.NatFam Dg X Y) (m : Rep D.F0 (F X.1)) (p : D.PV) : N.Ψ m p = ∑ e ∈ Dg.degs, (N.φ (p, X.2 * e⁻¹)) ((Dg.proj e (↑p) X.1) (m p))

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam.Ψ_single {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} {D : MeshData F L} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Dg : HomGrading F G} {X Y : ι × G} (N : D.NatFam Dg X Y) (p : D.PV) {e : G} {m : F ↑p ⟶ F X.1} (hm : Dg.IsHom e m) : N.Ψ (single p m) p = (N.φ (p, X.2 * e⁻¹)) m

Ψ on a homogeneous component concentrated at one label.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.NatFam.exists_hom {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} {D : MeshData F L} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Dg : HomGrading F G} {X Y : ι × G} (N : D.NatFam Dg X Y) : ∃ (f : F X.1 ⟶ F Y.1), Dg.IsHom (X.2⁻¹ * Y.2) f ∧ ∀ (z : D.PV × G), ∀ m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1, (N.φ z) m = CategoryTheory.CategoryStruct.comp m f

Lemma 4.8, fullness: a natural family is composition with a morphism X̃ → Ỹ of the cover.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.eq_zero_of_lifted {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {L : LocalFamily F} {D : MeshData F L} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Dg : HomGrading F G} {X Y : ι × G} (f : F X.1 ⟶ F Y.1) (h : ∀ (z : D.PV × G), ∀ m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1, CategoryTheory.CategoryStruct.comp m f = 0) : f = 0

Lemma 4.8, faithfulness: a morphism killed by every lifted projective vertex is zero.