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 .

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

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

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).toPrefunctor.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).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✝) : (_ : U.right.as = U.right.as) = (_ : U.right.as = U.right.as)

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 = CategoryTheory.CostructuredArrow.homMk f

@[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✝) : (_ : g.right.as = g.right.as) = (_ : g.right.as = g.right.as)

@[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✝) : (_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)

@[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).inv.left = hl.inv

@[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).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 = CategoryTheory.CostructuredArrow.isoMk hl

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 .

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).toPrefunctor.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).toPrefunctor.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, ι := CategoryTheory.NatTrans.mk CategoryTheory.Comma.hom }

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 .

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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.map g).left = g.left

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)

Mapping by the identity morphism is just the identity functor.

Equations

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

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.Functor.comp (CategoryTheory.Over.map f) (CategoryTheory.Over.map g)

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

Equations

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

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

Equations

• (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Over.forget X)) = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Over.forget X))

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.Faithful (CategoryTheory.Over.forget X)

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.Over.forget X)) = (_ : CategoryTheory.Faithful (CategoryTheory.Over.forget X))

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

• (_ : CategoryTheory.Mono k.left) = (_ : CategoryTheory.Mono k.left)

@[simp]

theorem CategoryTheory.Over.iteratedSliceForward_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) (α : CategoryTheory.Over f) : (CategoryTheory.Over.iteratedSliceForward f).toPrefunctor.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), (CategoryTheory.Over.iteratedSliceForward f).toPrefunctor.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) : (CategoryTheory.Over.iteratedSliceBackward f).toPrefunctor.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), (CategoryTheory.Over.iteratedSliceBackward f).toPrefunctor.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) : (CategoryTheory.Over.iteratedSliceEquiv f).functor = CategoryTheory.Over.iteratedSliceForward f

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquiv_unitIso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) : (CategoryTheory.Over.iteratedSliceEquiv f).unitIso = CategoryTheory.NatIso.ofComponents fun (g : CategoryTheory.Over f) => CategoryTheory.Over.isoMk (CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over f)).toPrefunctor.obj g).left.left))

@[simp]

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

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquiv_counitIso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) : (CategoryTheory.Over.iteratedSliceEquiv f).counitIso = CategoryTheory.NatIso.ofComponents fun (g : CategoryTheory.Over f.left) => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Over.iteratedSliceBackward f) (CategoryTheory.Over.iteratedSliceForward f)).toPrefunctor.obj g).left)

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) : CategoryTheory.Functor.comp (CategoryTheory.Over.iteratedSliceForward f) (CategoryTheory.Over.forget f.left) = CategoryTheory.Functor.comp (CategoryTheory.Over.forget f) (CategoryTheory.Over.forget X)

theorem CategoryTheory.Over.iteratedSliceBackward_forget_forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) : CategoryTheory.Functor.comp (CategoryTheory.Over.iteratedSliceBackward f) (CategoryTheory.Functor.comp (CategoryTheory.Over.forget f) (CategoryTheory.Over.forget X)) = CategoryTheory.Over.forget 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).toPrefunctor.obj Y = CategoryTheory.Over.mk (F.toPrefunctor.map Y.hom)

@[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).toPrefunctor.map f = CategoryTheory.Over.homMk (F.toPrefunctor.map f.left)

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.toPrefunctor.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_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 (CategoryTheory.Functor.comp F (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X✝)) : ((CategoryTheory.CostructuredArrow.toOver F X✝).toPrefunctor.obj X).right = X.right

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

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

@[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 (CategoryTheory.Functor.comp F (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X✝)) : ((CategoryTheory.CostructuredArrow.toOver F X✝).toPrefunctor.obj X).left = F.toPrefunctor.obj X.left

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.instFaithfulCostructuredArrowInstCategoryCostructuredArrowOverInstCategoryOverToOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (X : T) [CategoryTheory.Faithful F] : CategoryTheory.Faithful (CategoryTheory.CostructuredArrow.toOver F X)

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.CostructuredArrow.toOver F X)) = (_ : CategoryTheory.Faithful (CategoryTheory.CostructuredArrow.pre F (CategoryTheory.Functor.id T) X))

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

Equations

• CategoryTheory.CostructuredArrow.instFullCostructuredArrowInstCategoryCostructuredArrowOverInstCategoryOverToOver F X = let_fun this := inferInstance; this

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

Equations

• (_ : CategoryTheory.EssSurj (CategoryTheory.CostructuredArrow.toOver F X)) = (_ : CategoryTheory.EssSurj (CategoryTheory.CostructuredArrow.pre F (CategoryTheory.Functor.id T) X))

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

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

Equations

