Total spaces of super vector spaces

Forgetting the grading gives the product of the even and odd components. Morphisms act componentwise, giving an algebra map on endomorphisms.

@[reducible, inline]

abbrev RS.Tot (V : SuperVect) : Type

The total space of a super vector space.

Equations

• RS.Tot V = (V.even × V.odd)

def RS.tot {V W : SuperVect} (f : V ⟶ W) : Tot V →ₗ[ℂ] Tot W

The total linear map of a morphism of super vector spaces.

Equations

• RS.tot f = f.evenMap.prodMap f.oddMap

@[simp]

theorem RS.tot_id (V : SuperVect) : tot (CategoryTheory.CategoryStruct.id V) = LinearMap.id

The total map of the identity.

theorem RS.tot_comp {V W X : SuperVect} (f : V ⟶ W) (g : W ⟶ X) : tot (CategoryTheory.CategoryStruct.comp f g) = tot g ∘ₗ tot f

The total map of a composite.

theorem RS.tot_add {V W : SuperVect} (f g : V ⟶ W) : tot (f + g) = tot f + tot g

The total map is additive in the morphism.

theorem RS.tot_smul {V W : SuperVect} (c : ℂ) (f : V ⟶ W) : tot (c • f) = c • tot f

The total map is homogeneous in the morphism.

@[simp]

theorem RS.tot_zero (V W : SuperVect) : tot 0 = 0

The total map of a zero morphism.

def RS.totAlgHom (V : SuperVect) : CategoryTheory.End V →ₐ[ℂ] Module.End ℂ (Tot V)

Forgetting the grading preserves the endomorphism algebra.

Equations

• RS.totAlgHom V = { toFun := RS.tot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def RS.totIso {V W : SuperVect} (e : V ≅ W) : Tot V ≃ₗ[ℂ] Tot W

A super isomorphism induces a linear equivalence of total spaces.

Equations

• RS.totIso e = { toLinearMap := RS.tot e.hom, invFun := ⇑(RS.tot e.inv), left_inv := ⋯, right_inv := ⋯ }