structure GroupoidMultitensor.FiniteGroupoidData : Type (max (u + 1) (v + 1))

A finite groupoid presented combinatorially as objects Obj, morphisms Mor, source/target maps, composition (defined when tgt g = src h), identity, and inverse, all subject to the expected groupoid relations.

• Obj : Type u
• Mor : Type v
• finObj : Fintype self.Obj
• finMor : Fintype self.Mor
• decEqObj : DecidableEq self.Obj
• decEqMor : DecidableEq self.Mor
• src : self.Mor → self.Obj
• tgt : self.Mor → self.Obj
• comp (g h : self.Mor) : self.tgt g = self.src h → self.Mor
• id : self.Obj → self.Mor
• inv : self.Mor → self.Mor
• src_id (x : self.Obj) : self.src (self.id x) = x
• tgt_id (x : self.Obj) : self.tgt (self.id x) = x
• src_comp (g h : self.Mor) (p : self.tgt g = self.src h) : self.src (self.comp g h p) = self.src g
• tgt_comp (g h : self.Mor) (p : self.tgt g = self.src h) : self.tgt (self.comp g h p) = self.tgt h
• src_inv (g : self.Mor) : self.src (self.inv g) = self.tgt g
• tgt_inv (g : self.Mor) : self.tgt (self.inv g) = self.src g

def GroupoidMultitensor.FiniteGroupoidData.IsSingleObject (G : FiniteGroupoidData) : Prop

The groupoid G has a single object (its object set has cardinality 1).

noncomputable def GroupoidMultitensor.FiniteGroupoidData.numObjects (G : FiniteGroupoidData) : ℕ

The number of objects of the finite groupoid G.

def GroupoidMultitensor.FiniteGroupoidData.MorBetween (G : FiniteGroupoidData) (x y : G.Obj) : Type v

The subtype of morphisms of G between two specified objects.

theorem GroupoidMultitensor.FiniteGroupoidData.id_injective (G : FiniteGroupoidData) : Function.Injective G.id

The identity-morphism map Obj → Mor of a groupoid is injective.

def GroupoidMultitensor.FiniteGroupoidData.unitComponents (G : FiniteGroupoidData) : Finset G.Mor

The image of the identity map: the set of identity morphisms, one per object.

def GroupoidMultitensor.FiniteGroupoidData.HasSimpleUnit (G : FiniteGroupoidData) : Prop

The groupoid has a single connected component contributing to the unit, i.e. only one identity morphism.

theorem GroupoidMultitensor.FiniteGroupoidData.unitComponents_card (G : FiniteGroupoidData) : G.unitComponents.card = Fintype.card G.Obj

The cardinality of unitComponents equals the number of objects of G.

@[reducible, inline]

abbrev GroupoidMultitensor.FiniteGroupoidData.EndUnit (G : FiniteGroupoidData) (k : Type w) [Field k] : Type (max w u_1)

The algebra of endomorphisms of the unit object for the groupoid-graded k-vector space category: pointwise scalars indexed by objects of G.

theorem GroupoidMultitensor.FiniteGroupoidData.finrank_endUnit (G : FiniteGroupoidData) (k : Type w) [Field k] : Module.finrank k (G.EndUnit k) = Fintype.card G.Obj

The dimension of EndUnit equals the number of objects of G.

theorem GroupoidMultitensor.FiniteGroupoidData.endUnit_iso_k_iff_singleObject (G : FiniteGroupoidData) (k : Type w) [Field k] : Module.finrank k (G.EndUnit k) = 1 ↔ G.IsSingleObject

The endomorphism algebra of the unit has dimension 1 iff the groupoid has a single object — the criterion separating tensor from multitensor categories.

noncomputable def GroupoidMultitensor.FiniteGroupoidData.endUnitLinearEquivOfSingleObject (G : FiniteGroupoidData) (k : Type w) [Field k] (h : G.IsSingleObject) : G.EndUnit k ≃ₗ[k] k

If G has a single object, EndUnit k is k-linearly equivalent to k.

noncomputable def GroupoidMultitensor.FiniteGroupoidData.endUnitAlgEquivOfSingleObject (G : FiniteGroupoidData) (k : Type w) [Field k] (h : G.IsSingleObject) : G.EndUnit k ≃ₐ[k] k

