Documentation

Mathlib.CategoryTheory.Comma.Over.OverClass

Typeclasses for S-objects and S-morphisms #

Warning: This is not usually how typeclasses should be used. This is only a sensible approach when the morphism is considered as a structure on X, typically in algebraic geometry.

This is analogous to to how we view ringhoms as structures via the Algebra typeclass.

For other applications use unbundled arrows or CategoryTheory.Over.

Main definition #

class CategoryTheory.OverClass {C : Type u} [Category.{v, u} C] (X S : C) :

OverClass X S is the typeclass containing the data of a structure morphism X ↘ S : X ⟶ S.

  • ofHom :: (
    • hom : X S

      The structure morphism. Use X ↘ S instead.

  • )
Instances
    def CategoryTheory.over {C : Type u} [Category.{v, u} C] (X S : C) :

    The structure morphism X ↘ S : X ⟶ S given OverClass X S. The instance argument is an optParam instead so that it appears in the discrimination tree.

    Equations

    The structure morphism X ↘ S : X ⟶ S given OverClass X S.

    Equations

    See Note [custom simps projection]

    Equations

    X.CanonicallyOverClass S is the typeclass containing the data of a structure morphism X ↘ S : X ⟶ S, and that S is (uniquely) inferable from the structure of X.

    Instances
      @[simp]
      class CategoryTheory.HomIsOver {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) (S : C) [OverClass X S] [OverClass Y S] :

      Given OverClass X S and OverClass Y S and f : X ⟶ Y, HomIsOver f S is the typeclass asserting f commutes with the structure morphisms.

      Instances
        @[simp]
        theorem CategoryTheory.comp_over {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) (S : C) [OverClass X S] [OverClass Y S] [HomIsOver f S] :
        @[simp]
        theorem CategoryTheory.comp_over_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) (S : C) [OverClass X S] [OverClass Y S] [HomIsOver f S] {Z : C} (h : S Z) :
        instance CategoryTheory.instHomIsOverComp {C : Type u} [Category.{v, u} C] {X Y Z : C} (S : C) [OverClass X S] [OverClass Y S] [OverClass Z S] (f : X Y) (g : Y Z) [HomIsOver f S] [HomIsOver g S] :
        @[reducible, inline]
        abbrev CategoryTheory.IsOverTower {C : Type u} [Category.{v, u} C] (X Y S : C) [OverClass X S] [OverClass Y S] [OverClass X Y] :

        Scheme.IsOverTower X Y S is the typeclass asserting that the structure morphisms X ↘ Y, Y ↘ S, and X ↘ S commute.

        Equations
        instance CategoryTheory.instIsOverTower {C : Type u} [Category.{v, u} C] {X : C} (S : C) [OverClass X S] :
        instance CategoryTheory.instIsOverTower_1 {C : Type u} [Category.{v, u} C] {X : C} (S : C) [OverClass X S] :
        theorem CategoryTheory.homIsOver_of_isOverTower {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) (S S' : C) [OverClass X S] [OverClass X S'] [OverClass Y S] [OverClass Y S'] [OverClass S S'] [IsOverTower X S S'] [IsOverTower Y S S'] [HomIsOver f S] :
        instance CategoryTheory.instHomIsOverOfIsOverTower {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) (S S' : C) [CanonicallyOverClass X S] [OverClass X S'] [OverClass Y S] [OverClass Y S'] [OverClass S S'] [IsOverTower X S S'] [IsOverTower Y S S'] [HomIsOver f S] :
        instance CategoryTheory.instHomIsOverOfIsOverTower_1 {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) (S S' : C) [OverClass X S] [OverClass X S'] [CanonicallyOverClass Y S] [OverClass Y S'] [OverClass S S'] [IsOverTower X S S'] [IsOverTower Y S S'] [HomIsOver f S] :

        Bundle X with an OverClass X S instance into Over S.

        Equations
        @[simp]
        theorem CategoryTheory.OverClass.asOver_hom {C : Type u} [Category.{v, u} C] (X S : C) [OverClass X S] :
        (asOver X S).hom = X S
        @[simp]
        theorem CategoryTheory.OverClass.asOver_left {C : Type u} [Category.{v, u} C] (X S : C) [OverClass X S] :
        (asOver X S).left = X
        def CategoryTheory.OverClass.asOverHom {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (f : X Y) [HomIsOver f S] :
        asOver X S asOver Y S

        Bundle a morphism f : X ⟶ Y with HomIsOver f S into a morphism in Over S.

        Equations
        @[simp]
        theorem CategoryTheory.OverClass.asOverHom_left {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (f : X Y) [HomIsOver f S] :
        (asOverHom S f).left = f
        @[simp]
        theorem CategoryTheory.OverClass.fromOver_over {C : Type u} [Category.{v, u} C] {S : C} (X : Over S) :
        X.left S = X.hom
        instance CategoryTheory.instHomIsOverLeftDiscretePUnit {C : Type u} [Category.{v, u} C] {S : C} {X Y : Over S} (f : X Y) :