Over and under categories #

Over (and under) categories are special cases of comma categories.

If L is the identity functor and R is a constant functor, then Comma L R is the "slice" or "over" category over the object R maps to.
Conversely, if L is a constant functor and R is the identity functor, then Comma L R is the "coslice" or "under" category under the object L maps to.

Tags #

Comma, Slice, Coslice, Over, Under

source

def CategoryTheory.Over {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

Type (max u₁ v₁)

The over category has as objects arrows in T with codomain X and as morphisms commutative triangles.

See https://stacks.math.columbia.edu/tag/001G.

Equations

CategoryTheory.Over X = CategoryTheory.CostructuredArrow (CategoryTheory.Functor.id T) X

Instances For

source

instance CategoryTheory.instCategoryOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Over X)

Equations

CategoryTheory.instCategoryOver X = CategoryTheory.commaCategory

source

instance CategoryTheory.Over.inhabited {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] [Inhabited T] :

Inhabited (CategoryTheory.Over default)

Equations

CategoryTheory.Over.inhabited = { default := { left := default, right := default, hom := CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id T).obj default) } }

source

theorem CategoryTheory.Over.OverMorphism.ext {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f g : U ⟶ V} (h : f.left = g.left) :

f = g

source

@[simp]

theorem CategoryTheory.Over.over_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Over X) :

U.right = { as := PUnit.unit }

source

@[simp]

theorem CategoryTheory.Over.id_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Over X) :

(CategoryTheory.CategoryStruct.id U).left = CategoryTheory.CategoryStruct.id U.left

source

@[simp]

theorem CategoryTheory.Over.comp_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (a b c : CategoryTheory.Over X) (f : a ⟶ b) (g : b ⟶ c) :

(CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left

source

theorem CategoryTheory.Over.comp_left_assoc {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (a b c : CategoryTheory.Over X) (f : a ⟶ b) (g : b ⟶ c) {Z : T} (h : c.left ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).left h = CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp g.left h)

source

@[simp]

theorem CategoryTheory.Over.w {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {A B : CategoryTheory.Over X} (f : A ⟶ B) :

CategoryTheory.CategoryStruct.comp f.left B.hom = A.hom

source

@[simp]

theorem CategoryTheory.Over.w_assoc {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {A B : CategoryTheory.Over X} (f : A ⟶ B) {Z : T} (h : (CategoryTheory.Functor.fromPUnit X).obj B.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp B.hom h) = CategoryTheory.CategoryStruct.comp A.hom h

source

def CategoryTheory.Over.mk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X) :

CategoryTheory.Over X

To give an object in the over category, it suffices to give a morphism with codomain X.

Equations

CategoryTheory.Over.mk f = CategoryTheory.CostructuredArrow.mk f

Instances For

source

@[simp]

theorem CategoryTheory.Over.mk_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X) :

(CategoryTheory.Over.mk f).left = Y

source

@[simp]

theorem CategoryTheory.Over.mk_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X) :

(CategoryTheory.Over.mk f).hom = f

source

def CategoryTheory.Over.coeFromHom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} :

CoeOut (Y ⟶ X) (CategoryTheory.Over X)

We can set up a coercion from arrows with codomain X to over X. This most likely should not be a global instance, but it is sometimes useful.

Equations

CategoryTheory.Over.coeFromHom = { coe := CategoryTheory.Over.mk }

Instances For

source

@[simp]

theorem CategoryTheory.Over.coe_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X) :

(CategoryTheory.Over.mk f).hom = f

source

def CategoryTheory.Over.homMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by aesop_cat) :

U ⟶ V

To give a morphism in the over category, it suffices to give an arrow fitting in a commutative triangle.

Equations

CategoryTheory.Over.homMk f w = CategoryTheory.CostructuredArrow.homMk f w

Instances For

source

@[simp]

theorem CategoryTheory.Over.homMk_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by aesop_cat) :

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Over.homMk_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by aesop_cat) :

(CategoryTheory.Over.homMk f w).left = f

source

