Local families with exact right meshes

The structure of C = gr_J ind(mod A) used in the proof of Proposition 2.10 (graded-category.tex): the positive-degree ideal is the categorical radical, it is nilpotent, each degree-zero endomorphism ring is k, and degree-zero maps between distinct objects vanish (Lemma 2.7); the right mesh map at each label has image the radical (Lemma 2.7), and at a nonprojective label the right mesh is exact in both variables (Proposition 2.6(1)); at a projective label the mesh map is monic (Proposition 2.6(2)).

We record these properties for a finite family of objects of a k-linear category (LocalFamily, MeshData), and derive the module-theoretic consequences over the category algebra Λ.

structure MultiplicativeBasisDeformations.CatAlg.LocalFamily {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] (F : ι → 𝒞) : Type w

A family of objects with local endomorphism rings with residue field k and a nilpotent radical containing all maps between distinct objects.

• rad (x y : ι) : Submodule k (F x ⟶ F y)

  The radical.

• comp_left {x y z : ι} (f : F x ⟶ F y) {g : F y ⟶ F z} : g ∈ self.rad y z → CategoryTheory.CategoryStruct.comp f g ∈ self.rad x z
• comp_right {x y z : ι} {f : F x ⟶ F y} : f ∈ self.rad x y → ∀ (g : F y ⟶ F z), CategoryTheory.CategoryStruct.comp f g ∈ self.rad x z
• mem_of_ne {x y : ι} : x ≠ y → ∀ (f : F x ⟶ F y), f ∈ self.rad x y
• diag (x : ι) (f : F x ⟶ F x) : ∃ (c : k), f - c • CategoryTheory.CategoryStruct.id (F x) ∈ self.rad x x
• id_not_mem (x : ι) : CategoryTheory.CategoryStruct.id (F x) ∉ self.rad x x
• nilpotent (x : ι) (f : CategoryTheory.End (F x)) : f ∈ self.rad x x → IsNilpotent f
• idealNilp : ∃ (N : ℕ), ∀ (l : List (Alg F)), N ≤ l.length → (∀ a ∈ l, ∀ (y z : ι), a y z ∈ self.rad y z) → l.prod = 0

  The radical ideal of Λ is nilpotent.

structure MultiplicativeBasisDeformations.CatAlg.MeshData {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] (F : ι → 𝒞) (L : LocalFamily F) : Type (max 1 w)

The right meshes: at each x, arrows p_a : F (mid a) → F x whose sums of composites give exactly the radical; at a nonprojective x a translate τ x with q_a : F (τ x) → F (mid a), exact in both variables; at a projective x the mesh map is monic.

• Mid : ι → Type
• fin (x : ι) : Fintype (self.Mid x)
• decMid (x : ι) : DecidableEq (self.Mid x)
• mid (x : ι) : self.Mid x → ι
• p (x : ι) (a : self.Mid x) : F (self.mid x a) ⟶ F x
• p_rad (x : ι) (a : self.Mid x) : self.p x a ∈ L.rad (self.mid x a) x
• image (x w : ι) (f : F w ⟶ F x) : f ∈ L.rad w x → ∃ (g : (a : self.Mid x) → F w ⟶ F (self.mid x a)), f = ∑ a : self.Mid x, CategoryTheory.CategoryStruct.comp (g a) (self.p x a)
• proj : ι → Prop
• decProj : DecidablePred self.proj
• tau (x : ι) : ¬self.proj x → ι
• q (x : ι) (hx : ¬self.proj x) (a : self.Mid x) : F (self.tau x hx) ⟶ F (self.mid x a)
• comp_zero (x : ι) (hx : ¬self.proj x) : ∑ a : self.Mid x, CategoryTheory.CategoryStruct.comp (self.q x hx a) (self.p x a) = 0
• cov_exact (x : ι) (hx : ¬self.proj x) (w : ι) (g : (a : self.Mid x) → F w ⟶ F (self.mid x a)) : ∑ a : self.Mid x, CategoryTheory.CategoryStruct.comp (g a) (self.p x a) = 0 → ∃ (z : F w ⟶ F (self.tau x hx)), ∀ (a : self.Mid x), g a = CategoryTheory.CategoryStruct.comp z (self.q x hx a)
• cov_mono (x : ι) (hx : ¬self.proj x) (w : ι) (z : F w ⟶ F (self.tau x hx)) : (∀ (a : self.Mid x), CategoryTheory.CategoryStruct.comp z (self.q x hx a) = 0) → z = 0
• contra_exact (x : ι) (hx : ¬self.proj x) (w : ι) (v : (a : self.Mid x) → F (self.mid x a) ⟶ F w) : ∑ a : self.Mid x, CategoryTheory.CategoryStruct.comp (self.q x hx a) (v a) = 0 → ∃ (u : F x ⟶ F w), ∀ (a : self.Mid x), v a = CategoryTheory.CategoryStruct.comp (self.p x a) u
• contra_mono (x : ι) (hx : ¬self.proj x) (w : ι) (u : F x ⟶ F w) : (∀ (a : self.Mid x), CategoryTheory.CategoryStruct.comp (self.p x a) u = 0) → u = 0
• proj_mono (x : ι) : self.proj x → ∀ (w : ι) (g : (a : self.Mid x) → F w ⟶ F (self.mid x a)), ∑ a : self.Mid x, CategoryTheory.CategoryStruct.comp (g a) (self.p x a) = 0 → ∀ (a : self.Mid x), g a = 0