• CategoryTheory.CostructuredArrow.isEquivalenceToOver F X = CategoryTheory.CostructuredArrow.isEquivalencePre F (CategoryTheory.Functor.id T) X

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_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : X ⟶ Y) : (CategoryTheory.Under.mk f).right = Y

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

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_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).right = 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✝) : (_ : U.left.as = U.left.as) = (_ : U.left.as = U.left.as)

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 = CategoryTheory.StructuredArrow.homMk f

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 = CategoryTheory.StructuredArrow.isoMk hr

@[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).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).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).toPrefunctor.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).toPrefunctor.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, π := CategoryTheory.NatTrans.mk CategoryTheory.Comma.hom }

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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.map g).right = g.right

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

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

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.Functor.comp (CategoryTheory.Under.map g) (CategoryTheory.Under.map f)

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

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.ReflectsIsomorphisms (CategoryTheory.Under.forget X)

Equations

• (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Under.forget X)) = (_ : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Under.forget X))

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.Faithful (CategoryTheory.Under.forget X)

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.Under.forget X)) = (_ : CategoryTheory.Faithful (CategoryTheory.Under.forget X))

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

• (_ : CategoryTheory.Epi k.right) = (_ : CategoryTheory.Epi k.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).toPrefunctor.obj Y = CategoryTheory.Under.mk (F.toPrefunctor.map Y.hom)

@[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).toPrefunctor.map f = CategoryTheory.Under.homMk (F.toPrefunctor.map f.right)

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

@[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✝) (CategoryTheory.Functor.comp F (CategoryTheory.Functor.id T))) : ((CategoryTheory.StructuredArrow.toUnder X✝ F).toPrefunctor.obj X).left = X.left

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

@[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✝) (CategoryTheory.Functor.comp F (CategoryTheory.Functor.id T))) : ((CategoryTheory.StructuredArrow.toUnder X✝ F).toPrefunctor.obj X).right = F.toPrefunctor.obj X.right

@[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✝) (CategoryTheory.Functor.comp F (CategoryTheory.Functor.id T))) : ((CategoryTheory.StructuredArrow.toUnder X✝ F).toPrefunctor.obj X).hom = X.hom

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.instFaithfulStructuredArrowInstCategoryStructuredArrowUnderInstCategoryUnderToUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : T) (F : CategoryTheory.Functor D T) [CategoryTheory.Faithful F] : CategoryTheory.Faithful (CategoryTheory.StructuredArrow.toUnder X F)

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.StructuredArrow.toUnder X F)) = (_ : CategoryTheory.Faithful (CategoryTheory.StructuredArrow.pre X F (CategoryTheory.Functor.id T)))

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

Equations

• CategoryTheory.StructuredArrow.instFullStructuredArrowInstCategoryStructuredArrowUnderInstCategoryUnderToUnder X F = let_fun this := inferInstance; this

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

Equations

• (_ : CategoryTheory.EssSurj (CategoryTheory.StructuredArrow.toUnder X F)) = (_ : CategoryTheory.EssSurj (CategoryTheory.StructuredArrow.pre X F (CategoryTheory.Functor.id T)))

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

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

Equations

• CategoryTheory.StructuredArrow.isEquivalenceToUnder X F = CategoryTheory.StructuredArrow.isEquivalencePre X F (CategoryTheory.Functor.id T)

@[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.toPrefunctor.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map g) (f Z) = f Y) : ∀ {X_1 Y : S} (g : X_1 ⟶ Y), ((CategoryTheory.Functor.toOver F X f h).toPrefunctor.map g).left = F.toPrefunctor.map g

@[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.toPrefunctor.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map g) (f Z) = f Y) (Y : S) : ((CategoryTheory.Functor.toOver F X f h).toPrefunctor.obj Y).left = F.toPrefunctor.obj Y

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.toPrefunctor.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.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

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

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.toPrefunctor.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map g) (f Z) = f Y) : CategoryTheory.Functor.comp (CategoryTheory.Functor.toOver F X f (_ : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map g) (f Z) = f Y)) (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

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

@[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.toPrefunctor.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map g) (f Z) = f Y) : CategoryTheory.Functor.comp (CategoryTheory.Functor.toOver F X f (_ : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map g) (f Z) = f Y)) (CategoryTheory.Over.forget X) = F

@[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.toPrefunctor.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.toPrefunctor.map g) = f Z) (Y : S) : ((CategoryTheory.Functor.toUnder F X f h).toPrefunctor.obj Y).right = F.toPrefunctor.obj Y

@[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.toPrefunctor.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.toPrefunctor.map g) = f Z) : ∀ {X_1 Y : S} (g : X_1 ⟶ Y), ((CategoryTheory.Functor.toUnder F X f h).toPrefunctor.map g).right = F.toPrefunctor.map g

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.toPrefunctor.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.toPrefunctor.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

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

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

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

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