def CategoryTheory.Over.isoMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left) (hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat) :

f ≅ g

Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

Equations

CategoryTheory.Over.isoMk hl hw = CategoryTheory.CostructuredArrow.isoMk hl hw

Instances For

source

@[simp]

theorem CategoryTheory.Over.isoMk_inv_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left) (hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat) :

(CategoryTheory.Over.isoMk hl hw).inv.left = hl.inv

source

@[simp]

theorem CategoryTheory.Over.isoMk_inv_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left) (hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat) :

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Over.isoMk_hom_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left) (hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat) :

(CategoryTheory.Over.isoMk hl hw).hom.left = hl.hom

source

@[simp]

theorem CategoryTheory.Over.isoMk_hom_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left) (hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat) :

⋯ = ⋯

source

def CategoryTheory.Over.forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

CategoryTheory.Functor (CategoryTheory.Over X) T

The forgetful functor mapping an arrow to its domain.

See https://stacks.math.columbia.edu/tag/001G.

Equations

CategoryTheory.Over.forget X = CategoryTheory.Comma.fst (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X)

Instances For

source

@[simp]

theorem CategoryTheory.Over.forget_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Over X} :

(CategoryTheory.Over.forget X).obj U = U.left

source

@[simp]

theorem CategoryTheory.Over.forget_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f : U ⟶ V} :

(CategoryTheory.Over.forget X).map f = f.left

source

def CategoryTheory.Over.forgetCocone {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

CategoryTheory.Limits.Cocone (CategoryTheory.Over.forget X)

The natural cocone over the forgetful functor Over X ⥤ T with cocone point X.

Equations

CategoryTheory.Over.forgetCocone X = { pt := X, ι := { app := CategoryTheory.Comma.hom, naturality := ⋯ } }

Instances For

source

@[simp]

theorem CategoryTheory.Over.forgetCocone_ι_app {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (self : CategoryTheory.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X)) :

(CategoryTheory.Over.forgetCocone X).ι.app self = self.hom

source

@[simp]

theorem CategoryTheory.Over.forgetCocone_pt {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

(CategoryTheory.Over.forgetCocone X).pt = X

source

def CategoryTheory.Over.map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)

A morphism f : X ⟶ Y induces a functor Over X ⥤ Over Y in the obvious way.

See https://stacks.math.columbia.edu/tag/001G.

Equations

CategoryTheory.Over.map f = CategoryTheory.Comma.mapRight (CategoryTheory.Functor.id T) (CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete PUnit.{1}) => f)

Instances For

source

@[simp]

theorem CategoryTheory.Over.map_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X} :

((CategoryTheory.Over.map f).obj U).left = U.left

source

@[simp]

theorem CategoryTheory.Over.map_obj_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X} :

((CategoryTheory.Over.map f).obj U).hom = CategoryTheory.CategoryStruct.comp U.hom f

source

@[simp]

theorem CategoryTheory.Over.map_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U V : CategoryTheory.Over X} {g : U ⟶ V} :

((CategoryTheory.Over.map f).map g).left = g.left

This section proves various equalities between functors that demonstrate, for instance, that over categories assemble into a functor mapFunctor : T ⥤ Cat.

These equalities between functors are then converted to natural isomorphisms using eqToIso. Such natural isomorphisms could be obtained directly using Iso.refl but this method will have better computational properties, when used, for instance, in developing the theory of Beck-Chevalley transformations.

source

theorem CategoryTheory.Over.mapId_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (Y : T) :

CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.Functor.id (CategoryTheory.Over Y)

Mapping by the identity morphism is just the identity functor.

source

def CategoryTheory.Over.mapId {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (Y : T) :

CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id Y) ≅ CategoryTheory.Functor.id (CategoryTheory.Over Y)

The natural isomorphism arising from mapForget_eq.

Equations

CategoryTheory.Over.mapId Y = CategoryTheory.eqToIso ⋯

Instances For

source

theorem CategoryTheory.Over.mapForget_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

