class CommGrp_Class {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) extends Grp_Class X, IsCommMon X : Type u_2

• one : 𝟙_ C ⟶ X
• mul : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X
• one_mul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one X) mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
• mul_one' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X one) mul = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
• mul_assoc' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul) mul)
• inv : X ⟶ X
• left_inv' : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift inv (CategoryTheory.CategoryStruct.id X)) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit X) Mon_Class.one
• right_inv' : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.id X) inv) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit X) Mon_Class.one
• mul_comm' : CategoryTheory.CategoryStruct.comp (β_ X X).hom Mon_Class.mul = Mon_Class.mul

instance instCommGrp_ClassX {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.ChosenFiniteProducts C] (X : CommGrp_ C) : CommGrp_Class X.X

Equations

• instCommGrp_ClassX X = CommGrp_Class.mk

noncomputable instance instGrp_ClassSchemeTorusInt (σ : Type u_1) : Grp_Class (AlgebraicGeometry.TorusInt σ)

Equations

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

instance instIsCommMonSchemeTorusInt (σ : Type u_1) : IsCommMon (AlgebraicGeometry.TorusInt σ)

def CategoryTheory.Over.equivalenceOfIsTerminal {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : Over X ≌ C

If X : C is initial, then the under category of X is equivalent to C.

Equations

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

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_unitIso {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).unitIso = NatIso.ofComponents (fun (Y : Over X) => isoMk (Iso.refl ((Functor.id (Over X)).obj Y).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_functor {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).functor = forget X

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_counitIso {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).counitIso = NatIso.ofComponents (fun (x : C) => Iso.refl (({ obj := fun (Y : C) => mk (hX.from Y), map := fun {X_1 Y : C} (f : X_1 ⟶ Y) => homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (forget X)).obj x)) ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (equivalenceOfIsTerminal hX).inverse.map f = homMk f ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) (Y : C) : (equivalenceOfIsTerminal hX).inverse.obj Y = mk (hX.from Y)

instance instIsRightAdjointOverStar_toric {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C] {X : C} : (CategoryTheory.Over.star X).IsRightAdjoint

noncomputable def Over.forgetMapTerminal {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasTerminal C] (S : C) : CategoryTheory.Over.forget S ≅ (CategoryTheory.Over.map (CategoryTheory.Limits.terminal.from S)).comp (CategoryTheory.Over.equivalenceOfIsTerminal CategoryTheory.Limits.terminalIsTerminal).functor

Equations

• Over.forgetMapTerminal S = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Over S) => CategoryTheory.Iso.refl ((CategoryTheory.Over.forget S).obj X)) ⋯

def CommGrp_Torus (S : AlgebraicGeometry.Scheme) (σ : Type u_1) : CommGrp_ (CategoryTheory.Over S)

Equations

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

def SplitTorus (S : AlgebraicGeometry.Scheme) (σ : Type u_1) : AlgebraicGeometry.Scheme

The (split) algebraic torus over S indexed by σ.

Equations

• SplitTorus S σ = (CommGrp_Torus S σ).X.left

def «term𝔾ₘ[_]» : Lean.ParserDescr

Equations

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

instance SplitTorus.instCanonicallyOver (S : AlgebraicGeometry.Scheme) (σ : Type u_1) : AlgebraicGeometry.Scheme.CanonicallyOver S

Equations

• SplitTorus.instCanonicallyOver S σ = CategoryTheory.CanonicallyOverClass.mk

instance instCommGrp_ClassOverSchemeMkOverSplitTorusInferInstanceOverClass (S : AlgebraicGeometry.Scheme) (σ : Type u_1) : CommGrp_Class (CategoryTheory.Over.mk (SplitTorus S σ ↘ S))

Equations

• instCommGrp_ClassOverSchemeMkOverSplitTorusInferInstanceOverClass S σ = inferInstanceAs (CommGrp_Class (CommGrp_Torus S σ).X)

def SplitTorus.representableBy (S : AlgebraicGeometry.Scheme) (σ : Type u_1) : ((CategoryTheory.Over.forget S).op.comp (AlgebraicGeometry.Scheme.Γ.comp ((CategoryTheory.forget₂ CommRingCat CommMonCat).comp (CommMonCat.units.comp ((CommGrp.coyonedaRight.obj (Opposite.op σ)).comp (CategoryTheory.forget CommGrp)))))).RepresentableBy (CategoryTheory.Over.mk (SplitTorus S σ ↘ S))

Equations

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