A small model of SuperVect

RS.SuperVect is a large category: its objects are pairs of finite-dimensional complex vector spaces drawn from Type, so the type of objects lives in Type 1, while every hom-space is a pair of linear maps in Type 0. The whole Ind-layer — RS.indOf, the Ind C instances, and the realization functor RS.superRealize — runs over a small preadditive category with finite colimits and a biproduct-generating pair. This file supplies the missing bridge.

• Classification: every super vector space is isomorphic to the standard object stdObj (p, q) — Fin p → ℂ in even degree, Fin q → ℂ in odd degree — of its dimension pair (isoStdObj).

• Colimit structure: SuperVect has a zero object, all finite biproducts (componentwise products, piBicone), and cokernels (componentwise quotients, cokerIsColimit), hence coequalizers and all finite colimits.

• The small model SmallSuperVect: the category induced on the dimension pairs ℕ × ℕ by stdObj. It is a small category with Preadditive, Linear ℂ, and HasFiniteColimits instances, and the inclusion smallSuperInclusion is an equivalence (smallSuperEquiv); in particular SuperVect is essentially small relative to Type 0.

• Generators: the images sEven = (1, 0) and sOdd = (0, 1) of the unit and the odd line biproduct-generate the small model (biproductGenerates_smallSuper): a (p, q)-dimensional object is the biproduct of p copies of the unit and q copies of the odd line. This discharges the hypothesis of RS.isZero_of_isZero_superRealize at C := SmallSuperVect.

The small model is built as an InducedCategory on ℕ × ℕ rather than through Mathlib's SmallModel: the induced category's hom-spaces are the hom-spaces of SuperVect between standard objects, wrapped in the one-field structure InducedCategory.Hom, so smallness, Preadditive, Linear ℂ, and full faithfulness of the inclusion are existing Mathlib instances, whereas SmallModel (a skeleton quotient) would need every instance conjugated across equivSmallModel. Mathlib's EssentiallySmall/SmallModel/equivSmallModel API, the biproduct machinery (Bicone, isBilimitOfTotal, biproduct.uniqueUpToIso, biproduct.reindex), and the colimit constructions (Preadditive.hasCoequalizers_of_hasCokernels, hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts) are all reachable through the funnel; isBilimitOfTotal lives in the root CategoryTheory.Limits namespace, not on Bicone.

Standard objects and the classification by dimension

def RS.SuperVect.stdObj (pq : ℕ × ℕ) : SuperVect

The standard super vector space of a dimension pair: Fin p → ℂ in even degree and Fin q → ℂ in odd degree. Every super vector space is isomorphic to exactly one standard object, which is the entire content of the small model below.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.SuperVect.stdObj_even (pq : ℕ × ℕ) : (stdObj pq).even = (Fin pq.1 → ℂ)

The even component of a standard object.

@[simp]

theorem RS.SuperVect.stdObj_odd (pq : ℕ × ℕ) : (stdObj pq).odd = (Fin pq.2 → ℂ)

The odd component of a standard object.

def RS.SuperVect.isoOfEquivs {V W : SuperVect} (e : V.even ≃ₗ[ℂ] W.even) (o : V.odd ≃ₗ[ℂ] W.odd) : V ≅ W

Componentwise linear equivalences assemble to an isomorphism of super vector spaces.

Equations