(CategoryTheory.Over.map f).comp (CategoryTheory.Over.forget Y) = CategoryTheory.Over.forget X

Mapping by f and then forgetting is the same as forgetting.

source

def CategoryTheory.Over.mapForget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

(CategoryTheory.Over.map f).comp (CategoryTheory.Over.forget Y) ≅ CategoryTheory.Over.forget X

The natural isomorphism arising from mapForget_eq.

Equations

CategoryTheory.Over.mapForget f = CategoryTheory.eqToIso ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Over.eqToHom_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} (e : U = V) :

(CategoryTheory.eqToHom e).left = CategoryTheory.eqToHom ⋯

source

theorem CategoryTheory.Over.mapComp_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Over.map f).comp (CategoryTheory.Over.map g)

Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

source

def CategoryTheory.Over.mapComp {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g) ≅ (CategoryTheory.Over.map f).comp (CategoryTheory.Over.map g)

The natural isomorphism arising from mapComp_eq.

Equations

CategoryTheory.Over.mapComp f g = CategoryTheory.eqToIso ⋯

Instances For

source

def CategoryTheory.Over.mapFunctor (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] :

CategoryTheory.Functor T CategoryTheory.Cat

The functor defined by the over categories.

Equations

CategoryTheory.Over.mapFunctor T = { obj := fun (X : T) => CategoryTheory.Cat.of (CategoryTheory.Over X), map := fun {X Y : T} => CategoryTheory.Over.map, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Over.mapFunctor_obj (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

(CategoryTheory.Over.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Over X)

source

@[simp]

theorem CategoryTheory.Over.mapFunctor_map (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) :

(CategoryTheory.Over.mapFunctor T).map f = CategoryTheory.Over.map f

source

instance CategoryTheory.Over.forget_reflects_iso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} :

(CategoryTheory.Over.forget X).ReflectsIsomorphisms

Equations

⋯ = ⋯

source

noncomputable def CategoryTheory.Over.mkIdTerminal {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} :

CategoryTheory.Limits.IsTerminal (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))

The identity over X is terminal.

Equations

CategoryTheory.Over.mkIdTerminal = CategoryTheory.CostructuredArrow.mkIdTerminal

Instances For

source

instance CategoryTheory.Over.forget_faithful {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} :

(CategoryTheory.Over.forget X).Faithful

Equations

⋯ = ⋯

source

theorem CategoryTheory.Over.epi_of_epi_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g) [hk : CategoryTheory.Epi k.left] :

CategoryTheory.Epi k

If k.left is an epimorphism, then k is an epimorphism. In other words, Over.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Over.epi_left_of_epi.

source

theorem CategoryTheory.Over.mono_of_mono_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g) [hk : CategoryTheory.Mono k.left] :

CategoryTheory.Mono k

If k.left is a monomorphism, then k is a monomorphism. In other words, Over.forget X reflects monomorphisms. The converse of CategoryTheory.Over.mono_left_of_mono.

This lemma is not an instance, to avoid loops in type class inference.

source

instance CategoryTheory.Over.mono_left_of_mono {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g) [CategoryTheory.Mono k] :

CategoryTheory.Mono k.left

If k is a monomorphism, then k.left is a monomorphism. In other words, Over.forget X preserves monomorphisms. The converse of CategoryTheory.Over.mono_of_mono_left.

Equations

⋯ = ⋯

source

def CategoryTheory.Over.iteratedSliceForward {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

CategoryTheory.Functor (CategoryTheory.Over f) (CategoryTheory.Over f.left)

Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceForward_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) (α : CategoryTheory.Over f) :

f.iteratedSliceForward.obj α = CategoryTheory.Over.mk α.hom.left

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceForward_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) {X✝ Y✝ : CategoryTheory.Over f} (κ : X✝ ⟶ Y✝) :

f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk κ.left.left ⋯

source

def CategoryTheory.Over.iteratedSliceBackward {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

CategoryTheory.Functor (CategoryTheory.Over f.left) (CategoryTheory.Over f)

Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceBackward_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) {X✝ Y✝ : CategoryTheory.Over f.left} (α : X✝ ⟶ Y✝) :

