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.

Stacks Tag 001G

Equations

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

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

Equations

• CategoryTheory.instCategoryOver X = CategoryTheory.commaCategory

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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.

Equations

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

@[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 aesop_cat) : U ⟶ V

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

Equations

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

@[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 aesop_cat) : (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 aesop_cat) : f ≅ g

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

Equations

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

@[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 aesop_cat) : (isoMk hl hw).inv.left = hl.inv

@[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 aesop_cat) : (isoMk hl hw).hom.left = hl.hom

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

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.

Stacks Tag 001G

Equations

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

@[simp]

theorem CategoryTheory.Over.forget_obj {T : Type u₁} [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.

Equations

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

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

Stacks Tag 001G

Equations

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

@[simp]

theorem CategoryTheory.Over.map_obj_left {T : Type u₁} [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.

Equations

• CategoryTheory.Over.mapIso f = CategoryTheory.Comma.mapRightIso (CategoryTheory.Functor.id T) (CategoryTheory.Discrete.natIso fun (x : CategoryTheory.Discrete PUnit.{1}) => f)

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

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.

Equations

• CategoryTheory.Over.mapId Y = CategoryTheory.eqToIso ⋯

@[simp]

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

@[simp]

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

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.

Equations

• CategoryTheory.Over.mapForget f = CategoryTheory.eqToIso ⋯

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

Equations

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

@[simp]

theorem CategoryTheory.Over.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.Over.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.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.

Equations

• CategoryTheory.Over.mapCongr f g h = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Over X) => CategoryTheory.eqToIso ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.mapCongr_hom_app {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✝ = eqToHom ⋯

@[simp]

theorem CategoryTheory.Over.mapCongr_inv_app {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✝ = eqToHom ⋯

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

The functor defined by the over categories

Equations

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

@[simp]

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

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

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.

Equations

• CategoryTheory.Over.mkIdTerminal = CategoryTheory.CostructuredArrow.mkIdTerminal

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.

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

Equations

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

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

Equations

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

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

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

Equations

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

@[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_functor {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (f : Over X) : f.iteratedSliceEquiv.functor = f.iteratedSliceForward

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

Equations

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

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

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

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.{u_2, 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.{u_2, 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.

Equations

• CategoryTheory.Over.postComp F G = CategoryTheory.NatIso.ofComponents (fun (X_1 : CategoryTheory.Over X) => CategoryTheory.Iso.refl ((CategoryTheory.Over.post (F.comp G)).obj X_1)) ⋯

@[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.{u_2, 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.{u_2, 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 Under.map.

Equations

• CategoryTheory.Over.postMap e = { app := fun (Y : CategoryTheory.Over X) => CategoryTheory.Over.homMk (e.app Y.left) ⋯, naturality := ⋯ }

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

Equations

• CategoryTheory.Over.postCongr e = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Over X) => CategoryTheory.Over.isoMk (e.app A.left) ⋯) ⋯

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

Equations

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

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

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.

Equations

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

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

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

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

Equations

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

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

Equations

• CategoryTheory.instCategoryUnder X = CategoryTheory.commaCategory

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

Equations

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

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

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

Equations

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

@[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 aesop_cat) : U ⟶ V

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

Equations

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

@[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 aesop_cat) : (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 aesop_cat) : f ≅ g

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

Equations

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

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

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.

Equations

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

@[simp]

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

Equations

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

@[simp]

theorem CategoryTheory.Under.forgetCone_pt {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (forgetCone X).pt = 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

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.

Equations

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

@[simp]

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

Equations

• CategoryTheory.Under.mapIso f = CategoryTheory.Comma.mapLeftIso (CategoryTheory.Functor.id T) (CategoryTheory.Discrete.natIso fun (x : CategoryTheory.Discrete PUnit.{1}) => f.symm)

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

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.

Equations

• CategoryTheory.Under.mapId Y = CategoryTheory.eqToIso ⋯

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

Equations

• CategoryTheory.Under.mapForget f = CategoryTheory.eqToIso ⋯

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

Equations

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

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

Equations

• CategoryTheory.Under.mapCongr f g h = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Under Y) => CategoryTheory.eqToIso ⋯) ⋯

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

Equations

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

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

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

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.

Equations

• CategoryTheory.Under.mkIdInitial = CategoryTheory.StructuredArrow.mkIdInitial

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.

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_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.

Equations

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

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

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

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.{u_2, 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.{u_2, 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.

Equations

• CategoryTheory.Under.postComp F G = CategoryTheory.NatIso.ofComponents (fun (X_1 : CategoryTheory.Under X) => CategoryTheory.Iso.refl ((CategoryTheory.Under.post (F.comp G)).obj X_1)) ⋯

@[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.{u_2, 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.{u_2, 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.

Equations

• CategoryTheory.Under.postMap e = { app := fun (Y : CategoryTheory.Under X) => CategoryTheory.Under.homMk (e.app Y.right) ⋯, naturality := ⋯ }

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

Equations

• CategoryTheory.Under.postCongr e = CategoryTheory.NatIso.ofComponents (fun (A : CategoryTheory.Under X) => CategoryTheory.Under.isoMk (e.app A.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

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

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

Equations

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

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

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

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.

Equations

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

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

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

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.

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.

Equations

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

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

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

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.

Equations

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

@[simp]

theorem CategoryTheory.Functor.toOver_comp_forget {T : Type u₁} [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.

Equations

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

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.toUnder_comp_forget {T : Type u₁} [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.

Equations

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

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

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

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.

Equations

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

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

Equations

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

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.

Equations

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

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

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

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.

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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

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

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.

Equations

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

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

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

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.

Equations

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

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

Equations

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

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

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

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.

Equations

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

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

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

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.

Equations

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

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.

Equations

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

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

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

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.

Equations

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

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

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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

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.

Equations

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

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

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

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.

Equations

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

@[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_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_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_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.opToOpUnder {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : Functor (Over (Opposite.op X)) (Under X)ᵒᵖ

The canonical functor by reversing structure arrows.

Equations

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

@[simp]

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

@[simp]

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

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

The canonical functor by reversing structure arrows.

Equations

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

@[simp]

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

@[simp]

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

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

Over.opToOpUnder is an equivalence of categories.

Equations

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

@[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 {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpUnder X).inverse = Under.opToOverOp X

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_counitIso {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpUnder X).counitIso = Iso.refl ((Under.opToOverOp X).comp (opToOpUnder X))

@[simp]

theorem CategoryTheory.Over.opEquivOpUnder_functor {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpUnder X).functor = opToOpUnder X

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

The canonical functor by reversing structure arrows.

Equations

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

@[simp]

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

@[simp]

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

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

The canonical functor by reversing structure arrows.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Over.opToUnderOp_obj {T : Type u₁} [Category.{v₁, u₁} T] (X : T) (Y : (Over X)ᵒᵖ) : (opToUnderOp X).obj Y = Under.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)ᵒᵖ

Under.opToOpOver is an equivalence of categories.

Equations

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

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_inverse {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpOver X).inverse = Over.opToUnderOp X

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_functor {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpOver X).functor = opToOpOver X

@[simp]

theorem CategoryTheory.Under.opEquivOpOver_counitIso {T : Type u₁} [Category.{v₁, u₁} T] (X : T) : (opEquivOpOver X).counitIso = Iso.refl ((Over.opToUnderOp X).comp (opToOpOver X))

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