If G has a single object, EndUnit k is k-algebra-equivalent to k.

theorem GroupoidMultitensor.FiniteGroupoidData.endUnit_dim_gt_one_of_multipleObjects (G : FiniteGroupoidData) (k : Type w) [Field k] (h : 1 < Fintype.card G.Obj) : 1 < Module.finrank k (G.EndUnit k)

If G has more than one object, EndUnit k has dimension greater than one.

def GroupoidMultitensor.groupAsGroupoidData (G : Type u) [Group G] [Fintype G] [DecidableEq G] : FiniteGroupoidData

View a finite group as the single-object groupoid whose morphisms are the group elements.

def GroupoidMultitensor.pairGroupoidData (X : Type u) [Fintype X] [DecidableEq X] : FiniteGroupoidData

The pair groupoid on a finite set X: objects are points of X, with a unique morphism between any two of them.

def GroupoidMultitensor.transformationGroupoidData (G X : Type u) [Group G] [Fintype G] [DecidableEq G] [Fintype X] [DecidableEq X] [MulAction G X] : FiniteGroupoidData

The transformation groupoid X ⋊ G associated with a finite group acting on a finite set: objects are points of X, morphisms are pairs (g, x) from x to g • x.

structure GroupoidMultitensor.GroupoidGradedVecData (k : Type w) [Field k] (G : FiniteGroupoidData) : Type (max v (w + 1))

A groupoid-graded vector space: assignment of a k-vector space to each morphism of G. The categories of such gradings model multitensor categories arising from groupoids.

• component : G.Mor → Type w
• instAddCommMonoid (g : G.Mor) : AddCommMonoid (self.component g)
• instModule (g : G.Mor) : Module k (self.component g)

def GroupoidMultitensor.GroupoidGradedVecData.isUnitComponent (G : FiniteGroupoidData) (g : G.Mor) : Prop

A morphism g is a unit-component iff it equals some identity morphism G.id x.

def GroupoidMultitensor.GroupoidGradedVecData.dualGrading (G : FiniteGroupoidData) (g : G.Mor) : G.Mor

Grading shift for the dual object: invert the morphism.

@[reducible]

def GroupoidMultitensor.ggvCategoryInstance (k : Type w) [Field k] (G : FiniteGroupoidData) : CategoryTheory.Category.{max v w, max (w + 1) v} (GroupoidGradedVecData k G)

Category structure on GroupoidGradedVecData k G: a morphism is a family of k-linear maps between the components indexed by morphisms of G.

@[implicit_reducible]

noncomputable instance GroupoidMultitensor.ggvMonoidalInstance (k : Type w) [Field k] (G : FiniteGroupoidData) : CategoryTheory.MonoidalCategory (GroupoidGradedVecData k G)

Monoidal structure on GroupoidGradedVecData k G whose tensor product convolves gradings along composition in the groupoid.

structure GroupoidMultitensor.MatrixVecData (k : Type w) [Field k] (n : ℕ) : Type (w + 1)

Matrix-valued vector space data: a k-vector space component i j assigned to each (i, j) index pair in Fin n × Fin n.

• component : Fin n → Fin n → Type w
• instAddCommMonoid (i j : Fin n) : AddCommMonoid (self.component i j)
• instModule (i j : Fin n) : Module k (self.component i j)

@[reducible]

def GroupoidMultitensor.matVecCategoryInstance (k : Type w) [Field k] (n : ℕ) : CategoryTheory.Category.{w, w + 1} (MatrixVecData k n)

Category structure on MatrixVecData k n: morphisms are entrywise linear maps.

@[implicit_reducible]

noncomputable instance GroupoidMultitensor.matVecMonoidalInstance (k : Type w) [Field k] (n : ℕ) : CategoryTheory.MonoidalCategory (MatrixVecData k n)

Monoidal structure on MatrixVecData k n using matrix multiplication of components.

structure GroupoidMultitensor.ProductMatrixGroupVecData (k : Type w) [Field k] {m : ℕ} (n : Fin m → ℕ) (G : Fin m → Type w) [(i : Fin m) → Group (G i)] [(i : Fin m) → Fintype (G i)] [(i : Fin m) → DecidableEq (G i)] : Type (w + 1)