f.iteratedSliceBackward.map α = CategoryTheory.Over.homMk (CategoryTheory.Over.homMk α.left ⋯) ⋯

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceBackward_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) (g : CategoryTheory.Over f.left) :

f.iteratedSliceBackward.obj g = CategoryTheory.Over.mk (CategoryTheory.Over.homMk g.hom ⋯)

source

def CategoryTheory.Over.iteratedSliceEquiv {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

CategoryTheory.Over f ≌ CategoryTheory.Over f.left

Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquiv_unitIso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

f.iteratedSliceEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (g : CategoryTheory.Over f) => CategoryTheory.Over.isoMk (CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over f)).obj g).left.left) ⋯) ⋯) ⋯

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquiv_counitIso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

f.iteratedSliceEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (g : CategoryTheory.Over f.left) => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((f.iteratedSliceBackward.comp f.iteratedSliceForward).obj g).left) ⋯) ⋯

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquiv_inverse {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

f.iteratedSliceEquiv.inverse = f.iteratedSliceBackward

source

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquiv_functor {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

f.iteratedSliceEquiv.functor = f.iteratedSliceForward

source

theorem CategoryTheory.Over.iteratedSliceForward_forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

f.iteratedSliceForward.comp (CategoryTheory.Over.forget f.left) = (CategoryTheory.Over.forget f).comp (CategoryTheory.Over.forget X)

source

theorem CategoryTheory.Over.iteratedSliceBackward_forget_forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :

f.iteratedSliceBackward.comp ((CategoryTheory.Over.forget f).comp (CategoryTheory.Over.forget X)) = CategoryTheory.Over.forget f.left

source

def CategoryTheory.Over.post {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} (F : CategoryTheory.Functor T D) :

CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over (F.obj X))

A functor F : T ⥤ D induces a functor Over X ⥤ Over (F.obj X) in the obvious way.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Over.post_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} (F : CategoryTheory.Functor T D) (Y : CategoryTheory.Over X) :

(CategoryTheory.Over.post F).obj Y = CategoryTheory.Over.mk (F.map Y.hom)

source

@[simp]

theorem CategoryTheory.Over.post_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} (F : CategoryTheory.Functor T D) {X✝ Y✝ : CategoryTheory.Over X} (f : X✝ ⟶ Y✝) :

(CategoryTheory.Over.post F).map f = CategoryTheory.Over.homMk (F.map f.left) ⋯

source

def CategoryTheory.CostructuredArrow.toOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) :

CategoryTheory.Functor (CategoryTheory.CostructuredArrow F X) (CategoryTheory.Over X)

Reinterpreting an F-costructured arrow F.obj d ⟶ X as an arrow over X induces a functor CostructuredArrow F X ⥤ Over X.

Equations

CategoryTheory.CostructuredArrow.toOver F X = CategoryTheory.CostructuredArrow.pre F (CategoryTheory.Functor.id T) X

Instances For

source

@[simp]

theorem CategoryTheory.CostructuredArrow.toOver_obj_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) (X✝ : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)) :

((CategoryTheory.CostructuredArrow.toOver F X).obj X✝).hom = X✝.hom

source

@[simp]

theorem CategoryTheory.CostructuredArrow.toOver_map_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) {X✝ Y✝ : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)} (f : X✝ ⟶ Y✝) :

((CategoryTheory.CostructuredArrow.toOver F X).map f).right = CategoryTheory.CategoryStruct.id X✝.right

source

@[simp]

theorem CategoryTheory.CostructuredArrow.toOver_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) {X✝ Y✝ : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)} (f : X✝ ⟶ Y✝) :

((CategoryTheory.CostructuredArrow.toOver F X).map f).left = F.map f.left

source

@[simp]

theorem CategoryTheory.CostructuredArrow.toOver_obj_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) (X✝ : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)) :

((CategoryTheory.CostructuredArrow.toOver F X).obj X✝).right = X✝.right

source

@[simp]