• RS.SuperVect.isoOfEquivs e o = { hom := { evenMap := ↑e, oddMap := ↑o }, inv := { evenMap := ↑e.symm, oddMap := ↑o.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.SuperVect.isoStdObj (V : SuperVect) : V ≅ stdObj (Module.finrank ℂ V.even, Module.finrank ℂ V.odd)

Classification of super vector spaces: every object of SuperVect is isomorphic to the standard object of its dimension pair, componentwise by LinearEquiv.ofFinrankEq.

Equations

• One or more equations did not get rendered due to their size.

Subsingleton hom-spaces

instance RS.SuperVect.instSubsingletonEvenStdObjMkNatOfNat (q : ℕ) : Subsingleton (stdObj (0, q)).even

The even component of a purely odd standard object is trivial.

instance RS.SuperVect.instSubsingletonOddStdObjMkNatOfNat (p : ℕ) : Subsingleton (stdObj (p, 0)).odd

The odd component of a purely even standard object is trivial.

theorem RS.SuperVect.hom_eq_of_subsingleton {V W : SuperVect} (he : Subsingleton (V.even →ₗ[ℂ] W.even)) (ho : Subsingleton (V.odd →ₗ[ℂ] W.odd)) (f g : V ⟶ W) : f = g

Hom-spaces whose component spaces of linear maps are subsingletons are themselves subsingletons: this recognises the zero object and kills the mixed-parity morphisms between the two generator lines.

instance RS.SuperVect.homSubsingleton {V W : SuperVect} [Subsingleton (V.even →ₗ[ℂ] W.even)] [Subsingleton (V.odd →ₗ[ℂ] W.odd)] : Subsingleton (V ⟶ W)

A subsingleton instance form of hom_eq_of_subsingleton.

The zero object

theorem RS.SuperVect.isZero_stdObj_zero : CategoryTheory.Limits.IsZero (stdObj (0, 0))

The standard object of dimensions (0, 0) is a zero object.

instance RS.SuperVect.instHasZeroObject : CategoryTheory.Limits.HasZeroObject SuperVect

SuperVect has a zero object.

Finite biproducts

theorem RS.SuperVect.sum_single_comp_proj {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → Type) [(i : ι) → AddCommGroup (φ i)] [(i : ι) → Module ℂ (φ i)] : ∑ j : ι, LinearMap.single ℂ φ j ∘ₗ LinearMap.proj j = LinearMap.id

The sum of the coordinate inclusion-projection round trips on a finite product of modules is the identity.

def RS.SuperVect.piObj {n : ℕ} (f : Fin n → SuperVect) : SuperVect

The componentwise product of a finite family of super vector spaces: the biproduct candidate.

Equations

• One or more equations did not get rendered due to their size.

def RS.SuperVect.piBicone {n : ℕ} (f : Fin n → SuperVect) : CategoryTheory.Limits.Bicone f

The componentwise bicone over a finite family: coordinate projections and inclusions in each degree.

Equations

• One or more equations did not get rendered due to their size.

def RS.SuperVect.evenMapAddHom (V W : SuperVect) : (V ⟶ W) →+ V.even →ₗ[ℂ] W.even

Taking the even component of a morphism is additive.

Equations

• V.evenMapAddHom W = { toFun := fun (f : V ⟶ W) => f.evenMap, map_zero' := ⋯, map_add' := ⋯ }

def RS.SuperVect.oddMapAddHom (V W : SuperVect) : (V ⟶ W) →+ V.odd →ₗ[ℂ] W.odd

Taking the odd component of a morphism is additive.

Equations

• V.oddMapAddHom W = { toFun := fun (f : V ⟶ W) => f.oddMap, map_zero' := ⋯, map_add' := ⋯ }

theorem RS.SuperVect.sum_evenMap {α : Type u_1} (s : Finset α) {V W : SuperVect} (f : α → (V ⟶ W)) : (∑ i ∈ s, f i).evenMap = ∑ i ∈ s, (f i).evenMap

The even component of a finite sum of morphisms is the sum of the even components.

theorem RS.SuperVect.sum_oddMap {α : Type u_1} (s : Finset α) {V W : SuperVect} (f : α → (V ⟶ W)) : (∑ i ∈ s, f i).oddMap = ∑ i ∈ s, (f i).oddMap

The odd component of a finite sum of morphisms is the sum of the odd components.

def RS.SuperVect.piBiconeIsBilimit {n : ℕ} (f : Fin n → SuperVect) : (piBicone f).IsBilimit

The componentwise bicone is a bilimit: the coordinate round trips sum to the identity in each degree.

Equations

• RS.SuperVect.piBiconeIsBilimit f = CategoryTheory.Limits.isBilimitOfTotal (RS.SuperVect.piBicone f) ⋯

instance RS.SuperVect.instHasFiniteBiproducts : CategoryTheory.Limits.HasFiniteBiproducts SuperVect

SuperVect has all finite biproducts, componentwise.

Cokernels and finite colimits

def RS.SuperVect.cokerObj {V W : SuperVect} (f : V ⟶ W) : SuperVect

The componentwise cokernel object of a morphism: the quotient by the range in each degree.

Equations

• One or more equations did not get rendered due to their size.

def RS.SuperVect.cokerπ {V W : SuperVect} (f : V ⟶ W) : W ⟶ cokerObj f

The projection onto the componentwise cokernel.

Equations

• RS.SuperVect.cokerπ f = { evenMap := f.evenMap.range.mkQ, oddMap := f.oddMap.range.mkQ }

theorem RS.SuperVect.comp_cokerπ {V W : SuperVect} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp f (cokerπ f) = 0

The cokernel projection annihilates the morphism.

def RS.SuperVect.cokerDesc {V W Z : SuperVect} (f : V ⟶ W) (g : W ⟶ Z) (hg : CategoryTheory.CategoryStruct.comp f g = 0) : cokerObj f ⟶ Z

Descent through the componentwise cokernel: a morphism annihilating f factors through the quotient in each degree.

Equations

• RS.SuperVect.cokerDesc f g hg = { evenMap := f.evenMap.range.liftQ g.evenMap ⋯, oddMap := f.oddMap.range.liftQ g.oddMap ⋯ }

def RS.SuperVect.cokerIsColimit {V W : SuperVect} (f : V ⟶ W) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (cokerπ f) ⋯)

The componentwise cokernel is a categorical cokernel.

Equations

• One or more equations did not get rendered due to their size.

instance RS.SuperVect.instHasCokernels : CategoryTheory.Limits.HasCokernels SuperVect

SuperVect has all cokernels, componentwise.

instance RS.SuperVect.instHasCoequalizers : CategoryTheory.Limits.HasCoequalizers SuperVect

SuperVect has coequalizers: in a preadditive category they are cokernels of differences.

instance RS.SuperVect.instHasFiniteColimits : CategoryTheory.Limits.HasFiniteColimits SuperVect

SuperVect has all finite colimits: finite coproducts come from the componentwise biproducts and coequalizers from the componentwise cokernels.

The generator lines

def RS.SuperVect.evenLineIn (p q : ℕ) (i : Fin p) : stdObj (1, 0) ⟶ stdObj (p, q)

The inclusion of the even line at coordinate i: the even component places the scalar at coordinate i, the odd component is zero.

Equations

• RS.SuperVect.evenLineIn p q i = { evenMap := LinearMap.single ℂ (fun (x : Fin p) => ℂ) i ∘ₗ LinearMap.proj 0, oddMap := 0 }

def RS.SuperVect.evenLinePrj (p q : ℕ) (i : Fin p) : stdObj (p, q) ⟶ stdObj (1, 0)

The projection onto the even line at coordinate i.

Equations

• RS.SuperVect.evenLinePrj p q i = { evenMap := LinearMap.single ℂ (fun (x : Fin 1) => ℂ) 0 ∘ₗ LinearMap.proj i, oddMap := 0 }

def RS.SuperVect.oddLineIn (p q : ℕ) (j : Fin q) : stdObj (0, 1) ⟶ stdObj (p, q)

The inclusion of the odd line at coordinate j.

Equations

• RS.SuperVect.oddLineIn p q j = { evenMap := 0, oddMap := LinearMap.single ℂ (fun (x : Fin q) => ℂ) j ∘ₗ LinearMap.proj 0 }

def RS.SuperVect.oddLinePrj (p q : ℕ) (j : Fin q) : stdObj (p, q) ⟶ stdObj (0, 1)

The projection onto the odd line at coordinate j.

Equations

• RS.SuperVect.oddLinePrj p q j = { evenMap := 0, oddMap := LinearMap.single ℂ (fun (x : Fin 1) => ℂ) 0 ∘ₗ LinearMap.proj j }

theorem RS.SuperVect.evenLineIn_comp_prj_same (p q : ℕ) (i : Fin p) : CategoryTheory.CategoryStruct.comp (evenLineIn p q i) (evenLinePrj p q i) = CategoryTheory.CategoryStruct.id (stdObj (1, 0))

The even-line round trip through stdObj (p, q) at equal coordinates is the identity.

theorem RS.SuperVect.evenLineIn_comp_prj_ne (p q : ℕ) {i i' : Fin p} (h : i ≠ i') : CategoryTheory.CategoryStruct.comp (evenLineIn p q i) (evenLinePrj p q i') = 0

The even-line round trip at distinct coordinates vanishes.

theorem RS.SuperVect.oddLineIn_comp_prj_same (p q : ℕ) (j : Fin q) : CategoryTheory.CategoryStruct.comp (oddLineIn p q j) (oddLinePrj p q j) = CategoryTheory.CategoryStruct.id (stdObj (0, 1))

The odd-line round trip at equal coordinates is the identity.

theorem RS.SuperVect.oddLineIn_comp_prj_ne (p q : ℕ) {j j' : Fin q} (h : j ≠ j') : CategoryTheory.CategoryStruct.comp (oddLineIn p q j) (oddLinePrj p q j') = 0

The odd-line round trip at distinct coordinates vanishes.

theorem RS.SuperVect.evenLineIn_comp_oddPrj (p q : ℕ) (i : Fin p) (j : Fin q) : CategoryTheory.CategoryStruct.comp (evenLineIn p q i) (oddLinePrj p q j) = 0

Mixed-parity composites vanish: even line into odd line.

theorem RS.SuperVect.oddLineIn_comp_evenPrj (p q : ℕ) (i : Fin p) (j : Fin q) : CategoryTheory.CategoryStruct.comp (oddLineIn p q j) (evenLinePrj p q i) = 0

Mixed-parity composites vanish: odd line into even line.

theorem RS.SuperVect.evenLinePrj_comp_in_evenMap (p q : ℕ) (i : Fin p) : (CategoryTheory.CategoryStruct.comp (evenLinePrj p q i) (evenLineIn p q i)).evenMap = LinearMap.single ℂ (fun (x : Fin p) => ℂ) i ∘ₗ LinearMap.proj i

The even component of the even-line projection-then-inclusion round trip through the point is the coordinate round trip.

theorem RS.SuperVect.evenLinePrj_comp_in_oddMap (p q : ℕ) (i : Fin p) : (CategoryTheory.CategoryStruct.comp (evenLinePrj p q i) (evenLineIn p q i)).oddMap = 0

The odd component of the even-line round trip through the point vanishes.

theorem RS.SuperVect.oddLinePrj_comp_in_oddMap (p q : ℕ) (j : Fin q) : (CategoryTheory.CategoryStruct.comp (oddLinePrj p q j) (oddLineIn p q j)).oddMap = LinearMap.single ℂ (fun (x : Fin q) => ℂ) j ∘ₗ LinearMap.proj j

The odd component of the odd-line projection-then-inclusion round trip through the point is the coordinate round trip.

theorem RS.SuperVect.oddLinePrj_comp_in_evenMap (p q : ℕ) (j : Fin q) : (CategoryTheory.CategoryStruct.comp (oddLinePrj p q j) (oddLineIn p q j)).evenMap = 0

The even component of the odd-line round trip through the point vanishes.

theorem RS.SuperVect.lines_total (p q : ℕ) : ∑ i : Fin p, CategoryTheory.CategoryStruct.comp (evenLinePrj p q i) (evenLineIn p q i) + ∑ j : Fin q, CategoryTheory.CategoryStruct.comp (oddLinePrj p q j) (oddLineIn p q j) = CategoryTheory.CategoryStruct.id (stdObj (p, q))

The line decomposition of a standard object: the sum of all line round trips through stdObj (p, q) is the identity.

The small model

@[reducible, inline]

abbrev RS.SmallSuperVect : Type

The small model of SuperVect: the category induced on the type ℕ × ℕ of dimension pairs by the standard objects. Its hom-spaces are the hom-spaces of SuperVect between standard objects (wrapped in InducedCategory.homMk), so smallness, Preadditive, Linear ℂ, and full faithfulness of the inclusion are all Mathlib instances on InducedCategory — the choice of an induced category over Mathlib's SmallModel (a skeleton quotient, which would need every instance conjugated across equivSmallModel) is what makes them free.

Equations

• RS.SmallSuperVect = CategoryTheory.InducedCategory RS.SuperVect RS.SuperVect.stdObj

@[reducible, inline]

abbrev RS.smallSuperInclusion : CategoryTheory.Functor SmallSuperVect SuperVect

The inclusion of the small model into SuperVect, sending a dimension pair to its standard object. An abbreviation so that the InducedCategory instances (full, faithful, additive) apply to it directly.

Equations

• RS.smallSuperInclusion = CategoryTheory.inducedFunctor RS.SuperVect.stdObj

instance RS.instEssSurjSmallSuperVectSuperVectSmallSuperInclusion : smallSuperInclusion.EssSurj

The inclusion of the small model is essentially surjective: every super vector space is standard up to isomorphism.

instance RS.instIsEquivalenceSmallSuperVectSuperVectSmallSuperInclusion : smallSuperInclusion.IsEquivalence

The inclusion of the small model is an equivalence: fully faithful and essentially surjective.

noncomputable def RS.smallSuperEquiv : SmallSuperVect ≌ SuperVect

The small-model equivalence: the small model is equivalent to SuperVect.

Equations

• RS.smallSuperEquiv = RS.smallSuperInclusion.asEquivalence

instance RS.instEssentiallySmallSuperVect : CategoryTheory.EssentiallySmall.{0, 0, 1} SuperVect

SuperVect is essentially small relative to Type 0: the small model is a witness.

instance RS.instHasFiniteColimitsSmallSuperVect : CategoryTheory.Limits.HasFiniteColimits SmallSuperVect

The small model has all finite colimits, transported across the inclusion equivalence from the componentwise colimits of SuperVect.

The generator pair

def RS.sEven : SmallSuperVect

The even generator of the small model: the unit line (1, 0), whose standard object is the monoidal unit of SuperVect up to isomorphism (sEvenIso).

Equations

• RS.sEven = (1, 0)

def RS.sOdd : SmallSuperVect

The odd generator of the small model: the odd line (0, 1).

Equations

• RS.sOdd = (0, 1)

def RS.zeroLinearEquiv (M N : Type) [AddCommGroup M] [Module ℂ M] [AddCommGroup N] [Module ℂ N] [Subsingleton M] [Subsingleton N] : M ≃ₗ[ℂ] N

Any two subsingleton ℂ-modules are linearly equivalent by the zero map.

Equations

• RS.zeroLinearEquiv M N = { toFun := fun (x : M) => 0, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : N) => 0, left_inv := ⋯, right_inv := ⋯ }

def RS.sEvenIso : smallSuperInclusion.obj sEven ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit SuperVect

The standard object of the even generator is the monoidal unit of SuperVect: Fin 1 → ℂ is the scalar line and the odd component is trivial.

Equations

• One or more equations did not get rendered due to their size.

Biproduct generation

def RS.genWord (p q : ℕ) (s : Fin p ⊕ Fin q) : Bool

The parity word of the generating decomposition of (p, q): the first p letters select the even generator, the last q the odd one.

Equations

• RS.genWord p q s = Sum.elim (fun (x : Fin p) => false) (fun (x : Fin q) => true) s

def RS.genFamily (p q : ℕ) (s : Fin p ⊕ Fin q) : SmallSuperVect

The sum-indexed generator family underlying the generating biproduct decomposition of (p, q).

Equations

• RS.genFamily p q s = RS.generatorPair RS.sEven RS.sOdd (RS.genWord p q s)

theorem RS.smallZero_hom {X Y : SmallSuperVect} : CategoryTheory.InducedCategory.Hom.hom 0 = 0

The underlying morphism of the zero morphism of the small model is zero.

def RS.genBicone (p q : ℕ) : CategoryTheory.Limits.Bicone (genFamily p q)

The generating bicone: (p, q) carries the line inclusions and projections over the sum-indexed generator family.

Equations

• One or more equations did not get rendered due to their size.

def RS.genBiconeIsBilimit (p q : ℕ) : (genBicone p q).IsBilimit

The generating bicone is a bilimit: the line round trips sum to the identity.

Equations

• RS.genBiconeIsBilimit p q = CategoryTheory.Limits.isBilimitOfTotal (RS.genBicone p q) ⋯

theorem RS.biproductGenerates_smallSuper : BiproductGenerates (generatorPair sEven sOdd)

Biproduct generation for the small model: every dimension pair is a finite biproduct of copies of the unit line and the odd line — (p, q) decomposes as p copies of sEven followed by q copies of sOdd. This discharges the generation hypothesis of RS.isZero_of_isZero_superRealize at C := SmallSuperVect.