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₁} [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.

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Over.homMk_comp {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {U V W : Over X} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (w_f : CategoryStruct.comp f V.hom = U.hom) (w_g : CategoryStruct.comp g W.hom = V.hom) : homMk (CategoryStruct.comp f g) ⋯ = CategoryStruct.comp (homMk f w_f) (homMk g w_g)

This is useful when homMk (· ≫ ·) appears under Functor.map or a natural equivalence.

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Over.hom_left_inv_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (e : f ≅ g) : CategoryStruct.comp e.hom.left e.inv.left = CategoryStruct.id f.left

@[simp]

theorem CategoryTheory.Over.hom_left_inv_left_assoc {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (e : f ≅ g) {Z : T} (h : f.left ⟶ Z) : CategoryStruct.comp e.hom.left (CategoryStruct.comp e.inv.left h) = h

@[simp]

theorem CategoryTheory.Over.inv_left_hom_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (e : f ≅ g) : CategoryStruct.comp e.inv.left e.hom.left = CategoryStruct.id g.left

@[simp]

theorem CategoryTheory.Over.inv_left_hom_left_assoc {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (e : f ≅ g) {Z : T} (h : g.left ⟶ Z) : CategoryStruct.comp e.inv.left (CategoryStruct.comp e.hom.left h) = h

theorem CategoryTheory.Over.forall_iff {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (P : Over X → Prop) : (∀ (Y : Over X), P Y) ↔ ∀ (Y : T) (f : Y ⟶ X), P (mk f)

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

theorem CategoryTheory.Over.homMk_surjective {T : Type u₁} [Category.{v₁, u₁} T] {S : T} {X Y : Over S} (f : X ⟶ Y) : ∃ (g : X.left ⟶ Y.left) (hg : CategoryStruct.comp g Y.hom = X.hom), f = homMk g ⋯

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

The forgetful functor mapping an arrow to its domain.

@[simp]

theorem CategoryTheory.Over.forget_obj {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {U : Over X} : (forget X).obj U = U.left

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

If f is an isomorphism, map f is an equivalence of categories.

@[simp]

theorem CategoryTheory.Over.mapIso_functor {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom

@[simp]

theorem CategoryTheory.Over.mapIso_inverse {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv

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

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₁} [Category.{v₁, u₁} T] (Y : T) : map (CategoryStruct.id Y) = Functor.id (Over Y)

Mapping by the identity morphism is just the identity functor.

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

The natural isomorphism arising from mapForget_eq.

@[simp]

theorem CategoryTheory.Over.mapId_hom_app_left {T : Type u₁} [Category.{v₁, u₁} T] (Y : T) (X : Over Y) : ((mapId Y).hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Over.mapId_inv_app_left {T : Type u₁} [Category.{v₁, u₁} T] (Y : T) (X : Over Y) : ((mapId Y).inv.app X).left = CategoryStruct.id X.left

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

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

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

The natural isomorphism arising from mapForget_eq.

@[simp]

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

theorem CategoryTheory.Over.mapComp_eq {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryStruct.comp f g) = (map f).comp (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₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryStruct.comp f g) ≅ (map f).comp (map g)

The natural isomorphism arising from mapComp_eq.

@[simp]

theorem CategoryTheory.Over.mapComp_inv_app_left {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : Over X) : ((mapComp f g).inv.app X✝).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Over.mapComp_hom_app_left {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : Over X) : ((mapComp f g).hom.app X✝).left = CategoryStruct.id X✝.left

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

If f = g, then map f is naturally isomorphic to map g.

@[simp]

theorem CategoryTheory.Over.mapCongr_inv_app_left {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g) (X✝ : Over X) : ((mapCongr f g h).inv.app X✝).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Over.mapCongr_hom_app_left {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g) (X✝ : Over X) : ((mapCongr f g h).hom.app X✝).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.Over.mapCongr_rfl {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) : mapCongr f f ⋯ = Iso.refl (map f)

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

The functor defined by the over categories

@[simp]

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

@[simp]

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

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

noncomputable def CategoryTheory.Over.mkIdTerminal {T : Type u₁} [Category.{v₁, u₁} T] {X : T} : Limits.IsTerminal (mk (CategoryStruct.id X))

The identity over X is terminal.

@[simp]

theorem CategoryTheory.Over.mkIdTerminal_from_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (Y : Over X) : (mkIdTerminal.from Y).left = Y.hom

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

theorem CategoryTheory.Over.epi_of_epi_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (k : f ⟶ g) [hk : Epi k.left] : 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.

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

theorem CategoryTheory.Over.mono_of_mono_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (k : f ⟶ g) [hk : Mono k.left] : 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_homMk {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {U V : Over X} {f : U.left ⟶ V.left} [Mono f] (w : CategoryStruct.comp f V.hom = U.hom) : Mono (homMk f w)

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Over.iteratedSliceForward_obj {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (f : Over X) (α : Over f) : f.iteratedSliceForward.obj α = mk α.hom.left

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Over.iteratedSliceBackward_obj {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (f : Over X) (g : Over f.left) : f.iteratedSliceBackward.obj g = mk (homMk g.hom ⋯)

theorem CategoryTheory.Over.iteratedSliceBackward_forget {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (f : Over X) : f.iteratedSliceBackward.comp (forget f) = map f.hom

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def CategoryTheory.Over.iteratedSliceForwardNaturalityIso {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (p : f ⟶ g) : f.iteratedSliceForward.comp (map p.left) ≅ (map p).comp g.iteratedSliceForward

The naturality of the iterated slice equivalence up to isomorphism.

@[simp]

theorem CategoryTheory.Over.iteratedSliceForwardNaturalityIso_inv_app {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (p : f ⟶ g) (X✝ : Over f) : (iteratedSliceForwardNaturalityIso p).inv.app X✝ = CategoryStruct.id ((map p.left).obj (mk X✝.hom.left))

@[simp]

theorem CategoryTheory.Over.iteratedSliceForwardNaturalityIso_hom_app {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (p : f ⟶ g) (X✝ : Over f) : (iteratedSliceForwardNaturalityIso p).hom.app X✝ = CategoryStruct.id ((map p.left).obj (mk X✝.hom.left))

def CategoryTheory.Over.iteratedSliceEquivOverMapIso {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (p : f ⟶ g) : f.iteratedSliceForward.comp ((map p.left).comp g.iteratedSliceBackward) ≅ map p

The natural isomorphism relating the functor Over.map p to the functor Over.map p.left, mediated by the underlying functor of the iterated slice equivalence. Note that iteratedSliceForward can in fact be considered as a natural transformation from the 2-functor Over (C := Over X) : Over X ⥤ Cat to the composite 2-functor forget X ⋙ Over : Over X ⥤ Cat, and the naturality isormphism is then given by iteratedSliceEquivOverMapIso.

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquivOverMapIso_hom_app_left_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (p : f ⟶ g) (X✝ : Over f) : ((iteratedSliceEquivOverMapIso p).hom.app X✝).left.left = CategoryStruct.id X✝.left.left

@[simp]

theorem CategoryTheory.Over.iteratedSliceEquivOverMapIso_inv_app_left_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Over X} (p : f ⟶ g) (X✝ : Over f) : ((iteratedSliceEquivOverMapIso p).inv.app X✝).left.left = CategoryStruct.id X✝.left.left

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

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Over.post_comp {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) : post (F.comp G) = (post F).comp (post G)

def CategoryTheory.Over.postComp {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) : post (F.comp G) ≅ (post F).comp (post G)

post (F ⋙ G) is isomorphic (actually equal) to post F ⋙ post G.

@[simp]

theorem CategoryTheory.Over.postComp_hom_app_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) (X✝ : Over X) : ((postComp F G).hom.app X✝).left = CategoryStruct.id (G.obj (F.obj X✝.left))

@[simp]

theorem CategoryTheory.Over.postComp_inv_app_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) (X✝ : Over X) : ((postComp F G).inv.app X✝).left = CategoryStruct.id (G.obj (F.obj X✝.left))

def CategoryTheory.Over.postMap {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ⟶ G) : (post F).comp (map (e.app X)) ⟶ post G

A natural transformation F ⟶ G induces a natural transformation on Over X up to Over.map.

@[simp]

theorem CategoryTheory.Over.postMap_app {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ⟶ G) (Y : Over X) : (postMap e).app Y = homMk (e.app Y.left) ⋯

def CategoryTheory.Over.postCongr {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ≅ G) : (post F).comp (map (e.hom.app X)) ≅ post G

If F and G are naturally isomorphic, then Over.post F and Over.post G are also naturally isomorphic up to Over.map

@[simp]

theorem CategoryTheory.Over.postCongr_hom_app_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ≅ G) (X✝ : Over X) : ((postCongr e).hom.app X✝).left = e.hom.app X✝.left

@[simp]

theorem CategoryTheory.Over.postCongr_inv_app_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ≅ G) (X✝ : Over X) : ((postCongr e).inv.app X✝).left = e.inv.app X✝.left

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

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

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

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

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

If F is fully faithful, then so is Over.post F.

def CategoryTheory.Over.postAdjunctionRight {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} {F : Functor T D} {G : Functor D T} (a : F ⊣ G) : (post F).comp (map (a.counit.app Y)) ⊣ post G

If G is a right adjoint, then so is post G : Over Y ⥤ Over (G Y).

If the left adjoint of G is F, then the left adjoint of post G is given by (X ⟶ G Y) ↦ (F X ⟶ F G Y ⟶ Y).

@[simp]

theorem CategoryTheory.Over.postAdjunctionRight_unit_app {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} {F : Functor T D} {G : Functor D T} (a : F ⊣ G) (A : Over (G.obj Y)) : (postAdjunctionRight a).unit.app A = homMk (a.unit.app A.left) ⋯

@[simp]

theorem CategoryTheory.Over.postAdjunctionRight_counit_app {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} {F : Functor T D} {G : Functor D T} (a : F ⊣ G) (A : Over ((Functor.id D).obj Y)) : (postAdjunctionRight a).counit.app A = homMk (a.counit.app A.left) ⋯

instance CategoryTheory.Over.isRightAdjoint_post {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {Y : D} {G : Functor D T} [G.IsRightAdjoint] : (post G).IsRightAdjoint

def CategoryTheory.Over.postEquiv {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : Over X ≌ Over (F.functor.obj X)

An equivalence of categories induces an equivalence on over categories.

@[simp]

theorem CategoryTheory.Over.postEquiv_counitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).counitIso = NatIso.ofComponents (fun (A : Over (F.functor.obj X)) => isoMk (F.counitIso.app A.left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.postEquiv_unitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).unitIso = NatIso.ofComponents (fun (A : Over X) => isoMk (F.unitIso.app A.left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.postEquiv_inverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).inverse = (post F.inverse).comp (map (F.unitIso.inv.app X))

@[simp]

theorem CategoryTheory.Over.postEquiv_functor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).functor = post F.functor

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

post (Over.forget X) : Over f ⥤ Over (forget.obj f) is naturally isomorphic to the functor Over.iteratedSliceForward : Over f ⥤ Over f.left.

@[simp]

theorem CategoryTheory.Over.iteratedSliceForwardIsoPost_inv_app {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (f : Over X) (X✝ : Over f) : (iteratedSliceForwardIsoPost X f).inv.app X✝ = CategoryStruct.id (mk X✝.hom.left)

@[simp]

theorem CategoryTheory.Over.iteratedSliceForwardIsoPost_hom_app {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (f : Over X) (X✝ : Over f) : (iteratedSliceForwardIsoPost X f).hom.app X✝ = CategoryStruct.id (mk X✝.hom.left)

def CategoryTheory.Over.equivalenceOfIsTerminal {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsTerminal X) : Over X ≌ T

If X : T is terminal, then the over category of X is equivalent to T.

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsTerminal X) (Y : T) : (equivalenceOfIsTerminal hX).inverse.obj Y = mk (hX.from Y)

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_functor {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).functor = forget X

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsTerminal X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (equivalenceOfIsTerminal hX).inverse.map f = homMk f ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_unitIso {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).unitIso = NatIso.ofComponents (fun (Y : Over X) => isoMk (Iso.refl ((Functor.id (Over X)).obj Y).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_counitIso {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).counitIso = NatIso.ofComponents (fun (x : T) => Iso.refl (({ obj := fun (Y : T) => mk (hX.from Y), map := fun {X_1 Y : T} (f : X_1 ⟶ Y) => homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (forget X)).obj x)) ⋯

def CategoryTheory.Over.lift {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) : Functor J (Over X)

The induced functor to Over X from a functor J ⥤ C and natural maps sᵢ : X ⟶ Dᵢ. For the converse direction see CategoryTheory.WithTerminal.commaFromOver.

@[simp]

theorem CategoryTheory.Over.lift_obj {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) (j : J) : (Over.lift D s).obj j = mk (s.app j)

@[simp]

theorem CategoryTheory.Over.lift_map {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (Over.lift D s).map f = homMk (D.map f) ⋯

def CategoryTheory.Over.liftCone {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) (c : Limits.Cone D) (p : c.pt ⟶ X) (hp : ∀ (j : J), CategoryStruct.comp (c.π.app j) (s.app j) = p) : Limits.Cone (Over.lift D s)

The induced cone on Over X on the lifted functor.

@[simp]

theorem CategoryTheory.Over.liftCone_π_app {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) (c : Limits.Cone D) (p : c.pt ⟶ X) (hp : ∀ (j : J), CategoryStruct.comp (c.π.app j) (s.app j) = p) (j : J) : (liftCone D s c p hp).π.app j = homMk (c.π.app j) ⋯

@[simp]

theorem CategoryTheory.Over.liftCone_pt {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) (c : Limits.Cone D) (p : c.pt ⟶ X) (hp : ∀ (j : J), CategoryStruct.comp (c.π.app j) (s.app j) = p) : (liftCone D s c p hp).pt = mk p

def CategoryTheory.Over.isLimitLiftCone {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] [Nonempty J] (D : Functor J T) {X : T} (s : D ⟶ (Functor.const J).obj X) (c : Limits.Cone D) (p : c.pt ⟶ X) (hp : ∀ (j : J), CategoryStruct.comp (c.π.app j) (s.app j) = p) (hc : Limits.IsLimit c) : Limits.IsLimit (liftCone D s c p hp)

The lifted cone on Over X is a limit cone if the original cone was limiting and J is nonempty.

def CategoryTheory.Limits.Cone.overPost {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] {D : Functor J C} (c : Cone D) (j : J) : Cone (Over.post D)

Restrict a cone to the diagram over j. This preserves being limiting if the forgetful functor Over j ⥤ J is initial (see CategoryTheory.Limits.IsLimit.overPost).

@[simp]

theorem CategoryTheory.Limits.Cone.overPost_π_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] {D : Functor J C} (c : Cone D) (j : J) (k : Over j) : (c.overPost j).π.app k = Over.homMk (c.π.app k.left) ⋯

@[simp]

theorem CategoryTheory.Limits.Cone.overPost_pt {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] {D : Functor J C} (c : Cone D) (j : J) : (c.overPost j).pt = Over.mk (c.π.app j)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

Auxiliary definition for costructuredArrowToOverEquivalence.

@[simp]

theorem CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor_map {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) {X : T} (Y : Over X) {X✝ Y✝ : CostructuredArrow (toOver F X) Y} (f : X✝ ⟶ Y✝) : (functor F Y).map f = homMk f.left.left ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor_obj {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) {X : T} (Y : Over X) (Z : CostructuredArrow (toOver F X) Y) : (functor F Y).obj Z = mk Z.hom.left

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

Auxiliary definition for costructuredArrowToOverEquivalence.

@[simp]

theorem CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse_obj {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) {X : T} (Y : Over X) (Z : CostructuredArrow F Y.left) : (inverse F Y).obj Z = mk (Over.homMk Z.hom ⋯)

@[simp]

theorem CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.inverse_map {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) {X : T} (Y : Over X) {X✝ Y✝ : CostructuredArrow F Y.left} (f : X✝ ⟶ Y✝) : (inverse F Y).map f = homMk (homMk f.left ⋯) ⋯

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

A category of costructured arrows for a functor toOver F X identifies to a category of costructured arrows for F.

def CategoryTheory.Under {T : Type u₁} [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.

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Under.homMk_comp {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {U V W : Under X} (f : U.right ⟶ V.right) (g : V.right ⟶ W.right) (w_f : CategoryStruct.comp U.hom f = V.hom) (w_g : CategoryStruct.comp V.hom g = W.hom) : homMk (CategoryStruct.comp f g) ⋯ = CategoryStruct.comp (homMk f w_f) (homMk g w_g)

This is useful when homMk (· ≫ ·) appears under Functor.map or a natural equivalence.

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Under.hom_right_inv_right {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Under X} (e : f ≅ g) : CategoryStruct.comp e.hom.right e.inv.right = CategoryStruct.id f.right

@[simp]

theorem CategoryTheory.Under.hom_right_inv_right_assoc {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Under X} (e : f ≅ g) {Z : T} (h : f.right ⟶ Z) : CategoryStruct.comp e.hom.right (CategoryStruct.comp e.inv.right h) = h

@[simp]

theorem CategoryTheory.Under.inv_right_hom_right {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Under X} (e : f ≅ g) : CategoryStruct.comp e.inv.right e.hom.right = CategoryStruct.id g.right

@[simp]

theorem CategoryTheory.Under.inv_right_hom_right_assoc {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Under X} (e : f ≅ g) {Z : T} (h : g.right ⟶ Z) : CategoryStruct.comp e.inv.right (CategoryStruct.comp e.hom.right h) = h

theorem CategoryTheory.Under.forall_iff {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (P : Under X → Prop) : (∀ (Y : Under X), P Y) ↔ ∀ (Y : T) (f : X ⟶ Y), P (mk f)

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

theorem CategoryTheory.Under.homMk_surjective {T : Type u₁} [Category.{v₁, u₁} T] {S : T} {X Y : Under S} (f : X ⟶ Y) : ∃ (g : X.right ⟶ Y.right) (hg : CategoryStruct.comp X.hom g = Y.hom), homMk g ⋯ = f

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

The forgetful functor mapping an arrow to its domain.

@[simp]

theorem CategoryTheory.Under.forget_obj {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {U : Under X} : (forget X).obj U = U.right

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

If f is an isomorphism, map f is an equivalence of categories.

@[simp]

theorem CategoryTheory.Under.mapIso_functor {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom

@[simp]

theorem CategoryTheory.Under.mapIso_inverse {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv

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

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₁} [Category.{v₁, u₁} T] (Y : T) : map (CategoryStruct.id Y) = Functor.id (Under Y)

Mapping by the identity morphism is just the identity functor.

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

Mapping by the identity morphism is just the identity functor.

@[simp]

theorem CategoryTheory.Under.mapId_hom {T : Type u₁} [Category.{v₁, u₁} T] (Y : T) : (mapId Y).hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Under.mapId_inv {T : Type u₁} [Category.{v₁, u₁} T] (Y : T) : (mapId Y).inv = eqToHom ⋯

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

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

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

The natural isomorphism arising from mapForget_eq.

@[simp]

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

theorem CategoryTheory.Under.mapComp_eq {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryStruct.comp f g) = (map g).comp (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₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryStruct.comp f g) ≅ (map g).comp (map f)

The natural isomorphism arising from mapComp_eq.

@[simp]

theorem CategoryTheory.Under.mapComp_hom {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : (mapComp f g).hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Under.mapComp_inv {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : (mapComp f g).inv = eqToHom ⋯

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

If f = g, then map f is naturally isomorphic to map g.

@[simp]

theorem CategoryTheory.Under.mapCongr_hom_app {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g) (X✝ : Under Y) : (mapCongr f g h).hom.app X✝ = eqToHom ⋯

@[simp]

theorem CategoryTheory.Under.mapCongr_inv_app {T : Type u₁} [Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g) (X✝ : Under Y) : (mapCongr f g h).inv.app X✝ = eqToHom ⋯

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

The functor defined by the under categories

@[simp]

theorem CategoryTheory.Under.mapFunctor_obj (T : Type u₁) [Category.{v₁, u₁} T] (X : Tᵒᵖ) : (mapFunctor T).obj X = Cat.of (Under (Opposite.unop X))

@[simp]

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

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

noncomputable def CategoryTheory.Under.mkIdInitial {T : Type u₁} [Category.{v₁, u₁} T] {X : T} : Limits.IsInitial (mk (CategoryStruct.id X))

The identity under X is initial.

@[simp]

theorem CategoryTheory.Under.mkIdInitial_to_right {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (Y : Under X) : (mkIdInitial.to Y).right = Y.hom

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

theorem CategoryTheory.Under.mono_of_mono_right {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Under X} (k : f ⟶ g) [hk : Mono k.right] : 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.

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

theorem CategoryTheory.Under.epi_of_epi_right {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {f g : Under X} (k : f ⟶ g) [hk : Epi k.right] : 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_homMk {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {U V : Under X} {f : U.right ⟶ V.right} [Epi f] (w : CategoryStruct.comp U.hom f = V.hom) : Epi (homMk f w)

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

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

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Under.post_comp {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) : post (F.comp G) = (post F).comp (post G)

def CategoryTheory.Under.postComp {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) : post (F.comp G) ≅ (post F).comp (post G)

post (F ⋙ G) is isomorphic (actually equal) to post F ⋙ post G.

@[simp]

theorem CategoryTheory.Under.postComp_hom_app_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) (X✝ : Under X) : ((postComp F G).hom.app X✝).right = CategoryStruct.id (G.obj (F.obj X✝.right))

@[simp]

theorem CategoryTheory.Under.postComp_inv_app_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {E : Type u_1} [Category.{v_1, u_1} E] (F : Functor T D) (G : Functor D E) (X✝ : Under X) : ((postComp F G).inv.app X✝).right = CategoryStruct.id (G.obj (F.obj X✝.right))

def CategoryTheory.Under.postMap {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ⟶ G) : post F ⟶ (post G).comp (map (e.app X))

A natural transformation F ⟶ G induces a natural transformation on Under X up to Under.map.

@[simp]

theorem CategoryTheory.Under.postMap_app {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ⟶ G) (Y : Under X) : (postMap e).app Y = homMk (e.app Y.right) ⋯

def CategoryTheory.Under.postCongr {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ≅ G) : post F ≅ (post G).comp (map (e.hom.app X))

If F and G are naturally isomorphic, then Under.post F and Under.post G are also naturally isomorphic up to Under.map

@[simp]

theorem CategoryTheory.Under.postCongr_hom_app_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ≅ G) (X✝ : Under X) : ((postCongr e).hom.app X✝).right = e.hom.app X✝.right

@[simp]

theorem CategoryTheory.Under.postCongr_inv_app_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F G : Functor T D} (e : F ≅ G) (X✝ : Under X) : ((postCongr e).inv.app X✝).right = e.inv.app X✝.right

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

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

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

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

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

If F is fully faithful, then so is Under.post F.

def CategoryTheory.Under.postAdjunctionLeft {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} {G : Functor D T} (a : F ⊣ G) : post F ⊣ (post G).comp (map (a.unit.app X))

If F is a left adjoint, then so is post F : Under X ⥤ Under (F X).

If the right adjoint of F is G, then the right adjoint of post F is given by (F X ⟶ Y) ↦ (X ⟶ G F X ⟶ G Y).

@[simp]

theorem CategoryTheory.Under.postAdjunctionLeft_unit_app {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} {G : Functor D T} (a : F ⊣ G) (A : Under ((Functor.id T).obj X)) : (postAdjunctionLeft a).unit.app A = homMk (a.unit.app A.right) ⋯

@[simp]

theorem CategoryTheory.Under.postAdjunctionLeft_counit_app {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} {G : Functor D T} (a : F ⊣ G) (A : Under (F.obj ((Functor.id T).obj X))) : (postAdjunctionLeft a).counit.app A = homMk (a.counit.app A.right) ⋯

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

def CategoryTheory.Under.postEquiv {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : Under X ≌ Under (F.functor.obj X)

An equivalence of categories induces an equivalence on under categories.

@[simp]

theorem CategoryTheory.Under.postEquiv_unitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).unitIso = NatIso.ofComponents (fun (A : Under X) => isoMk (F.unitIso.app A.right) ⋯) ⋯

@[simp]

theorem CategoryTheory.Under.postEquiv_functor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).functor = post F.functor

@[simp]

theorem CategoryTheory.Under.postEquiv_counitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).counitIso = NatIso.ofComponents (fun (A : Under (F.functor.obj X)) => isoMk (F.counitIso.app A.right) ⋯) ⋯

@[simp]

theorem CategoryTheory.Under.postEquiv_inverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (X : T) (F : T ≌ D) : (postEquiv X F).inverse = (post F.inverse).comp (map (F.unitIso.hom.app X))

def CategoryTheory.Under.equivalenceOfIsInitial {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsInitial X) : Under X ≌ T

If X : T is initial, then the under category of X is equivalent to T.

@[simp]

theorem CategoryTheory.Under.equivalenceOfIsInitial_counitIso {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsInitial X) : (equivalenceOfIsInitial hX).counitIso = NatIso.ofComponents (fun (x : T) => Iso.refl (({ obj := fun (Y : T) => mk (hX.to Y), map := fun {X_1 Y : T} (f : X_1 ⟶ Y) => homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (forget X)).obj x)) ⋯

@[simp]

theorem CategoryTheory.Under.equivalenceOfIsInitial_unitIso {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsInitial X) : (equivalenceOfIsInitial hX).unitIso = NatIso.ofComponents (fun (Y : Under X) => isoMk (Iso.refl ((Functor.id (Under X)).obj Y).right) ⋯) ⋯

@[simp]

theorem CategoryTheory.Under.equivalenceOfIsInitial_functor {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsInitial X) : (equivalenceOfIsInitial hX).functor = forget X

@[simp]

theorem CategoryTheory.Under.equivalenceOfIsInitial_inverse_map {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsInitial X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (equivalenceOfIsInitial hX).inverse.map f = homMk f ⋯

@[simp]

theorem CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (hX : Limits.IsInitial X) (Y : T) : (equivalenceOfIsInitial hX).inverse.obj Y = mk (hX.to Y)

def CategoryTheory.Under.lift {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) : Functor J (Under X)

The induced functor to Under X from a functor J ⥤ C and natural maps sᵢ : X ⟶ Dᵢ.

@[simp]

theorem CategoryTheory.Under.lift_map {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (Under.lift D s).map f = homMk (D.map f) ⋯

@[simp]

theorem CategoryTheory.Under.lift_obj {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) (j : J) : (Under.lift D s).obj j = mk (s.app j)

def CategoryTheory.Under.liftCocone {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) (c : Limits.Cocone D) (p : X ⟶ c.pt) (hp : ∀ (j : J), CategoryStruct.comp (s.app j) (c.ι.app j) = p) : Limits.Cocone (Under.lift D s)

The induced cocone on Under X from on the lifted functor.

@[simp]

theorem CategoryTheory.Under.liftCocone_pt {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) (c : Limits.Cocone D) (p : X ⟶ c.pt) (hp : ∀ (j : J), CategoryStruct.comp (s.app j) (c.ι.app j) = p) : (liftCocone D s c p hp).pt = mk p

@[simp]

theorem CategoryTheory.Under.liftCocone_ι_app {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) (c : Limits.Cocone D) (p : X ⟶ c.pt) (hp : ∀ (j : J), CategoryStruct.comp (s.app j) (c.ι.app j) = p) (j : J) : (liftCocone D s c p hp).ι.app j = homMk (c.ι.app j) ⋯

def CategoryTheory.Under.isColimitLiftCocone {T : Type u₁} [Category.{v₁, u₁} T] {J : Type u_1} [Category.{v_1, u_1} J] [Nonempty J] (D : Functor J T) {X : T} (s : (Functor.const J).obj X ⟶ D) (c : Limits.Cocone D) (p : X ⟶ c.pt) (hp : ∀ (j : J), CategoryStruct.comp (s.app j) (c.ι.app j) = p) (hc : Limits.IsColimit c) : Limits.IsColimit (liftCocone D s c p hp)

The lifted cocone on Under X is a colimit cocone if the original cocone was colimiting and J is nonempty.

def CategoryTheory.Limits.Cocone.underPost {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] {D : Functor J C} (c : Cocone D) (j : J) : Cocone (Under.post D)

Restrict a cocone to the diagram under j. This preserves being colimiting if the forgetful functor Over j ⥤ J is final (see CategoryTheory.Limits.IsColimit.underPost).

@[simp]

theorem CategoryTheory.Limits.Cocone.underPost_pt {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] {D : Functor J C} (c : Cocone D) (j : J) : (c.underPost j).pt = Under.mk (c.ι.app j)

@[simp]

theorem CategoryTheory.Limits.Cocone.underPost_ι_app {J : Type u_1} {C : Type u_2} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] {D : Functor J C} (c : Cocone D) (j : J) (k : Under j) : (c.underPost j).ι.app k = Under.homMk (c.ι.app k.right) ⋯

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem CategoryTheory.Functor.essImage.of_overPost {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} {Y : Over (F.obj X)} : (Over.post F).essImage Y → F.essImage Y.left

theorem CategoryTheory.Functor.essImage.of_underPost {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} {Y : Under (F.obj X)} : (Under.post F).essImage Y → F.essImage Y.right

@[simp]

theorem CategoryTheory.Functor.essImage_overPost {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} [F.Full] {Y : Over (F.obj X)} : (Over.post F).essImage Y ↔ F.essImage Y.left

The essential image of Over.post F where F is full is the same as the essential image of F.

@[simp]

theorem CategoryTheory.Functor.essImage_underPost {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {X : T} {F : Functor T D} [F.Full] {Y : Under (F.obj X)} : (Under.post F).essImage Y ↔ F.essImage Y.right

The essential image of Under.post F where F is full is the same as the essential image of F.

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

@[simp]

theorem CategoryTheory.Functor.toOver_obj_left {T : Type u₁} [Category.{v₁, u₁} T] {S : Type u₂} [Category.{v₂, u₂} S] (F : Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), 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₁} [Category.{v₁, u₁} T] {S : Type u₂} [Category.{v₂, u₂} S] (F : Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), 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

def CategoryTheory.Functor.toOverCompForget {T : Type u₁} [Category.{v₁, u₁} T] {S : Type u₂} [Category.{v₂, u₂} S] (F : Functor S T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryStruct.comp (F.map g) (f Z) = f Y) : (F.toOver X f ⋯).comp (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.

@[simp]

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.toUnderCompForget {T : Type u₁} [Category.{v₁, u₁} T] {S : Type u₂} [Category.{v₂, u₂} S] (F : Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryStruct.comp (f Y) (F.map g) = f Z) : (F.toUnder X f ⋯).comp (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.

@[simp]

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

def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) : Functor (StructuredArrow X (proj Y F)) (StructuredArrow Y ((Under.forget X).comp F))

A functor from the structured arrow category on the projection functor for any structured arrow category.

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow X (proj Y F)) : ((functor F Y X).obj Y✝).right.right = Y✝.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow X (proj Y F)) : ((functor F Y X).obj Y✝).right.hom = Y✝.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow X (proj Y F)) : ((functor F Y X).obj Y✝).right.left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow X (proj Y F)) : ((functor F Y X).obj Y✝).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow X (proj Y F)) : ((functor F Y X).obj Y✝).hom = Y✝.right.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) {X✝ Y✝ : StructuredArrow X (proj Y F)} (g : X✝ ⟶ Y✝) : ((functor F Y X).map g).right.right = g.right.right

def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) : Functor (StructuredArrow Y ((Under.forget X).comp F)) (StructuredArrow X (proj Y F))

The inverse functor of ofStructuredArrowProjEquivalence.functor.

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow Y ((Under.forget X).comp F)) : ((inverse F Y X).obj Y✝).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow Y ((Under.forget X).comp F)) : ((inverse F Y X).obj Y✝).right.hom = Y✝.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow Y ((Under.forget X).comp F)) : ((inverse F Y X).obj Y✝).right.right = Y✝.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) {X✝ Y✝ : StructuredArrow Y ((Under.forget X).comp F)} (g : X✝ ⟶ Y✝) : ((inverse F Y X).map g).right.right = g.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow Y ((Under.forget X).comp F)) : ((inverse F Y X).obj Y✝).right.left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) (Y✝ : StructuredArrow Y ((Under.forget X).comp F)) : ((inverse F Y X).obj Y✝).hom = Y✝.right.hom

def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D T) (Y : T) (X : D) : StructuredArrow X (proj Y F) ≌ StructuredArrow Y ((Under.forget X).comp F)

Characterization of the structured arrow category on the projection functor of any structured arrow category.

def CategoryTheory.StructuredArrow.ofDiagEquivalence.functor {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : Functor (StructuredArrow X (Functor.diag T)) (StructuredArrow X.2 (Under.forget X.1))

The canonical functor from the structured arrow category on the diagonal functor T ⥤ T × T to the structured arrow category on Under.forget.

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_hom {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X (Functor.diag T)) : ((functor X).obj Y).right.hom = Y.hom.1

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_right {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : StructuredArrow X (Functor.diag T)} (g : X✝ ⟶ Y✝) : ((functor X).map g).right.right = g.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_right {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X (Functor.diag T)) : ((functor X).obj Y).right.right = Y.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X (Functor.diag T)) : ((functor X).obj Y).hom = Y.hom.2

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_left_as {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X (Functor.diag T)) : ((functor X).obj Y).left.as = PUnit.unit

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_left_as {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X (Functor.diag T)) : ((functor X).obj Y).right.left.as = PUnit.unit

def CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : Functor (StructuredArrow X.2 (Under.forget X.1)) (StructuredArrow X (Functor.diag T))

The inverse functor of ofDiagEquivalence.functor.

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X.2 (Under.forget X.1)) : ((inverse X).obj Y).hom = (Y.right.hom, Y.hom)

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_right {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : StructuredArrow X.2 (Under.forget X.1)} (g : X✝ ⟶ Y✝) : ((inverse X).map g).right = g.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_right {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X.2 (Under.forget X.1)) : ((inverse X).obj Y).right = Y.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_left_as {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : StructuredArrow X.2 (Under.forget X.1)) : ((inverse X).obj Y).left.as = PUnit.unit

def CategoryTheory.StructuredArrow.ofDiagEquivalence {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : StructuredArrow X (Functor.diag T) ≌ StructuredArrow X.2 (Under.forget X.1)

Characterization of the structured arrow category on the diagonal functor T ⥤ T × T.

noncomputable def CategoryTheory.StructuredArrow.ofDiagEquivalence' {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : StructuredArrow X (Functor.diag T) ≌ StructuredArrow X.1 (Under.forget X.2)

A version of StructuredArrow.ofDiagEquivalence with the roles of the first and second projection swapped.

def CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : Functor (StructuredArrow c (Comma.fst F G)) (Comma ((Under.forget c).comp F) G)

The functor used to define the equivalence ofCommaSndEquivalence.

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (X : StructuredArrow c (Comma.fst F G)) : ((ofCommaSndEquivalenceFunctor F G c).obj X).left = Under.mk X.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (X : StructuredArrow c (Comma.fst F G)) : ((ofCommaSndEquivalenceFunctor F G c).obj X).hom = X.right.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (X : StructuredArrow c (Comma.fst F G)) : ((ofCommaSndEquivalenceFunctor F G c).obj X).right = X.right.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : StructuredArrow c (Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((ofCommaSndEquivalenceFunctor F G c).map f).left = Under.homMk f.right.left ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : StructuredArrow c (Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((ofCommaSndEquivalenceFunctor F G c).map f).right = f.right.right

def CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : Functor (Comma ((Under.forget c).comp F) G) (StructuredArrow c (Comma.fst F G))

The inverse functor used to define the equivalence ofCommaSndEquivalence.

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : Comma ((Under.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((ofCommaSndEquivalenceInverse F G c).map g).right.right = g.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Under.forget c).comp F) G) : ((ofCommaSndEquivalenceInverse F G c).obj Y).hom = Y.left.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Under.forget c).comp F) G) : ((ofCommaSndEquivalenceInverse F G c).obj Y).right.left = Y.left.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : Comma ((Under.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((ofCommaSndEquivalenceInverse F G c).map g).right.left = g.left.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Under.forget c).comp F) G) : ((ofCommaSndEquivalenceInverse F G c).obj Y).right.hom = Y.hom

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Under.forget c).comp F) G) : ((ofCommaSndEquivalenceInverse F G c).obj Y).right.right = Y.right

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Under.forget c).comp F) G) : ((ofCommaSndEquivalenceInverse F G c).obj Y).left.as = PUnit.unit

def CategoryTheory.StructuredArrow.ofCommaSndEquivalence {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : StructuredArrow c (Comma.fst F G) ≌ Comma ((Under.forget c).comp F) G

There is a canonical equivalence between the structured arrow category with domain c on the functor Comma.fst F G : Comma F G ⥤ F and the comma category over Under.forget c ⋙ F : Under c ⥤ T and G.

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalence_counitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaSndEquivalence F G c).counitIso = NatIso.ofComponents (fun (x : Comma ((Under.forget c).comp F) G) => Iso.refl (((ofCommaSndEquivalenceInverse F G c).comp (ofCommaSndEquivalenceFunctor F G c)).obj x)) ⋯

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalence_functor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaSndEquivalence F G c).functor = ofCommaSndEquivalenceFunctor F G c

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalence_inverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaSndEquivalence F G c).inverse = ofCommaSndEquivalenceInverse F G c