theorem CategoryTheory.CostructuredArrow.toOver_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) (X✝ : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)) :

((CategoryTheory.CostructuredArrow.toOver F X).obj X✝).left = F.obj X✝.left

source

instance CategoryTheory.CostructuredArrow.instFaithfulOverToOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) [F.Faithful] :

(CategoryTheory.CostructuredArrow.toOver F X).Faithful

Equations

⋯ = ⋯

source

instance CategoryTheory.CostructuredArrow.instFullOverToOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) [F.Full] :

(CategoryTheory.CostructuredArrow.toOver F X).Full

Equations

⋯ = ⋯

source

instance CategoryTheory.CostructuredArrow.instEssSurjOverToOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) [F.EssSurj] :

(CategoryTheory.CostructuredArrow.toOver F X).EssSurj

Equations

⋯ = ⋯

source

instance CategoryTheory.CostructuredArrow.isEquivalence_toOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) [F.IsEquivalence] :

(CategoryTheory.CostructuredArrow.toOver F X).IsEquivalence

An equivalence F induces an equivalence CostructuredArrow F X ≌ Over X.

Equations

⋯ = ⋯

source

def CategoryTheory.Under {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

Type (max u₁ v₁)

The under category has as objects arrows with domain X and as morphisms commutative triangles.

Equations

CategoryTheory.Under X = CategoryTheory.StructuredArrow X (CategoryTheory.Functor.id T)

Instances For

source

instance CategoryTheory.instCategoryUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Under X)

Equations

CategoryTheory.instCategoryUnder X = CategoryTheory.commaCategory

source

instance CategoryTheory.Under.inhabited {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] [Inhabited T] :

Inhabited (CategoryTheory.Under default)

Equations

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

source

theorem CategoryTheory.Under.UnderMorphism.ext {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f g : U ⟶ V} (h : f.right = g.right) :

f = g

source

@[simp]

theorem CategoryTheory.Under.under_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Under X) :

U.left = { as := PUnit.unit }

source

@[simp]

theorem CategoryTheory.Under.id_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (U : CategoryTheory.Under X) :

(CategoryTheory.CategoryStruct.id U).right = CategoryTheory.CategoryStruct.id U.right

source

@[simp]

theorem CategoryTheory.Under.comp_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (a b c : CategoryTheory.Under X) (f : a ⟶ b) (g : b ⟶ c) :

(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right

source

@[simp]

theorem CategoryTheory.Under.w {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {A B : CategoryTheory.Under X} (f : A ⟶ B) :

CategoryTheory.CategoryStruct.comp A.hom f.right = B.hom

source

@[simp]

theorem CategoryTheory.Under.w_assoc {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {A B : CategoryTheory.Under X} (f : A ⟶ B) {Z : T} (h : B.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp A.hom (CategoryTheory.CategoryStruct.comp f.right h) = CategoryTheory.CategoryStruct.comp B.hom h

source

def CategoryTheory.Under.mk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

CategoryTheory.Under X

To give an object in the under category, it suffices to give an arrow with domain X.

Equations

CategoryTheory.Under.mk f = CategoryTheory.StructuredArrow.mk f

Instances For

source

@[simp]

theorem CategoryTheory.Under.mk_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

(CategoryTheory.Under.mk f).hom = f

source

@[simp]

theorem CategoryTheory.Under.mk_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

(CategoryTheory.Under.mk f).right = Y

source

def CategoryTheory.Under.homMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} (f : U.right ⟶ V.right) (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom := by aesop_cat) :

U ⟶ V

To give a morphism in the under category, it suffices to give a morphism fitting in a commutative triangle.

Equations

CategoryTheory.Under.homMk f w = CategoryTheory.StructuredArrow.homMk f w

Instances For

source

@[simp]

theorem CategoryTheory.Under.homMk_left_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} (f : U.right ⟶ V.right) (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom := by aesop_cat) :

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Under.homMk_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} (f : U.right ⟶ V.right) (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom := by aesop_cat) :

(CategoryTheory.Under.homMk f w).right = f

source

def CategoryTheory.Under.isoMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (hr : f.right ≅ g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom := by aesop_cat) :

f ≅ g

Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

Equations

CategoryTheory.Under.isoMk hr hw = CategoryTheory.StructuredArrow.isoMk hr hw

Instances For

source

@[simp]

theorem CategoryTheory.Under.isoMk_hom_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (hr : f.right ≅ g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) :

(CategoryTheory.Under.isoMk hr hw).hom.right = hr.hom

source

@[simp]

theorem CategoryTheory.Under.isoMk_inv_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (hr : f.right ≅ g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) :

(CategoryTheory.Under.isoMk hr hw).inv.right = hr.inv

source

def CategoryTheory.Under.forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

CategoryTheory.Functor (CategoryTheory.Under X) T

The forgetful functor mapping an arrow to its domain.

Equations

CategoryTheory.Under.forget X = CategoryTheory.Comma.snd (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T)

Instances For

source

@[simp]

theorem CategoryTheory.Under.forget_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X} :

