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

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

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

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) } }

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Over.w_assoc {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {A : CategoryTheory.Over X} {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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Over.mk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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

def CategoryTheory.Over.coeFromHom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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 }

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Over.homMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : autoParam (CategoryTheory.CategoryStruct.comp f V.hom = U.hom) _auto✝) : 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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Over.isoMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {g : CategoryTheory.Over X} (hl : f.left ≅ g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) : 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

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)

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

@[simp]

theorem CategoryTheory.Over.forget_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} {f : U ⟶ V} : (CategoryTheory.Over.forget X).map f = f.left

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

@[simp]

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

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 := ⋯ } }

def CategoryTheory.Over.map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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)

@[simp]

theorem CategoryTheory.Over.map_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X} : ((CategoryTheory.Over.map f).obj U).left = U.left

@[simp]

theorem CategoryTheory.Over.map_obj_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X} : ((CategoryTheory.Over.map f).obj U).hom = CategoryTheory.CategoryStruct.comp U.hom f

@[simp]

theorem CategoryTheory.Over.map_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X ⟶ Y} {U : CategoryTheory.Over X} {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.

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.

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 ⋯

theorem CategoryTheory.Over.mapForget_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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.

def CategoryTheory.Over.mapForget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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 ⋯

@[simp]

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

theorem CategoryTheory.Over.mapComp_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {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.

def CategoryTheory.Over.mapComp {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {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 ⋯

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

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

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 := ⋯ }

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Over.epi_of_epi_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {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.

theorem CategoryTheory.Over.mono_of_mono_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {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.

instance CategoryTheory.Over.mono_left_of_mono {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {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

• ⋯ = ⋯

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

@[simp]

theorem CategoryTheory.Over.iteratedSliceForward_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) : ∀ {X_1 Y : CategoryTheory.Over f} (κ : X_1 ⟶ Y), f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk κ.left.left ⋯

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.

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

@[simp]

theorem CategoryTheory.Over.iteratedSliceBackward_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) : ∀ {X_1 Y : CategoryTheory.Over f.left} (α : X_1 ⟶ Y), f.iteratedSliceBackward.map α = CategoryTheory.Over.homMk (CategoryTheory.Over.homMk α.left ⋯) ⋯

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.

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

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

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

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

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.

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)

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

@[simp]

theorem CategoryTheory.Over.post_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor T D) : ∀ {X_1 Y : CategoryTheory.Over X} (f : X_1 ⟶ Y), (CategoryTheory.Over.post F).map f = CategoryTheory.Over.homMk (F.map f.left) ⋯

@[simp]

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

def CategoryTheory.Over.post {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (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.

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

@[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_1 Y : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)} (f : X_1 ⟶ Y), ((CategoryTheory.CostructuredArrow.toOver F X).map f).left = F.map f.left

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

@[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_1 Y : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)} (f : X_1 ⟶ Y), ((CategoryTheory.CostructuredArrow.toOver F X).map f).right = CategoryTheory.CategoryStruct.id X_1.right

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

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

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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)

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

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.

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Under.w_assoc {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {A : CategoryTheory.Under X} {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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Under.mk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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

@[simp]

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

@[simp]

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

def CategoryTheory.Under.homMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X} {V : CategoryTheory.Under X} (f : U.right ⟶ V.right) (w : autoParam (CategoryTheory.CategoryStruct.comp U.hom f = V.hom) _auto✝) : 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

def CategoryTheory.Under.isoMk {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {g : CategoryTheory.Under X} (hr : f.right ≅ g.right) (hw : autoParam (CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) _auto✝) : 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

@[simp]

theorem CategoryTheory.Under.isoMk_hom_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {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

@[simp]

theorem CategoryTheory.Under.isoMk_inv_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {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

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)

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

@[simp]

theorem CategoryTheory.Under.forget_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X} {V : CategoryTheory.Under X} {f : U ⟶ V} : (CategoryTheory.Under.forget X).map f = f.right

@[simp]

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

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

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 := ⋯ } }

def CategoryTheory.Under.map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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)

@[simp]

theorem CategoryTheory.Under.map_obj_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y} : ((CategoryTheory.Under.map f).obj U).right = U.right

@[simp]

theorem CategoryTheory.Under.map_obj_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y} : ((CategoryTheory.Under.map f).obj U).hom = CategoryTheory.CategoryStruct.comp f U.hom

@[simp]

theorem CategoryTheory.Under.map_map_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y} {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.

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.

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 ⋯

theorem CategoryTheory.Under.mapForget_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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.

def CategoryTheory.Under.mapForget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {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 ⋯

@[simp]

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

theorem CategoryTheory.Under.mapComp_eq {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {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.

def CategoryTheory.Under.mapComp {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {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 ⋯

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

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

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.

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Under.mono_of_mono_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {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.

theorem CategoryTheory.Under.epi_of_epi_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {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.

instance CategoryTheory.Under.epi_right_of_epi {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {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

• ⋯ = ⋯

@[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_1 Y : CategoryTheory.Under X} (f : X_1 ⟶ Y), (CategoryTheory.Under.post F).map f = CategoryTheory.Under.homMk (F.map f.right) ⋯

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

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.

@[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_1 Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))} (f : X_1 ⟶ Y), ((CategoryTheory.StructuredArrow.toUnder X F).map f).left = CategoryTheory.CategoryStruct.id X_1.left

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

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

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

@[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_1 Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))} (f : X_1 ⟶ Y), ((CategoryTheory.StructuredArrow.toUnder X F).map f).right = F.map f.right

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)

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

@[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_1 Y : S} (g : X_1 ⟶ Y), ((F.toOver X f h).map g).left = F.map g

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 ⋯

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))

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

@[simp]

theorem CategoryTheory.Functor.toUnder_map_right {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) : ∀ {X_1 Y : S} (g : X_1 ⟶ Y), ((F.toUnder X f h).map g).right = F.map g

@[simp]

theorem CategoryTheory.Functor.toUnder_obj_right {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) (Y : S) : ((F.toUnder X f h).obj Y).right = F.obj Y

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

• F.toUnder X f h = F.toStructuredArrow X (CategoryTheory.Functor.id T) f ⋯

def CategoryTheory.Functor.toUnderCompForget {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) : (F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) ≅ F

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

Equations

• F.toUnderCompForget X f h = CategoryTheory.Iso.refl ((F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X))

@[simp]

theorem CategoryTheory.Functor.toUnder_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) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) : (F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) = F