def MultiplicativeBasisDeformations.CatAlg.LocalFamily.radRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) (x : ι) : Submodule (Alg F) (Rep F (F x))

The radical of R_X.

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.isUnit_of_not_mem {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) {x : ι} {f : CategoryTheory.End (F x)} (hf : f ∉ L.rad x x) : IsUnit f

An endomorphism c 1 + r with c ≠ 0 and r radical is invertible.

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.unit_mem_span {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) {x : ι} {m : Rep F (F x)} (hm : m x ∉ L.rad x x) : unit x ∈ Alg F ∙ m

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.unit_not_mem {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) (x : ι) : unit x ∉ L.radRep x

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.eq_top_of_not_le {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) {x : ι} {N : Submodule (Alg F) (Rep F (F x))} (h : ¬N ≤ L.radRep x) : N = ⊤

R_x is local: a submodule not contained in the radical is everything.

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.isCoatom_radRep {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) (x : ι) : IsCoatom (L.radRep x)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.LocalFamily.Top {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) (x : ι) : Type w

The simple top L_x = R_x / rad R_x.

instance MultiplicativeBasisDeformations.CatAlg.LocalFamily.instIsSimpleModuleAlgTop {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) (x : ι) : IsSimpleModule (Alg F) (L.Top x)

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.sum_idem {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} : ∑ x : ι, idem x = 1

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.iso_top_of_idem {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) {S : Type u_1} [AddCommGroup S] [Module (Alg F) S] [IsSimpleModule (Alg F) S] (x : ι) (s : S) (hx : idem x • s ≠ 0) : Nonempty (S ≃ₗ[Alg F] L.Top x)

A simple module with a nonzero x-part is the top L_x.

theorem MultiplicativeBasisDeformations.CatAlg.LocalFamily.exists_iso_top {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (L : LocalFamily F) {S : Type u_1} [AddCommGroup S] [Module (Alg F) S] [IsSimpleModule (Alg F) S] : ∃ (x : ι), Nonempty (S ≃ₗ[Alg F] L.Top x)

Simple modules are the tops L_x.

def MultiplicativeBasisDeformations.CatAlg.MeshData.meshMap {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) : ((a : D.Mid x) → Rep F (F (D.mid x a))) →ₗ[Alg F] Rep F (F x)

The right mesh map ⊕_a R_{mid a} → R_x.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.meshMap_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (m : (a : D.Mid x) → Rep F (F (D.mid x a))) (y : ι) : (D.meshMap x) m y = ∑ a : D.Mid x, CategoryTheory.CategoryStruct.comp (m a y) (D.p x a)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.range_meshMap {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) : (D.meshMap x).range = L.radRep x

Lemma 2.7: the image of the right mesh map is the radical.

def MultiplicativeBasisDeformations.CatAlg.MeshData.tauMap {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) : Rep F (F (D.tau x hx)) →ₗ[Alg F] (a : D.Mid x) → Rep F (F (D.mid x a))

The left map R_{τ x} → ⊕_a R_{mid a} of the mesh resolution.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.tauMap_injective {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) : Function.Injective ⇑(D.tauMap x hx)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.range_tauMap {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) : (D.tauMap x hx).range = (D.meshMap x).ker

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.meshMap_injective {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : D.proj x) : Function.Injective ⇑(D.meshMap x)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.meshMap_single {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (a : D.Mid x) : D.meshMap x ∘ₗ LinearMap.single (Alg F) (fun (a : D.Mid x) => Rep F (F (D.mid x a))) a = repMap (D.p x a)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.contra_factor {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) (w : ι) (ψ : ((a : D.Mid x) → Rep F (F (D.mid x a))) →ₗ[Alg F] Rep F (F w)) (hψ : ψ ∘ₗ D.tauMap x hx = 0) : ∃ (φ : Rep F (F x) →ₗ[Alg F] Rep F (F w)), φ ∘ₗ D.meshMap x = ψ

Second sequence of Proposition 2.6(1), on modules: maps ⊕_a R_{mid a} → R_w killed by the translation map factor uniquely through the mesh map.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.contra_unique {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) (w : ι) (φ : Rep F (F x) →ₗ[Alg F] Rep F (F w)) (hφ : φ ∘ₗ D.meshMap x = 0) : φ = 0

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.meshMap_mem_rad {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (s : (a : D.Mid x) → Rep F (F (D.mid x a))) : (D.meshMap x) s ∈ L.radRep x

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.hom_top_eq_zero {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) (w : ι) (θ : L.Top x →ₗ[Alg F] Rep F (F w)) : θ = 0

Hom(L_x, R_w) = 0 at a nonprojective x.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extend_top {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (x : ι) (hx : ¬D.proj x) (w : ι) {M : Type u_1} [AddCommGroup M] [Module (Alg F) M] (U : Submodule (Alg F) M) (e : (M ⧸ U) ≃ₗ[Alg F] L.Top x) (g : ↥U →ₗ[Alg F] Rep F (F w)) : ∃ (f : M →ₗ[Alg F] Rep F (F w)), f ∘ₗ U.subtype = g

Ext¹(L_x, R_w) = 0 at a nonprojective x, in extension form: a map into R_w from a submodule with quotient L_x extends.