(CategoryTheory.Under.forget X).obj U = U.right

source

@[simp]

theorem CategoryTheory.Under.forget_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f : U ⟶ V} :

(CategoryTheory.Under.forget X).map f = f.right

source

def CategoryTheory.Under.forgetCone {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

CategoryTheory.Limits.Cone (CategoryTheory.Under.forget X)

The natural cone over the forgetful functor Under X ⥤ T with cone point X.

Equations

CategoryTheory.Under.forgetCone X = { pt := X, π := { app := CategoryTheory.Comma.hom, naturality := ⋯ } }

Instances For

source

@[simp]

theorem CategoryTheory.Under.forgetCone_pt {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :

(CategoryTheory.Under.forgetCone X).pt = X

source

@[simp]

theorem CategoryTheory.Under.forgetCone_π_app {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (self : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T)) :

(CategoryTheory.Under.forgetCone X).π.app self = self.hom

source

def CategoryTheory.Under.map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

CategoryTheory.Functor (CategoryTheory.Under Y) (CategoryTheory.Under X)

A morphism X ⟶ Y induces a functor Under Y ⥤ Under X in the obvious way.

Equations

CategoryTheory.Under.map f = CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.id T) (CategoryTheory.Discrete.natTrans fun (x : CategoryTheory.Discrete PUnit.{1}) => f)

Instances For

source

@[simp]

theorem CategoryTheory.Under.map_obj_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y} :

((CategoryTheory.Under.map f).obj U).right = U.right

source

@[simp]

theorem CategoryTheory.Under.map_obj_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y} :

((CategoryTheory.Under.map f).obj U).hom = CategoryTheory.CategoryStruct.comp f U.hom

source

@[simp]

theorem CategoryTheory.Under.map_map_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U V : CategoryTheory.Under Y} {g : U ⟶ V} :

((CategoryTheory.Under.map f).map g).right = g.right

This section proves various equalities between functors that demonstrate, for instance, that under categories assemble into a functor mapFunctor : Tᵒᵖ ⥤ Cat.

source

theorem CategoryTheory.Under.mapId_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (Y : T) :

CategoryTheory.Under.map (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.Functor.id (CategoryTheory.Under Y)

Mapping by the identity morphism is just the identity functor.

source

def CategoryTheory.Under.mapId {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (Y : T) :

CategoryTheory.Under.map (CategoryTheory.CategoryStruct.id Y) ≅ CategoryTheory.Functor.id (CategoryTheory.Under Y)

Mapping by the identity morphism is just the identity functor.

Equations

CategoryTheory.Under.mapId Y = CategoryTheory.eqToIso ⋯

Instances For

source

theorem CategoryTheory.Under.mapForget_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

(CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) = CategoryTheory.Under.forget Y

Mapping by f and then forgetting is the same as forgetting.

source

def CategoryTheory.Under.mapForget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) :

(CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) ≅ CategoryTheory.Under.forget Y

The natural isomorphism arising from mapForget_eq.

Equations

CategoryTheory.Under.mapForget f = CategoryTheory.eqToIso ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Under.eqToHom_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} (e : U = V) :

