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

• CategoryTheory.OverClass: OverClass X S equips X with a morphism into S. X ↘ S : X ⟶ S is the structure morphism.
• CategoryTheory.HomIsOver: HomIsOver f S asserts that f commutes with the structure morphisms.

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

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.

• )

def CategoryTheory.over {C : Type u} [Category.{v, u} C] (X S : C) : autoParam (OverClass X S) _auto✝ → (X ⟶ S)

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

• CategoryTheory.over X S x✝ = CategoryTheory.OverClass.hom

def CategoryTheory.«term_↘_» : Lean.TrailingParserDescr

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

Equations

• CategoryTheory.«term_↘_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_↘_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↘ ") (Lean.ParserDescr.cat `term 90))

def CategoryTheory.OverClass.Simps.over {C : Type u} [Category.{v, u} C] (X S : C) [OverClass X S] : X ⟶ S

See Note [custom simps projection]

Equations

• CategoryTheory.OverClass.Simps.over X S = X ↘ S

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

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.

• hom : X ⟶ S

def CategoryTheory.CanonicallyOverClass.Simps.over {C : Type u} [Category.{v, u} C] (X S : C) [CanonicallyOverClass X S] : X ⟶ S

See Note [custom simps projection]

Equations

• CategoryTheory.CanonicallyOverClass.Simps.over X S = X ↘ S

instance CategoryTheory.instOverClass {C : Type u} [Category.{v, u} C] {X : C} : OverClass X X

Equations

• CategoryTheory.instOverClass = { hom := CategoryTheory.CategoryStruct.id X }

@[simp]

theorem CategoryTheory.over_def {C : Type u} [Category.{v, u} C] {X : C} : X ↘ X = CategoryStruct.id X

instance CategoryTheory.instIsIsoOverInferInstanceOverClass {C : Type u} [Category.{v, u} C] (S : C) : IsIso (S ↘ S)

@[instance 900]

instance CategoryTheory.CanonicallyOverClass.instOverClass {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [CanonicallyOverClass X Y] [OverClass Y S] : OverClass X S

Equations

• CategoryTheory.CanonicallyOverClass.instOverClass S = { hom := CategoryTheory.CategoryStruct.comp (X ↘ Y) (Y ↘ S) }

theorem CategoryTheory.CanonicallyOverClass.over_def {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [CanonicallyOverClass X Y] [OverClass Y S] : X ↘ S = CategoryStruct.comp (X ↘ Y) (Y ↘ S)

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

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.

• comp_over : CategoryStruct.comp f (Y ↘ S) = X ↘ S

@[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] : CategoryStruct.comp f (Y ↘ S) = X ↘ 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) : CategoryStruct.comp f (CategoryStruct.comp (Y ↘ S) h) = CategoryStruct.comp (X ↘ S) h

instance CategoryTheory.instHomIsOverId {C : Type u} [Category.{v, u} C] {X : C} (S : C) [OverClass X S] : HomIsOver (CategoryStruct.id X) S

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] : HomIsOver (CategoryStruct.comp f 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] : Prop

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

Equations

• CategoryTheory.IsOverTower X Y S = CategoryTheory.HomIsOver (X ↘ Y) S

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

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

instance CategoryTheory.instIsOverTower_2 {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [CanonicallyOverClass X Y] [OverClass Y S] : IsOverTower X Y 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] : 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] : 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] : HomIsOver f S'

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

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

Equations

• CategoryTheory.OverClass.asOver X S = CategoryTheory.Over.mk (X ↘ S)

@[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

• CategoryTheory.OverClass.asOverHom S f = CategoryTheory.Over.homMk f ⋯

@[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

instance CategoryTheory.OverClass.fromOver {C : Type u} [Category.{v, u} C] {S : C} (X : Over S) : OverClass X.left S

Equations

• CategoryTheory.OverClass.fromOver X = { hom := X.hom }

@[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) : HomIsOver f.left S

instance CategoryTheory.OverClass.instIsIsoOverAsOverHom {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (f : X ⟶ Y) [IsIso f] [HomIsOver f S] : IsIso (asOverHom S f)

instance CategoryTheory.OverClass.instHomIsOverInvOfHom {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] {e : X ≅ Y} [HomIsOver e.hom S] : HomIsOver e.inv S

instance CategoryTheory.OverClass.instHomIsOverHomOfInv {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] {e : X ≅ Y} [HomIsOver e.inv S] : HomIsOver e.hom S

instance CategoryTheory.OverClass.instHomIsOverHomAsIso {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] {f : X ⟶ Y} [IsIso f] [HomIsOver f S] : HomIsOver (asIso f).hom S

instance CategoryTheory.OverClass.instHomIsOverInvAsIso {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] {f : X ⟶ Y} [IsIso f] [HomIsOver f S] : HomIsOver (asIso f).inv S

instance CategoryTheory.OverClass.instHomIsOverInv {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] {f : X ⟶ Y} [IsIso f] [HomIsOver f S] : HomIsOver (inv f) S

@[simp]

theorem CategoryTheory.OverClass.asOverHom_id {C : Type u} [Category.{v, u} C] {X : C} (S : C) [OverClass X S] : asOverHom S (CategoryStruct.id X) = CategoryStruct.id (asOver X S)

@[simp]

theorem CategoryTheory.OverClass.asOverHom_comp {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] : asOverHom S (CategoryStruct.comp f g) = CategoryStruct.comp (asOverHom S f) (asOverHom S g)

theorem CategoryTheory.OverClass.asOverHom_comp_assoc {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] {Z✝ : Over S} (h : asOver Z S ⟶ Z✝) : CategoryStruct.comp (asOverHom S (CategoryStruct.comp f g)) h = CategoryStruct.comp (asOverHom S f) (CategoryStruct.comp (asOverHom S g) h)

@[simp]

theorem CategoryTheory.OverClass.asOverHom_inv {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (f : X ⟶ Y) [IsIso f] [HomIsOver f S] : asOverHom S (inv f) = inv (asOverHom S f)

def CategoryTheory.Iso.asOver {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (e : X ≅ Y) [HomIsOver e.hom S] : OverClass.asOver X S ≅ OverClass.asOver Y S

Reinterpret an isomorphism over an object S into an isomorphism in the category over S.

Equations

• CategoryTheory.Iso.asOver S e = { hom := CategoryTheory.OverClass.asOverHom S e.hom, inv := CategoryTheory.OverClass.asOverHom S e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Iso.asOver_hom {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (e : X ≅ Y) [HomIsOver e.hom S] : (asOver S e).hom = OverClass.asOverHom S e.hom

@[simp]

theorem CategoryTheory.Iso.asOver_inv {C : Type u} [Category.{v, u} C] {X Y : C} (S : C) [OverClass X S] [OverClass Y S] (e : X ≅ Y) [HomIsOver e.hom S] : (asOver S e).inv = OverClass.asOverHom S e.inv