@[simp]

theorem CategoryTheory.StructuredArrow.ofCommaSndEquivalence_unitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaSndEquivalence F G c).unitIso = NatIso.ofComponents (fun (x : StructuredArrow c (Comma.fst F G)) => Iso.refl ((Functor.id (StructuredArrow c (Comma.fst F G))).obj x)) ⋯

def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) : Functor (CostructuredArrow (proj F Y) X) (CostructuredArrow ((Over.forget X).comp F) Y)

A functor from the costructured arrow category on the projection functor for any costructured arrow category.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_right_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow (proj F Y) X) : ((functor F Y X).obj Y✝).left.right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow (proj F Y) X) : ((functor F Y X).obj Y✝).hom = Y✝.left.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_left_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) {X✝ Y✝ : CostructuredArrow (proj F Y) X} (g : X✝ ⟶ Y✝) : ((functor F Y X).map g).left.left = g.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow (proj F Y) X) : ((functor F Y X).obj Y✝).left.hom = Y✝.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_right_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow (proj F Y) X) : ((functor F Y X).obj Y✝).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_obj_left_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow (proj F Y) X) : ((functor F Y X).obj Y✝).left.left = Y✝.left.left

def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) : Functor (CostructuredArrow ((Over.forget X).comp F) Y) (CostructuredArrow (proj F Y) X)