The product of m matrix-group-graded vector space datas: for each i we have a matrix indexed by Fin (n i) × Fin (n i) further graded by elements of G i.

• component (i : Fin m) : Fin (n i) → Fin (n i) → G i → Type w
• instAddCommMonoid (i : Fin m) (j₁ j₂ : Fin (n i)) (g : G i) : AddCommMonoid (self.component i j₁ j₂ g)
• instModule (i : Fin m) (j₁ j₂ : Fin (n i)) (g : G i) : Module k (self.component i j₁ j₂ g)

@[reducible]

def GroupoidMultitensor.pmgvCategoryInstance (k : Type w) [Field k] {m : ℕ} (n : Fin m → ℕ) (G : Fin m → Type w) [(i : Fin m) → Group (G i)] [(i : Fin m) → Fintype (G i)] [(i : Fin m) → DecidableEq (G i)] : CategoryTheory.Category.{w, w + 1} (ProductMatrixGroupVecData k n G)

Category structure on ProductMatrixGroupVecData with componentwise linear maps.

@[implicit_reducible]

noncomputable instance GroupoidMultitensor.pmgvMonoidalInstance (k : Type w) [Field k] {m : ℕ} (n : Fin m → ℕ) (G : Fin m → Type w) [(i : Fin m) → Group (G i)] [(i : Fin m) → Fintype (G i)] [(i : Fin m) → DecidableEq (G i)] : CategoryTheory.MonoidalCategory (ProductMatrixGroupVecData k n G)

Monoidal structure on ProductMatrixGroupVecData combining matrix multiplication and the group multiplications of the components.

def GroupoidMultitensor.AreMonoidallyEquivalent (C : Type u_1) (catC : CategoryTheory.Category.{u_3, u_1} C) (monC : CategoryTheory.MonoidalCategory C) (D : Type u_2) (catD : CategoryTheory.Category.{u_4, u_2} D) (monD : CategoryTheory.MonoidalCategory D) : Prop

Two monoidal categories C and D are monoidally equivalent if there is an equivalence between them whose forward functor carries a lax monoidal structure.

theorem GroupoidMultitensor.pairGroupoid_equiv_matrixVec (k : Type w) [Field k] (X : Type u) [Fintype X] [DecidableEq X] : AreMonoidallyEquivalent (GroupoidGradedVecData k (pairGroupoidData X)) (ggvCategoryInstance k (pairGroupoidData X)) (ggvMonoidalInstance k (pairGroupoidData X)) (MatrixVecData k (Fintype.card X)) (matVecCategoryInstance k (Fintype.card X)) (matVecMonoidalInstance k (Fintype.card X))

The monoidal category of pair-groupoid-graded vector spaces on X is monoidally equivalent to the matrix vector-space category of size |X|.

theorem GroupoidMultitensor.groupoid_decomposition (k : Type w) [Field k] (G : FiniteGroupoidData) : ∃ (m : ℕ) (n : Fin m → ℕ) (autGroup : Fin m → Type w) (x : (i : Fin m) → Group (autGroup i)) (x_1 : (i : Fin m) → Fintype (autGroup i)) (x_2 : (i : Fin m) → DecidableEq (autGroup i)), AreMonoidallyEquivalent (GroupoidGradedVecData k G) (ggvCategoryInstance k G) (ggvMonoidalInstance k G) (ProductMatrixGroupVecData k n autGroup) (pmgvCategoryInstance k n autGroup) (pmgvMonoidalInstance k n autGroup)

Decomposition theorem: every groupoid-graded vector space category is monoidally equivalent to a finite product of matrix-group-graded vector space categories, one per connected component.

def GroupoidMultitensor.componentSubcategoryGrading (G : FiniteGroupoidData) (x y : G.Obj) : Type u_2

The grading set indexing the (x, y) component subcategory: morphisms in G from y to x.

noncomputable def GroupoidMultitensor.fromMathlibGroupoid (X : Type u) [Fintype X] [DecidableEq X] [CategoryTheory.Groupoid X] [(x y : X) → Fintype (x ⟶ y)] [(x y : X) → DecidableEq (x ⟶ y)] : FiniteGroupoidData

Bridge from a Mathlib Groupoid instance with finite Hom sets to FiniteGroupoidData.