(CategoryTheory.eqToHom e).right = CategoryTheory.eqToHom ⋯

source

theorem CategoryTheory.Under.mapComp_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Under.map (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Under.map g).comp (CategoryTheory.Under.map f)

Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

source

def CategoryTheory.Under.mapComp {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Under.map (CategoryTheory.CategoryStruct.comp f g) ≅ (CategoryTheory.Under.map g).comp (CategoryTheory.Under.map f)

The natural isomorphism arising from mapComp_eq.

Equations

CategoryTheory.Under.mapComp f g = CategoryTheory.eqToIso ⋯

Instances For

source

def CategoryTheory.Under.mapFunctor (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] :

CategoryTheory.Functor Tᵒᵖ CategoryTheory.Cat

The functor defined by the under categories.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Under.mapFunctor_obj (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] (X : Tᵒᵖ) :

(CategoryTheory.Under.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Under (Opposite.unop X))

source

@[simp]

theorem CategoryTheory.Under.mapFunctor_map (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] {X✝ Y✝ : Tᵒᵖ} (f : X✝ ⟶ Y✝) :

(CategoryTheory.Under.mapFunctor T).map f = CategoryTheory.Under.map f.unop

source

instance CategoryTheory.Under.forget_reflects_iso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} :

(CategoryTheory.Under.forget X).ReflectsIsomorphisms

Equations

⋯ = ⋯

source

noncomputable def CategoryTheory.Under.mkIdInitial {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} :

CategoryTheory.Limits.IsInitial (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id X))

The identity under X is initial.

Equations

CategoryTheory.Under.mkIdInitial = CategoryTheory.StructuredArrow.mkIdInitial

Instances For

source

instance CategoryTheory.Under.forget_faithful {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} :

(CategoryTheory.Under.forget X).Faithful

Equations

⋯ = ⋯

source

theorem CategoryTheory.Under.mono_of_mono_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g) [hk : CategoryTheory.Mono k.right] :

CategoryTheory.Mono k

If k.right is a monomorphism, then k is a monomorphism. In other words, Under.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Under.mono_right_of_mono.

source

theorem CategoryTheory.Under.epi_of_epi_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g) [hk : CategoryTheory.Epi k.right] :

CategoryTheory.Epi k

If k.right is an epimorphism, then k is an epimorphism. In other words, Under.forget X reflects epimorphisms. The converse of CategoryTheory.Under.epi_right_of_epi.

This lemma is not an instance, to avoid loops in type class inference.

source

instance CategoryTheory.Under.epi_right_of_epi {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g) [CategoryTheory.Epi k] :

CategoryTheory.Epi k.right

If k is an epimorphism, then k.right is an epimorphism. In other words, Under.forget X preserves epimorphisms. The converse of CategoryTheory.under.epi_of_epi_right.

Equations

⋯ = ⋯

source

def CategoryTheory.Under.post {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} (F : CategoryTheory.Functor T D) :

CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.Under (F.obj X))

A functor F : T ⥤ D induces a functor Under X ⥤ Under (F.obj X) in the obvious way.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Under.post_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} (F : CategoryTheory.Functor T D) {X✝ Y✝ : CategoryTheory.Under X} (f : X✝ ⟶ Y✝) :

(CategoryTheory.Under.post F).map f = CategoryTheory.Under.homMk (F.map f.right) ⋯

source

@[simp]

theorem CategoryTheory.Under.post_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : T} (F : CategoryTheory.Functor T D) (Y : CategoryTheory.Under X) :

(CategoryTheory.Under.post F).obj Y = CategoryTheory.Under.mk (F.map Y.hom)

source

def CategoryTheory.StructuredArrow.toUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) :

CategoryTheory.Functor (CategoryTheory.StructuredArrow X F) (CategoryTheory.Under X)

Reinterpreting an F-structured arrow X ⟶ F.obj d as an arrow under X induces a functor StructuredArrow X F ⥤ Under X.

