The category of root pairings

This file defines the category of root pairings, following the definition of category of root data given in SGA III Exp. 21 Section 6.

Main definitions:

• RootPairingCat: Objects are root pairings.

TODO

• Forgetful functors
• Functions passing between module maps and root pairing homs

Implementation details

This is mostly copied from ModuleCat.

structure RootPairingCat (R : Type u) [CommRing R] : Type (max u (v + 1))

Objects in the category of root pairings.

• weight : Type v

  The weight space of a root pairing.

• weightIsAddCommGroup : AddCommGroup self.weight
• weightIsModule : Module R self.weight
• coweight : Type v

  The coweight space of a root pairing.

• coweightIsAddCommGroup : AddCommGroup self.coweight
• coweightIsModule : Module R self.coweight
• index : Type v

  The set that indexes roots and coroots.

• pairing : RootPairing self.index R self.weight self.coweight

  The root pairing structure.

instance RootPairingCat.category {R : Type u} [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (RootPairingCat R)

Equations

• RootPairingCat.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