Spherical varieties

This file defines a spherical variety over B over a ring R as a scheme X over Spec R equipped with an action B × X → X with an open orbit.

TODO

This is very experimental. Many conditions are missing.

class AlgebraicGeometry.SphericalVariety (R : CommRingCat) (B X : Scheme) [B.Over (Spec R)] [X.Over (Spec R)] [CategoryTheory.MonObj (B.asOver (Spec R))] extends CategoryTheory.ModObj (B.asOver (AlgebraicGeometry.Spec R)) (X.asOver (AlgebraicGeometry.Spec R)) : Type u_1

A spherical variety over B over a ring R is a scheme X equipped with an action B × X → X with an open dense orbit.

• smul : MonoidalCategory.MonoidalLeftActionStruct.actionObj (B.asOver (AlgebraicGeometry.Spec R)) (X.asOver (AlgebraicGeometry.Spec R)) ⟶ X.asOver (AlgebraicGeometry.Spec R)
• one_smul' : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.one (X.asOver (AlgebraicGeometry.Spec R))) smul = (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (X.asOver (AlgebraicGeometry.Spec R))).hom
• mul_smul' : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul (X.asOver (AlgebraicGeometry.Spec R))) smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso (B.asOver (AlgebraicGeometry.Spec R)) (B.asOver (AlgebraicGeometry.Spec R)) (X.asOver (AlgebraicGeometry.Spec R))).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight (B.asOver (AlgebraicGeometry.Spec R)) smul) smul)