The inverse functor of ofCostructuredArrowProjEquivalence.functor.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow ((Over.forget X).comp F) Y) : ((inverse F Y X).obj Y✝).left.left = Y✝.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow ((Over.forget X).comp F) Y) : ((inverse F Y X).obj Y✝).hom = Y✝.left.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow ((Over.forget X).comp F) Y) : ((inverse F Y X).obj Y✝).left.hom = Y✝.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) {X✝ Y✝ : CostructuredArrow ((Over.forget X).comp F) Y} (g : X✝ ⟶ Y✝) : ((inverse F Y X).map g).left.left = g.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_right_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow ((Over.forget X).comp F) Y) : ((inverse F Y X).obj Y✝).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_right_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) (Y✝ : CostructuredArrow ((Over.forget X).comp F) Y) : ((inverse F Y X).obj Y✝).left.right.as = PUnit.unit

def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor T D) (Y : D) (X : T) : CostructuredArrow (proj F Y) X ≌ CostructuredArrow ((Over.forget X).comp F) Y

Characterization of the costructured arrow category on the projection functor of any costructured arrow category.

def CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : Functor (CostructuredArrow (Functor.diag T) X) (CostructuredArrow (Over.forget X.1) X.2)

The canonical functor from the costructured arrow category on the diagonal functor T ⥤ T × T to the costructured arrow category on Under.forget.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_left {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Functor.diag T) X) : ((functor X).obj Y).left.left = Y.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_hom {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Functor.diag T) X) : ((functor X).obj Y).left.hom = Y.hom.1

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_right_as {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Functor.diag T) X) : ((functor X).obj Y).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_right_as {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Functor.diag T) X) : ((functor X).obj Y).left.right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Functor.diag T) X) : ((functor X).obj Y).hom = Y.hom.2

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_left_left {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : CostructuredArrow (Functor.diag T) X} (g : X✝ ⟶ Y✝) : ((functor X).map g).left.left = g.left

def CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : Functor (CostructuredArrow (Over.forget X.1) X.2) (CostructuredArrow (Functor.diag T) X)

The inverse functor of ofDiagEquivalence.functor.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_right_as {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Over.forget X.1) X.2) : ((inverse X).obj Y).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_left {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Over.forget X.1) X.2) : ((inverse X).obj Y).left = Y.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) (Y : CostructuredArrow (Over.forget X.1) X.2) : ((inverse X).obj Y).hom = (Y.left.hom, Y.hom)

@[simp]

theorem CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_map_left {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : CostructuredArrow (Over.forget X.1) X.2} (g : X✝ ⟶ Y✝) : ((inverse X).map g).left = g.left.left

def CategoryTheory.CostructuredArrow.ofDiagEquivalence {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : CostructuredArrow (Functor.diag T) X ≌ CostructuredArrow (Over.forget X.1) X.2

Characterization of the costructured arrow category on the diagonal functor T ⥤ T × T.

noncomputable def CategoryTheory.CostructuredArrow.ofDiagEquivalence' {T : Type u₁} [Category.{v₁, u₁} T] (X : T × T) : CostructuredArrow (Functor.diag T) X ≌ CostructuredArrow (Over.forget X.2) X.1

A version of CostructuredArrow.ofDiagEquivalence with the roles of the first and second projection swapped.

def CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : Functor (CostructuredArrow (Comma.fst F G) c) (Comma ((Over.forget c).comp F) G)

The functor used to define the equivalence ofCommaFstEquivalence.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (X : CostructuredArrow (Comma.fst F G) c) : ((ofCommaFstEquivalenceFunctor F G c).obj X).right = X.left.right

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_map_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : CostructuredArrow (Comma.fst F G) c} (f : X✝ ⟶ Y✝) : ((ofCommaFstEquivalenceFunctor F G c).map f).right = f.left.right

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (X : CostructuredArrow (Comma.fst F G) c) : ((ofCommaFstEquivalenceFunctor F G c).obj X).left = Over.mk X.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (X : CostructuredArrow (Comma.fst F G) c) : ((ofCommaFstEquivalenceFunctor F G c).obj X).hom = X.left.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_map_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : CostructuredArrow (Comma.fst F G) c} (f : X✝ ⟶ Y✝) : ((ofCommaFstEquivalenceFunctor F G c).map f).left = Over.homMk f.left.left ⋯

def CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : Functor (Comma ((Over.forget c).comp F) G) (CostructuredArrow (Comma.fst F G) c)

The inverse functor used to define the equivalence ofCommaFstEquivalence.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Over.forget c).comp F) G) : ((ofCommaFstEquivalenceInverse F G c).obj Y).left.hom = Y.hom

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Over.forget c).comp F) G) : ((ofCommaFstEquivalenceInverse F G c).obj Y).left.right = Y.right

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : Comma ((Over.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((ofCommaFstEquivalenceInverse F G c).map g).left.left = g.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_right {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) {X✝ Y✝ : Comma ((Over.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((ofCommaFstEquivalenceInverse F G c).map g).left.right = g.right

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_left {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Over.forget c).comp F) G) : ((ofCommaFstEquivalenceInverse F G c).obj Y).left.left = Y.left.left

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_right_as {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Over.forget c).comp F) G) : ((ofCommaFstEquivalenceInverse F G c).obj Y).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_hom {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) (Y : Comma ((Over.forget c).comp F) G) : ((ofCommaFstEquivalenceInverse F G c).obj Y).hom = Y.left.hom

def CategoryTheory.CostructuredArrow.ofCommaFstEquivalence {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : CostructuredArrow (Comma.fst F G) c ≌ Comma ((Over.forget c).comp F) G

There is a canonical equivalence between the costructured arrow category with codomain c on the functor Comma.fst F G : Comma F G ⥤ F and the comma category over Over.forget c ⋙ F : Over c ⥤ T and G.

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_inverse {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaFstEquivalence F G c).inverse = ofCommaFstEquivalenceInverse F G c

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_functor {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaFstEquivalence F G c).functor = ofCommaFstEquivalenceFunctor F G c

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_counitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaFstEquivalence F G c).counitIso = NatIso.ofComponents (fun (x : Comma ((Over.forget c).comp F) G) => Iso.refl (((ofCommaFstEquivalenceInverse F G c).comp (ofCommaFstEquivalenceFunctor F G c)).obj x)) ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_unitIso {T : Type u₁} [Category.{v₁, u₁} T] {D : Type u₂} [Category.{v₂, u₂} D] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor C T) (G : Functor D T) (c : C) : (ofCommaFstEquivalence F G c).unitIso = NatIso.ofComponents (fun (x : CostructuredArrow (Comma.fst F G) c) => Iso.refl ((Functor.id (CostructuredArrow (Comma.fst F G) c)).obj x)) ⋯