Equations

CategoryTheory.StructuredArrow.toUnder X F = CategoryTheory.StructuredArrow.pre X F (CategoryTheory.Functor.id T)

Instances For

source

@[simp]

theorem CategoryTheory.StructuredArrow.toUnder_obj_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) (X✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))) :

((CategoryTheory.StructuredArrow.toUnder X F).obj X✝).right = F.obj X✝.right

source

@[simp]

theorem CategoryTheory.StructuredArrow.toUnder_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))} (f : X✝ ⟶ Y✝) :

((CategoryTheory.StructuredArrow.toUnder X F).map f).left = CategoryTheory.CategoryStruct.id X✝.left

source

@[simp]

theorem CategoryTheory.StructuredArrow.toUnder_map_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))} (f : X✝ ⟶ Y✝) :

((CategoryTheory.StructuredArrow.toUnder X F).map f).right = F.map f.right

source

@[simp]

theorem CategoryTheory.StructuredArrow.toUnder_obj_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) (X✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))) :

((CategoryTheory.StructuredArrow.toUnder X F).obj X✝).hom = X✝.hom

source

@[simp]

theorem CategoryTheory.StructuredArrow.toUnder_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) (X✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))) :

((CategoryTheory.StructuredArrow.toUnder X F).obj X✝).left = X✝.left

source

instance CategoryTheory.StructuredArrow.instFaithfulUnderToUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) [F.Faithful] :

(CategoryTheory.StructuredArrow.toUnder X F).Faithful

Equations

⋯ = ⋯

source

instance CategoryTheory.StructuredArrow.instFullUnderToUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) [F.Full] :

(CategoryTheory.StructuredArrow.toUnder X F).Full

Equations

⋯ = ⋯

source

instance CategoryTheory.StructuredArrow.instEssSurjUnderToUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) [F.EssSurj] :

(CategoryTheory.StructuredArrow.toUnder X F).EssSurj

Equations

⋯ = ⋯

source

instance CategoryTheory.StructuredArrow.isEquivalence_toUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) [F.IsEquivalence] :

(CategoryTheory.StructuredArrow.toUnder X F).IsEquivalence

An equivalence F induces an equivalence StructuredArrow X F ≌ Under X.

Equations

⋯ = ⋯

source

def CategoryTheory.Functor.toOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

CategoryTheory.Functor S (CategoryTheory.Over X)

Given X : T, to upgrade a functor F : S ⥤ T to a functor S ⥤ Over X, it suffices to provide maps F.obj Y ⟶ X for all Y making the obvious triangles involving all F.map g commute.

Equations

F.toOver X f h = F.toCostructuredArrow (CategoryTheory.Functor.id T) X f ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Functor.toOver_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) (Y : S) :

((F.toOver X f h).obj Y).left = F.obj Y

source

@[simp]

theorem CategoryTheory.Functor.toOver_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) {X✝ Y✝ : S} (g : X✝ ⟶ Y✝) :

((F.toOver X f h).map g).left = F.map g

source

def CategoryTheory.Functor.toOverCompForget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

(F.toOver X f ⋯).comp (CategoryTheory.Over.forget X) ≅ F

Upgrading a functor S ⥤ T to a functor S ⥤ Over X and composing with the forgetful functor Over X ⥤ T recovers the original functor.

Equations

F.toOverCompForget X f h = CategoryTheory.Iso.refl ((F.toOver X f ⋯).comp (CategoryTheory.Over.forget X))

Instances For

source

@[simp]

theorem CategoryTheory.Functor.toOver_comp_forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

(F.toOver X f ⋯).comp (CategoryTheory.Over.forget X) = F

source

def CategoryTheory.Functor.toUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :

CategoryTheory.Functor S (CategoryTheory.Under X)

Given X : T, to upgrade a functor F : S ⥤ T to a functor S ⥤ Under X, it suffices to provide maps X ⟶ F.obj Y for all Y making the obvious triangles involving all F.map g commute.

Equations