def CategoryTheory.Over.opEquivOpUnder {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : Over (Opposite.op X) ≌ (Under X)ᵒᵖ

The canonical equivalence between over and under categories by reversing structure arrows.

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_counitIso {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpUnder X).counitIso = Iso.refl ({ obj := fun (Y : (Under X)ᵒᵖ) => mk (Opposite.unop Y).hom.op, map := fun {Z Y : (Under X)ᵒᵖ} (f : Z ⟶ Y) => homMk f.unop.right.op ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (Y : Over (Opposite.op X)) => Opposite.op (Under.mk Y.hom.unop), map := fun {Z Y : Over (Opposite.op X)} (f : Z ⟶ Y) => Opposite.op (Under.homMk f.left.unop ⋯), map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_unitIso {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpUnder X).unitIso = Iso.refl (Functor.id (Over (Opposite.op X)))

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_inverse_map {T : Type u₁} [Category.{v₁, u₁} T] (X : T) {Z Y : (Under X)ᵒᵖ} (f : Z ⟶ Y) : (opEquivOpUnder X).inverse.map f = homMk f.unop.right.op ⋯

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_functor_obj {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (Y : Over (Opposite.op X)) : (opEquivOpUnder X).functor.obj Y = Opposite.op (Under.mk Y.hom.unop)

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_functor_map {T : Type u₁} [Category.{v₁, u₁} T] (X : T) {Z Y : Over (Opposite.op X)} (f : Z ⟶ Y) : (opEquivOpUnder X).functor.map f = Opposite.op (Under.homMk f.left.unop ⋯)

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_inverse_obj {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (Y : (Under X)ᵒᵖ) : (opEquivOpUnder X).inverse.obj Y = mk (Opposite.unop Y).hom.op

def CategoryTheory.Under.opEquivOpOver {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : Under (Opposite.op X) ≌ (Over X)ᵒᵖ

The canonical equivalence between under and over categories by reversing structure arrows.

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_functor_obj {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (Y : Under (Opposite.op X)) : (opEquivOpOver X).functor.obj Y = Opposite.op (Over.mk Y.hom.unop)

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_unitIso {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpOver X).unitIso = Iso.refl (Functor.id (Under (Opposite.op X)))

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_counitIso {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpOver X).counitIso = Iso.refl ({ obj := fun (Y : (Over X)ᵒᵖ) => mk (Opposite.unop Y).hom.op, map := fun {Z Y : (Over X)ᵒᵖ} (f : Z ⟶ Y) => homMk f.unop.left.op ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (Y : Under (Opposite.op X)) => Opposite.op (Over.mk Y.hom.unop), map := fun {Z Y : Under (Opposite.op X)} (f : Z ⟶ Y) => Opposite.op (Over.homMk f.right.unop ⋯), map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_functor_map {T : Type u₁} [Category.{v₁, u₁} T] (X : T) {Z Y : Under (Opposite.op X)} (f : Z ⟶ Y) : (opEquivOpOver X).functor.map f = Opposite.op (Over.homMk f.right.unop ⋯)

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_inverse_map {T : Type u₁} [Category.{v₁, u₁} T] (X : T) {Z Y : (Over X)ᵒᵖ} (f : Z ⟶ Y) : (opEquivOpOver X).inverse.map f = homMk f.unop.left.op ⋯

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_inverse_obj {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (Y : (Over X)ᵒᵖ) : (opEquivOpOver X).inverse.obj Y = mk (Opposite.unop Y).hom.op