Mathlib.CategoryTheory.Comma.Over.Basic

CategoryTheory.Over definition

(X : T)

Full source

/-- The over category has as objects arrows in `T` with codomain `X` and as morphisms commutative
triangles. -/
@[stacks 001G]
def Over (X : T) :=
  CostructuredArrow (𝟭 T) X

Over category of $X$ in $T$

Informal description

The over category of an object $X$ in a category $T$ consists of all morphisms in $T$ with codomain $X$. The morphisms in this over category are commutative triangles between such morphisms.

CategoryTheory.instCategoryOver instance

(X : T) : Category (Over X)

Full source

instance (X : T) : Category (Over X) := commaCategory

Category Structure on the Over Category of $X$

Informal description

For any object $X$ in a category $T$, the over category $\mathrm{Over}\,X$ is a category where the objects are morphisms in $T$ with codomain $X$, and the morphisms are commutative triangles between such morphisms.

CategoryTheory.Over.inhabited instance

[Inhabited T] : Inhabited (Over (default : T))

Full source

instance Over.inhabited [Inhabited T] : Inhabited (Over (default : T)) where
  default :=
    { left := default
      right := default
      hom := 𝟙 _ }

Inhabited Over Category of Default Object

Informal description

For any inhabited category $T$, the over category of the default object in $T$ is also inhabited.

CategoryTheory.Over.OverMorphism.ext theorem

{X : T} {U V : Over X} {f g : U ⟶ V} (h : f.left = g.left) : f = g

Full source

@[ext]
theorem OverMorphism.ext {X : T} {U V : Over X} {f g : U ⟶ V} (h : f.left = g.left) : f = g := by
  let ⟨_,b,_⟩ := f
  let ⟨_,e,_⟩ := g
  congr
  simp only [eq_iff_true_of_subsingleton]

Extensionality of Morphisms in Over Category via Left Components

Informal description

For any object $X$ in a category $T$, and any two morphisms $f, g : U \to V$ in the over category of $X$, if the left components of $f$ and $g$ are equal (i.e., $f.\mathrm{left} = g.\mathrm{left}$), then $f = g$.

CategoryTheory.Over.over_right theorem

(U : Over X) : U.right = ⟨⟨⟩⟩

Full source

@[simp]
theorem over_right (U : Over X) : U.right = ⟨⟨⟩⟩ := by simp only

Right Component of Over Category Object is Terminal

Informal description

For any object $U$ in the over category of $X$, the right component of $U$ is equal to the unique object in the terminal category (represented by $\langle \langle \rangle \rangle$).

CategoryTheory.Over.id_left theorem

(U : Over X) : CommaMorphism.left (𝟙 U) = 𝟙 U.left

Full source

@[simp]
theorem id_left (U : Over X) : CommaMorphism.left (𝟙 U) = 𝟙 U.left :=
  rfl

Identity Morphism in Over Category Preserves Left Component

Informal description

For any object $U$ in the over category of $X$, the left component of the identity morphism on $U$ is equal to the identity morphism on the left component of $U$. That is, $(\mathrm{id}_U).\mathrm{left} = \mathrm{id}_{U.\mathrm{left}}$.

CategoryTheory.Over.comp_left theorem

(a b c : Over X) (f : a ⟶ b) (g : b ⟶ c) : (f ≫ g).left = f.left ≫ g.left

Full source

@[simp, reassoc]
theorem comp_left (a b c : Over X) (f : a ⟶ b) (g : b ⟶ c) : (f ≫ g).left = f.left ≫ g.left :=
  rfl

Composition in Over Category Preserves Left Components

Informal description

For any objects $a$, $b$, and $c$ in the over category of $X$, and morphisms $f \colon a \to b$ and $g \colon b \to c$, the left component of the composition $f \circ g$ is equal to the composition of the left components of $f$ and $g$, i.e., $(f \circ g)_{\text{left}} = f_{\text{left}} \circ g_{\text{left}}$.

CategoryTheory.Over.w theorem

{A B : Over X} (f : A ⟶ B) : f.left ≫ B.hom = A.hom

Full source

@[reassoc (attr := simp)]
theorem w {A B : Over X} (f : A ⟶ B) : f.left ≫ B.hom = A.hom := by have := f.w; aesop_cat

Commutativity condition for morphisms in the over category of $X$

Informal description

For any morphism $f \colon A \to B$ in the over category of $X$, the composition of the left component of $f$ with the morphism defining $B$ equals the morphism defining $A$. That is, if $A$ is given by $g_A \colon Y_A \to X$ and $B$ by $g_B \colon Y_B \to X$, then for any morphism $f = (f_{left}, \dots) \colon A \to B$, we have $f_{left} \circ g_B = g_A$.

CategoryTheory.Over.mk definition

{X Y : T} (f : Y ⟶ X) : Over X

Full source

/-- To give an object in the over category, it suffices to give a morphism with codomain `X`. -/
@[simps! left hom]
def mk {X Y : T} (f : Y ⟶ X) : Over X :=
  CostructuredArrow.mk f

Object in the over category of $X$ defined by a morphism $f \colon Y \to X$

Informal description

Given a morphism $f \colon Y \to X$ in a category $T$, the object `Over.mk f` represents an object in the over category of $X$, which consists of all morphisms in $T$ with codomain $X$.

CategoryTheory.Over.coeFromHom definition

{X Y : T} : CoeOut (Y ⟶ X) (Over X)

Full source

/-- 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. -/
def coeFromHom {X Y : T} : CoeOut (Y ⟶ X) (Over X) where coe := mk

Coercion from morphisms to objects in the over category

Informal description

Given a category $T$ and an object $X$ in $T$, the definition `Over.coeFromHom` provides a coercion from morphisms $f \colon Y \to X$ to objects in the over category of $X$. Specifically, for any morphism $f \colon Y \to X$, the coercion interprets $f$ as the object `Over.mk f` in the over category of $X$.

CategoryTheory.Over.coe_hom theorem

{X Y : T} (f : Y ⟶ X) : (f : Over X).hom = f

Full source

@[simp]
theorem coe_hom {X Y : T} (f : Y ⟶ X) : (f : Over X).hom = f :=
  rfl

Underlying Morphism of Over Category Object is Original Morphism

Informal description

For any morphism $f \colon Y \to X$ in a category $T$, the underlying morphism of the object in the over category of $X$ constructed from $f$ is equal to $f$ itself. That is, $(\text{Over.mk}\,f).\text{hom} = f$.

CategoryTheory.Over.homMk_eta theorem

{U V : Over X} (f : U ⟶ V) (h) : homMk f.left h = f

Full source

@[simp]
lemma homMk_eta {U V : Over X} (f : U ⟶ V) (h) :
    homMk f.left h = f := by
  rfl

Equality of Constructed Morphism in Over Category

Informal description

For any morphism $f \colon U \to V$ in the over category of $X$, and for any proof $h$ that the underlying morphism $f.\text{left}$ makes the appropriate triangle commute, the constructed morphism $\text{homMk}\,f.\text{left}\,h$ is equal to $f$.

CategoryTheory.Over.homMk_comp theorem

 {U V W : Over X} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (w_f w_g) :
  homMk (f ≫ g) (by aesop) = homMk f w_f ≫ homMk g w_g

Full source

/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/
lemma homMk_comp {U V W : Over X} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (w_f w_g) :
    homMk (f ≫ g) (by aesop) = homMkhomMk f w_f ≫ homMk g w_g := by
  ext
  simp

Composition of Constructed Morphisms in Over Category

Informal description

For any objects $U, V, W$ in the over category of $X$, and morphisms $f \colon U.\mathrm{left} \to V.\mathrm{left}$ and $g \colon V.\mathrm{left} \to W.\mathrm{left}$ in the base category $T$, the constructed morphism $\mathrm{homMk}(f \circ g)$ is equal to the composition $\mathrm{homMk}(f) \circ \mathrm{homMk}(g)$ in the over category.

CategoryTheory.Over.hom_left_inv_left theorem

{f g : Over X} (e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 f.left

Full source

@[reassoc (attr := simp)]
lemma hom_left_inv_left {f g : Over X} (e : f ≅ g) :
    e.hom.left ≫ e.inv.left = 𝟙 f.left := by
  simp [← Over.comp_left]

Composition of Isomorphism Components in Over Category Yields Identity

Informal description

For any objects $f$ and $g$ in the over category of $X$, and for any isomorphism $e \colon f \cong g$ between them, the composition of the underlying morphisms $e_{\text{hom}}.\text{left}$ and $e_{\text{inv}}.\text{left}$ in the base category $T$ equals the identity morphism on $f.\text{left}$.

CategoryTheory.Over.inv_left_hom_left theorem

{f g : Over X} (e : f ≅ g) : e.inv.left ≫ e.hom.left = 𝟙 g.left

Full source

@[reassoc (attr := simp)]
lemma inv_left_hom_left {f g : Over X} (e : f ≅ g) :
    e.inv.left ≫ e.hom.left = 𝟙 g.left := by
  simp [← Over.comp_left]

Inverse-Hom Composition Yields Identity in Over Category

Informal description

For any objects $f$ and $g$ in the over category of $X$, and any isomorphism $e \colon f \cong g$ between them, the composition of the underlying morphisms $e^{-1} \circ e$ in the base category $T$ is equal to the identity morphism on the domain of $g$.

CategoryTheory.Over.forget definition

: Over X ⥤ T

Full source

/-- The forgetful functor mapping an arrow to its domain. -/
@[stacks 001G]
def forget : OverOver X ⥤ T :=
  Comma.fst _ _

Forgetful functor from the over category of $X$ to $T$

Informal description

The forgetful functor from the over category of $X$ to the original category $T$, which maps each object (a morphism in $T$ with codomain $X$) to its domain in $T$, and each morphism (a commutative triangle) to its left leg in $T$.

CategoryTheory.Over.forget_obj theorem

{U : Over X} : (forget X).obj U = U.left

Full source

@[simp]
theorem forget_obj {U : Over X} : (forget X).obj U = U.left :=
  rfl

Forgetful Functor on Objects in Over Category Equals Domain

Informal description

For any object $U$ in the over category of $X$, the application of the forgetful functor to $U$ yields the domain of the morphism $U$ in the base category $T$, i.e., $\text{forget}(X)(U) = U.\text{left}$.

CategoryTheory.Over.forget_map theorem

{U V : Over X} {f : U ⟶ V} : (forget X).map f = f.left

Full source

@[simp]
theorem forget_map {U V : Over X} {f : U ⟶ V} : (forget X).map f = f.left :=
  rfl

Forgetful Functor Maps Morphisms to Their Left Legs in Over Category

Informal description

For any objects $U$ and $V$ in the over category of $X$ and any morphism $f \colon U \to V$ in this over category, the image of $f$ under the forgetful functor $\text{forget}(X) \colon \text{Over}(X) \to T$ is equal to the left leg $f.\text{left}$ of the commutative triangle representing $f$.

CategoryTheory.Over.forgetCocone definition

(X : T) : Limits.Cocone (forget X)

Full source

/-- The natural cocone over the forgetful functor `Over X ⥤ T` with cocone point `X`. -/
@[simps]
def forgetCocone (X : T) : Limits.Cocone (forget X) :=
  { pt := X
    ι := { app := Comma.hom } }

Natural cocone over the forgetful functor from $\text{Over}(X)$ to $T$ with cocone point $X$

Informal description

For an object $X$ in a category $T$, the natural cocone over the forgetful functor $\text{Over}(X) \to T$ has $X$ as its cocone point. The natural transformation components are given by the morphisms from objects in $\text{Over}(X)$ to $X$ that define the over category structure.

CategoryTheory.Over.map definition

{Y : T} (f : X ⟶ Y) : Over X ⥤ Over Y

Full source

/-- A morphism `f : X ⟶ Y` induces a functor `Over X ⥤ Over Y` in the obvious way. -/
@[stacks 001G]
def map {Y : T} (f : X ⟶ Y) : OverOver X ⥤ Over Y :=
  Comma.mapRight _ <| Discrete.natTrans fun _ => f

Functor induced by a morphism on over categories

Informal description

Given a morphism $f \colon X \to Y$ in a category $T$, the functor $\text{Over}(f) \colon \text{Over}(X) \to \text{Over}(Y)$ maps an object $U$ in $\text{Over}(X)$ (which is a morphism $U.\text{hom} \colon U.\text{left} \to X$) to the object in $\text{Over}(Y)$ given by the composition $U.\text{hom} \circ f \colon U.\text{left} \to Y$.

CategoryTheory.Over.map_obj_left theorem

: ((map f).obj U).left = U.left

Full source

@[simp]
theorem map_obj_left : ((map f).obj U).left = U.left :=
  rfl

Preservation of Left Component by Over Category Functor

Informal description

For any morphism $f \colon X \to Y$ in a category $T$ and any object $U$ in the over category $\mathrm{Over}(X)$, the left component of the object obtained by applying the functor $\mathrm{map}(f)$ to $U$ is equal to the left component of $U$, i.e., $(\mathrm{map}(f)(U)).\mathrm{left} = U.\mathrm{left}$.

CategoryTheory.Over.map_obj_hom theorem

: ((map f).obj U).hom = U.hom ≫ f

Full source

@[simp]
theorem map_obj_hom : ((map f).obj U).hom = U.hom ≫ f :=
  rfl

Homomorphism of Mapped Over Object is Composition with $f$

Informal description

For a morphism $f \colon X \to Y$ in a category $T$ and an object $U$ in the over category $\mathrm{Over}(X)$, the homomorphism of the image of $U$ under the functor $\mathrm{map}(f)$ is given by the composition $U.\mathrm{hom} \circ f \colon U.\mathrm{left} \to Y$.

CategoryTheory.Over.map_map_left theorem

: ((map f).map g).left = g.left

Full source

@[simp]
theorem map_map_left : ((map f).map g).left = g.left :=
  rfl

Preservation of Left Component by Over Category Functor

Informal description

Given a morphism $f \colon X \to Y$ in a category $T$ and a morphism $g$ in the over category $\mathrm{Over}(X)$, the left component of the image of $g$ under the functor $\mathrm{map}(f)$ is equal to the left component of $g$ itself. In other words, if $g \colon U \to V$ is a morphism in $\mathrm{Over}(X)$, then $(\mathrm{map}(f).\mathrm{map}(g)).\mathrm{left} = g.\mathrm{left}$.

CategoryTheory.Over.mapIso definition

{Y : T} (f : X ≅ Y) : Over X ≌ Over Y

Full source

/-- If `f` is an isomorphism, `map f` is an equivalence of categories. -/
def mapIso {Y : T} (f : X ≅ Y) : OverOver X ≌ Over Y :=
  Comma.mapRightIso _ <| Discrete.natIso fun _ ↦ f

Equivalence of over categories induced by an isomorphism

Informal description

Given an isomorphism $f \colon X \to Y$ in a category $T$, the functor $\text{map}(f)$ induces an equivalence of categories between the over categories $\text{Over}(X)$ and $\text{Over}(Y)$.

CategoryTheory.Over.mapIso_functor theorem

{Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom

Full source

@[simp] lemma mapIso_functor {Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom := rfl

Functor Component of Over Category Equivalence Induced by Isomorphism

Informal description

Given an isomorphism $f \colon X \to Y$ in a category $T$, the functor component of the equivalence $\text{mapIso}(f) \colon \text{Over}(X) \simeq \text{Over}(Y)$ is equal to the functor $\text{map}(f.\text{hom}) \colon \text{Over}(X) \to \text{Over}(Y)$ induced by the morphism $f.\text{hom} \colon X \to Y$.

CategoryTheory.Over.mapIso_inverse theorem

{Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv

Full source

@[simp] lemma mapIso_inverse {Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv := rfl

Inverse of Over Category Equivalence Induced by Isomorphism

Informal description

For any isomorphism $f \colon X \to Y$ in a category $T$, the inverse functor of the equivalence $\text{mapIso}(f) \colon \text{Over}(X) \simeq \text{Over}(Y)$ is equal to the functor $\text{map}(f^{-1}) \colon \text{Over}(Y) \to \text{Over}(X)$ induced by the inverse morphism $f^{-1} \colon Y \to X$.

CategoryTheory.Over.mapId_eq theorem

(Y : T) : map (𝟙 Y) = 𝟭 _

Full source

/-- Mapping by the identity morphism is just the identity functor. -/
theorem mapId_eq (Y : T) : map (𝟙 Y) = 𝟭 _ := by
  fapply Functor.ext
  · intro x
    dsimp [Over, Over.map, Comma.mapRight]
    simp only [Category.comp_id]
    exact rfl
  · intros x y u
    dsimp [Over, Over.map, Comma.mapRight]
    simp

Identity Morphism Induces Identity Functor on Over Category

Informal description

For any object $Y$ in a category $T$, the functor $\mathrm{map}(\mathrm{id}_Y)$ induced by the identity morphism on $Y$ is equal to the identity functor on the over category $\mathrm{Over}(Y)$.

CategoryTheory.Over.mapId definition

(Y : T) : map (𝟙 Y) ≅ 𝟭 _

Full source

/-- The natural isomorphism arising from `mapForget_eq`. -/
@[simps!]
def mapId (Y : T) : mapmap (𝟙 Y) ≅ 𝟭 _ := eqToIso (mapId_eq Y)

Natural isomorphism from identity-induced functor to identity functor on over category

Informal description

The natural isomorphism between the functor $\mathrm{map}(\mathrm{id}_Y) : \mathrm{Over}(Y) \to \mathrm{Over}(Y)$ induced by the identity morphism on $Y$ and the identity functor $\mathrm{id}_{\mathrm{Over}(Y)}$ on the over category of $Y$. This isomorphism arises from the equality $\mathrm{map}(\mathrm{id}_Y) = \mathrm{id}_{\mathrm{Over}(Y)}$ via the $\mathrm{eqToIso}$ construction.

CategoryTheory.Over.mapForget_eq theorem

{X Y : T} (f : X ⟶ Y) : (map f) ⋙ (forget Y) = (forget X)

Full source

/-- Mapping by `f` and then forgetting is the same as forgetting. -/
theorem mapForget_eq {X Y : T} (f : X ⟶ Y) :
    (map f) ⋙ (forget Y) = (forget X) := by
  fapply Functor.ext
  · dsimp [Over, Over.map]; intro x; exact rfl
  · intros x y u; simp

Compatibility of Mapping and Forgetful Functors in Over Categories

Informal description

Given a morphism $f \colon X \to Y$ in a category $T$, the composition of the functor $\mathrm{map}\,f \colon \mathrm{Over}\,X \to \mathrm{Over}\,Y$ with the forgetful functor $\mathrm{forget}\,Y \colon \mathrm{Over}\,Y \to T$ is equal to the forgetful functor $\mathrm{forget}\,X \colon \mathrm{Over}\,X \to T$.

CategoryTheory.Over.mapForget definition

{X Y : T} (f : X ⟶ Y) : (map f) ⋙ (forget Y) ≅ (forget X)

Full source

/-- The natural isomorphism arising from `mapForget_eq`. -/
def mapForget {X Y : T} (f : X ⟶ Y) :
    (map f) ⋙ (forget Y)(map f) ⋙ (forget Y) ≅ (forget X) := eqToIso (mapForget_eq f)

Natural isomorphism between composed mapping and forgetful functors in over categories

Informal description

Given a morphism $f \colon X \to Y$ in a category $T$, the natural isomorphism $\mathrm{mapForget}\,f$ relates the composition of the functor $\mathrm{map}\,f \colon \mathrm{Over}\,X \to \mathrm{Over}\,Y$ with the forgetful functor $\mathrm{forget}\,Y \colon \mathrm{Over}\,Y \to T$ to the forgetful functor $\mathrm{forget}\,X \colon \mathrm{Over}\,X \to T$. This isomorphism arises from the equality $\mathrm{mapForget\_eq}\,f$.

CategoryTheory.Over.eqToHom_left theorem

{X : T} {U V : Over X} (e : U = V) : (eqToHom e).left = eqToHom (e ▸ rfl : U.left = V.left)

Full source

@[simp]
theorem eqToHom_left {X : T} {U V : Over X} (e : U = V) :
    (eqToHom e).left = eqToHom (e ▸ rfl : U.left = V.left) := by
  subst e; rfl

Equality-Induced Morphism in Over Category Preserves Left Component

Informal description

Let $X$ be an object in a category $T$, and let $U$ and $V$ be objects in the over category $\mathrm{Over}\,X$. Given an equality $e : U = V$, the left component of the morphism $\mathrm{eqToHom}\,e$ in $\mathrm{Over}\,X$ is equal to $\mathrm{eqToHom}\,(e \triangleright \mathrm{rfl} : U.\mathrm{left} = V.\mathrm{left})$, where $U.\mathrm{left}$ and $V.\mathrm{left}$ are the domain objects of the morphisms $U$ and $V$ in $T$.

CategoryTheory.Over.mapComp_eq theorem

{X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) = (map f) ⋙ (map g)

Full source

/-- Mapping by the composite morphism `f ≫ g` is the same as mapping by `f` then by `g`. -/
theorem mapComp_eq {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    map (f ≫ g) = (map f) ⋙ (map g) := by
  fapply Functor.ext
  · simp [Over.map, Comma.mapRight]
  · intro U V k
    ext
    simp

Functoriality of Over Categories under Composition: $\mathrm{map}(f \circ g) = \mathrm{map}(f) \circ \mathrm{map}(g)$

Informal description

For any objects $X, Y, Z$ in a category $T$ and morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, the functor induced by the composite morphism $f \circ g$ on the over categories is equal to the composition of the functors induced by $f$ and $g$ respectively. That is, $\mathrm{map}(f \circ g) = \mathrm{map}(f) \circ \mathrm{map}(g)$.

CategoryTheory.Over.mapComp definition

{X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) ≅ (map f) ⋙ (map g)

Full source

/-- The natural isomorphism arising from `mapComp_eq`. -/
@[simps!]
def mapComp {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    mapmap (f ≫ g) ≅ (map f) ⋙ (map g) := eqToIso (mapComp_eq f g)

Natural isomorphism between composite and composition of over category functors

Informal description

For any objects $X, Y, Z$ in a category $T$ and morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, there is a natural isomorphism between the functor induced by the composite morphism $f \circ g$ on the over categories and the composition of the functors induced by $f$ and $g$ respectively. That is, $\mathrm{map}(f \circ g) \cong \mathrm{map}(f) \circ \mathrm{map}(g)$.

CategoryTheory.Over.mapCongr definition

{X Y : T} (f g : X ⟶ Y) (h : f = g) : map f ≅ map g

Full source

/-- If `f = g`, then `map f` is naturally isomorphic to `map g`. -/
@[simps!]
def mapCongr {X Y : T} (f g : X ⟶ Y) (h : f = g) :
    mapmap f ≅ map g :=
  NatIso.ofComponents (fun A ↦ eqToIso (by rw [h]))

Natural isomorphism between over category functors induced by equal morphisms

Informal description

Given objects $X$ and $Y$ in a category $T$ and morphisms $f, g \colon X \to Y$ with an equality $h \colon f = g$, there is a natural isomorphism between the functors $\text{map}\,f$ and $\text{map}\,g$ induced by $f$ and $g$ on the over categories of $X$ and $Y$ respectively. This isomorphism is constructed componentwise using the isomorphism $\text{eqToIso}$ applied to the equality $h$.

CategoryTheory.Over.mapFunctor definition

: T ⥤ Cat

Full source

/-- The functor defined by the over categories -/
@[simps] def mapFunctor : T ⥤ Cat where
  obj X := Cat.of (Over X)
  map := map
  map_id := mapId_eq
  map_comp := mapComp_eq

Functor from $T$ to categories of over objects

Informal description

The functor $\mathrm{mapFunctor} \colon T \to \mathrm{Cat}$ assigns to each object $X$ in the category $T$ the over category $\mathrm{Over}\,X$, and to each morphism $f \colon X \to Y$ in $T$ the functor $\mathrm{map}\,f \colon \mathrm{Over}\,X \to \mathrm{Over}\,Y$ that maps an object $U \in \mathrm{Over}\,X$ (a morphism $U.\mathrm{hom} \colon U.\mathrm{left} \to X$) to the object $U.\mathrm{hom} \circ f \colon U.\mathrm{left} \to Y$ in $\mathrm{Over}\,Y$. This functor satisfies $\mathrm{mapFunctor}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{Over}\,X}$ and $\mathrm{mapFunctor}(f \circ g) = \mathrm{mapFunctor}(f) \circ \mathrm{mapFunctor}(g)$ for composable morphisms $f$ and $g$.

CategoryTheory.Over.forget_reflects_iso instance

: (forget X).ReflectsIsomorphisms

Full source

instance forget_reflects_iso : (forget X).ReflectsIsomorphisms where
  reflects {Y Z} f t := by
    let g : Z ⟶ Y := Over.homMk (inv ((forget X).map f))
      ((asIso ((forget X).map f)).inv_comp_eq.2 (Over.w f).symm)
    dsimp [forget] at t
    refine ⟨⟨g, ⟨?_,?_⟩⟩⟩
    repeat (ext; simp [g])

Forgetful Functor from Over Category Reflects Isomorphisms

Informal description

The forgetful functor from the over category of $X$ to the original category $T$ reflects isomorphisms. That is, if a morphism $f$ in the over category is mapped to an isomorphism in $T$ by the forgetful functor, then $f$ itself is an isomorphism in the over category.

CategoryTheory.Over.mkIdTerminal definition

: Limits.IsTerminal (mk (𝟙 X))

Full source

/-- The identity over `X` is terminal. -/
noncomputable def mkIdTerminal : Limits.IsTerminal (mk (𝟙 X)) :=
  CostructuredArrow.mkIdTerminal

Terminality of the identity in the over category of $X$

Informal description

The identity morphism $\mathrm{id}_X \colon X \to X$ in the over category $\mathrm{Over}\,X$ is a terminal object. That is, for any object $f \colon Y \to X$ in $\mathrm{Over}\,X$, there exists a unique morphism from $f$ to $\mathrm{id}_X$ in the over category.

CategoryTheory.Over.forget_faithful instance

: (forget X).Faithful

Full source

instance forget_faithful : (forget X).Faithful where

-- TODO: Show the converse holds if `T` has binary products.

Faithfulness of the Forgetful Functor from the Over Category

Informal description

The forgetful functor from the over category of $X$ to the original category $T$ is faithful. That is, for any two morphisms $f, g$ in the over category, if they are mapped to the same morphism in $T$ by the forgetful functor, then $f = g$.

CategoryTheory.Over.epi_of_epi_left theorem

{f g : Over X} (k : f ⟶ g) [hk : Epi k.left] : Epi k

Full source

/--
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 epi_of_epi_left {f g : Over X} (k : f ⟶ g) [hk : Epi k.left] : Epi k :=
  (forget X).epi_of_epi_map hk

Epimorphism in Over Category Induced by Epimorphism in Base Category

Informal description

Let $f$ and $g$ be objects in the over category of $X$, and let $k : f \to g$ be a morphism between them. If the left component $k.\mathrm{left}$ is an epimorphism in the base category, then $k$ is an epimorphism in the over category.

CategoryTheory.Over.mono_of_mono_left theorem

{f g : Over X} (k : f ⟶ g) [hk : Mono k.left] : Mono k

Full source

/--
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.
-/
theorem mono_of_mono_left {f g : Over X} (k : f ⟶ g) [hk : Mono k.left] : Mono k :=
  (forget X).mono_of_mono_map hk

Monomorphism in Over Category Induced by Monomorphism in Base Category

Informal description

Let $T$ be a category and $X$ an object in $T$. For any morphism $k \colon f \to g$ in the over category $\mathrm{Over}\,X$, if the left component $k.\mathrm{left}$ is a monomorphism in $T$, then $k$ is a monomorphism in $\mathrm{Over}\,X$.

CategoryTheory.Over.mono_left_of_mono instance

{f g : Over X} (k : f ⟶ g) [Mono k] : Mono k.left

Full source

/--
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`.
-/
instance mono_left_of_mono {f g : Over X} (k : f ⟶ g) [Mono k] : Mono k.left := by
  refine ⟨fun {Y : T} l m a => ?_⟩
  let l' : mkmk (m ≫ f.hom) ⟶ f := homMk l (by
        dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc])
  suffices l' = (homMk m : mkmk (m ≫ f.hom) ⟶ f) by apply congrArg CommaMorphism.left this
  rw [← cancel_mono k]
  ext
  apply a

Left Component of a Monomorphism in Over Category is Monomorphism

Informal description

For any morphism $k \colon f \to g$ in the over category of $X$, if $k$ is a monomorphism, then its left component $k.\mathrm{left}$ is also a monomorphism in the base category.

CategoryTheory.Over.iteratedSliceForward definition

: Over f ⥤ Over f.left

Full source

/-- Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y -/
@[simps]
def iteratedSliceForward : OverOver f ⥤ Over f.left where
  obj α := Over.mk α.hom.left
  map κ := Over.homMk κ.left.left (by dsimp; rw [← Over.w κ]; rfl)

Functor from iterated slice category $ (T/X)/f $ to $ T/Y $

Informal description

Given a morphism $ f : Y \to X $ in a category $ T $, the functor $\text{iteratedSliceForward}$ maps an object $ \alpha $ in the over category of $ f $ (i.e., an object $ \alpha $ in $ (T/X)/f $) to the object $ \text{Over.mk}(\alpha.\text{hom}.\text{left}) $ in the over category of $ f.\text{left} $ (i.e., $ T/Y $). For a morphism $ \kappa $ between objects in $ (T/X)/f $, the functor maps $ \kappa $ to the morphism $ \text{Over.homMk}(\kappa.\text{left}.\text{left}) $ in $ T/Y $, where the commutativity condition is satisfied by the equality $ \kappa.\text{left}.\text{left} \circ \alpha.\text{hom}.\text{left} = \beta.\text{hom}.\text{left} $ (for objects $ \alpha, \beta $ in $ (T/X)/f $).

CategoryTheory.Over.iteratedSliceBackward definition

: Over f.left ⥤ Over f

Full source

/-- Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f -/
@[simps]
def iteratedSliceBackward : OverOver f.left ⥤ Over f where
  obj g := mk (homMk g.hom : mk (g.hom ≫ f.hom) ⟶ f)
  map α := homMk (homMk α.left (w_assoc α f.hom)) (OverMorphism.ext (w α))

Backward functor between iterated slice categories over $f$

Informal description

Given a morphism $f \colon Y \to X$ in a category $T$, the functor $\mathrm{iteratedSliceBackward}$ maps from the over category of $f.\mathrm{left}$ (the domain of $f$) to the over category of $f$. For an object $g$ in $\mathrm{Over}\,f.\mathrm{left}$ (i.e., a morphism $g \colon Z \to Y$), it constructs an object in $\mathrm{Over}\,f$ by composing with $f$ to get $g \circ f \colon Z \to X$ and using this as the underlying morphism. For a morphism $\alpha$ between objects in $\mathrm{Over}\,f.\mathrm{left}$, it constructs the corresponding morphism in $\mathrm{Over}\,f$ by lifting $\alpha$ through the composition with $f$.

CategoryTheory.Over.iteratedSliceEquiv definition

: Over f ≌ Over f.left

Full source

/-- Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y -/
@[simps]
def iteratedSliceEquiv : OverOver f ≌ Over f.left where
  functor := iteratedSliceForward f
  inverse := iteratedSliceBackward f
  unitIso := NatIso.ofComponents (fun g => Over.isoMk (Over.isoMk (Iso.refl _)))
  counitIso := NatIso.ofComponents (fun g => Over.isoMk (Iso.refl _))

Equivalence between $(T/X)/f$ and $T/Y$

Informal description

Given a morphism $f \colon Y \to X$ in a category $T$, there is an equivalence of categories between the over category of $f$ (i.e., the slice category $(T/X)/f$) and the over category of $Y$ (i.e., $T/Y$). The equivalence is constructed via two functors: - The forward functor maps an object $\alpha$ in $(T/X)/f$ to the object $\mathrm{mk}(\alpha.\mathrm{hom}.\mathrm{left})$ in $T/Y$. - The backward functor maps an object $g \colon Z \to Y$ in $T/Y$ to the object $\mathrm{mk}(g \circ f)$ in $(T/X)/f$. The unit and counit isomorphisms are given by identity isomorphisms at each object, ensuring that the functors form an adjoint equivalence.

CategoryTheory.Over.iteratedSliceForward_forget theorem

: iteratedSliceForward f ⋙ forget f.left = forget f ⋙ forget X

Full source

theorem iteratedSliceForward_forget :
    iteratedSliceForwarditeratedSliceForward f ⋙ forget f.left = forgetforget f ⋙ forget X :=
  rfl

Compatibility of Forgetful Functors in Iterated Slice Categories

Informal description

For a morphism $f \colon Y \to X$ in a category $T$, the composition of the functor $\mathrm{iteratedSliceForward}\,f$ from the over category of $f$ to the over category of $Y$ with the forgetful functor from the over category of $Y$ to $T$ is equal to the composition of the forgetful functor from the over category of $f$ with the forgetful functor from the over category of $X$ to $T$.

CategoryTheory.Over.iteratedSliceBackward_forget_forget theorem

: iteratedSliceBackward f ⋙ forget f ⋙ forget X = forget f.left

Full source

theorem iteratedSliceBackward_forget_forget :
    iteratedSliceBackwarditeratedSliceBackward f ⋙ forget f ⋙ forget X = forget f.left :=
  rfl

Commutativity of Forgetful Functors in Iterated Slice Categories

Informal description

Given a morphism $f \colon Y \to X$ in a category $T$, the composition of the functors $\mathrm{iteratedSliceBackward}\,f$, the forgetful functor from $\mathrm{Over}\,f$ to $T$, and the forgetful functor from $\mathrm{Over}\,X$ to $T$ is equal to the forgetful functor from $\mathrm{Over}\,f.\mathrm{left}$ to $T$. In other words, the following diagram of functors commutes: \[ \mathrm{Over}\,f.\mathrm{left} \xrightarrow{\mathrm{iteratedSliceBackward}\,f} \mathrm{Over}\,f \xrightarrow{\mathrm{forget}\,f} \mathrm{Over}\,X \xrightarrow{\mathrm{forget}\,X} T \] equals the forgetful functor $\mathrm{forget}\,f.\mathrm{left} \colon \mathrm{Over}\,f.\mathrm{left} \to T$.

CategoryTheory.Over.post definition

(F : T ⥤ D) : Over X ⥤ Over (F.obj X)

Full source

/-- A functor `F : T ⥤ D` induces a functor `Over X ⥤ Over (F.obj X)` in the obvious way. -/
@[simps]
def post (F : T ⥤ D) : OverOver X ⥤ Over (F.obj X) where
  obj Y := mk <| F.map Y.hom
  map f := Over.homMk (F.map f.left)
    (by simp only [Functor.id_obj, mk_left, Functor.const_obj_obj, mk_hom, ← F.map_comp, w])

Pushforward functor between over categories induced by $F$

Informal description

Given a functor $F \colon T \to D$ and an object $X$ in $T$, the functor $\mathrm{post}\,F$ maps objects and morphisms in the over category $\mathrm{Over}\,X$ to those in $\mathrm{Over}\,(F(X))$ as follows: - For an object $Y$ in $\mathrm{Over}\,X$ (represented by a morphism $Y \to X$), the image is the object in $\mathrm{Over}\,(F(X))$ represented by $F(Y) \to F(X)$ (the image of $Y \to X$ under $F$) - For a morphism $f$ in $\mathrm{Over}\,X$ (a commutative triangle), the image is the morphism in $\mathrm{Over}\,(F(X))$ obtained by applying $F$ to the components of the triangle

CategoryTheory.Over.post_comp theorem

{E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) : post (X := X) (F ⋙ G) = post (X := X) F ⋙ post G

Full source

lemma post_comp {E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) :
    post (X := X) (F ⋙ G) = postpost (X := X) F ⋙ post G :=
  rfl

Composition of Pushforward Functors on Over Categories

Informal description

Let $T$, $D$, and $E$ be categories, with $X$ an object in $T$. For any functors $F \colon T \to D$ and $G \colon D \to E$, the pushforward functor $\mathrm{post}(F \circ G)$ on the over category $\mathrm{Over}\,X$ is equal to the composition of pushforward functors $\mathrm{post}\,F \circ \mathrm{post}\,G$.

CategoryTheory.Over.postComp definition

{E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) : post (X := X) (F ⋙ G) ≅ post F ⋙ post G

Full source

/-- `post (F ⋙ G)` is isomorphic (actually equal) to `post F ⋙ post G`. -/
@[simps!]
def postComp {E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) :
    postpost (X := X) (F ⋙ G) ≅ post F ⋙ post G :=
  NatIso.ofComponents (fun X ↦ Iso.refl _)

Natural isomorphism between post-composed pushforward functors on over categories

Informal description

For any categories $T$, $D$, and $E$, and functors $F \colon T \to D$ and $G \colon D \to E$, the functor $\mathrm{post}\,(F \circ G)$ (applied to the over category of $X$ in $T$) is naturally isomorphic to the composition $\mathrm{post}\,F \circ \mathrm{post}\,G$. This isomorphism is given componentwise by the identity isomorphism on each object in the over category.

CategoryTheory.Over.postMap definition

{F G : T ⥤ D} (e : F ⟶ G) : post F ⋙ map (e.app X) ⟶ post G

Full source

/-- A natural transformation `F ⟶ G` induces a natural transformation on
`Over X` up to `Over.map`. -/
@[simps]
def postMap {F G : T ⥤ D} (e : F ⟶ G) : postpost F ⋙ map (e.app X)post F ⋙ map (e.app X) ⟶ post G where
  app Y := Over.homMk (e.app Y.left)

Natural transformation induced on over categories by a natural transformation of functors

Informal description

Given a natural transformation $e \colon F \to G$ between functors $F, G \colon T \to D$, the induced natural transformation $\text{postMap}(e) \colon \text{post}(F) \circ \text{map}(e_X) \to \text{post}(G)$ on the over categories is defined at each object $Y$ in $\text{Over}(X)$ by the morphism $e_{Y.\text{left}} \colon F(Y.\text{left}) \to G(Y.\text{left})$.

CategoryTheory.Over.postCongr definition

{F G : T ⥤ D} (e : F ≅ G) : post F ⋙ map (e.hom.app X) ≅ post G

Full source

/-- If `F` and `G` are naturally isomorphic, then `Over.post F` and `Over.post G` are also naturally
isomorphic up to `Over.map` -/
@[simps!]
def postCongr {F G : T ⥤ D} (e : F ≅ G) : postpost F ⋙ map (e.hom.app X)post F ⋙ map (e.hom.app X) ≅ post G :=
  NatIso.ofComponents (fun A ↦ Over.isoMk (e.app A.left))

Natural isomorphism between pushforward functors induced by a natural isomorphism of functors

Informal description

Given a natural isomorphism $e \colon F \cong G$ between functors $F, G \colon T \to D$, the composition of the pushforward functor $\mathrm{post}\,F$ with the over category functor $\mathrm{map}\,(e.hom.app\,X)$ is naturally isomorphic to the pushforward functor $\mathrm{post}\,G$. More precisely, for each object $A$ in the over category $\mathrm{Over}\,X$, the component of this natural isomorphism at $A$ is given by the isomorphism $\mathrm{Over.isoMk}\,(e.app\,A.left)$, which constructs an isomorphism in the over category from the component $e.app\,A.left$ of the natural isomorphism $e$.

CategoryTheory.Over.instFaithfulObjPost instance

[F.Faithful] : (Over.post (X := X) F).Faithful

Full source

instance [F.Faithful] : (Over.post (X := X) F).Faithful where
  map_injective {A B} f g h := by
    ext
    exact F.map_injective (congrArg CommaMorphism.left h)

Faithfulness of Pushforward Functor on Over Categories for Faithful Functors

Informal description

Given a faithful functor $F \colon T \to D$ and an object $X$ in $T$, the pushforward functor $\mathrm{post}\,F \colon \mathrm{Over}\,X \to \mathrm{Over}\,(F(X))$ is also faithful.

CategoryTheory.Over.instFullObjPostOfFaithful instance

[F.Faithful] [F.Full] : (Over.post (X := X) F).Full

Full source

instance [F.Faithful] [F.Full] : (Over.post (X := X) F).Full where
  map_surjective {A B} f := by
    obtain ⟨a, ha⟩ := F.map_surjective f.left
    have w : a ≫ B.hom = A.hom := F.map_injective <| by simpa [ha] using Over.w _
    exact ⟨Over.homMk a, by ext; simpa⟩

Fullness of Pushforward Functor on Over Categories for Faithful and Full Functors

Informal description

For any faithful and full functor $F \colon T \to D$ and any object $X$ in $T$, the pushforward functor $\mathrm{post}\,F \colon \mathrm{Over}\,X \to \mathrm{Over}\,(F(X))$ is full.

CategoryTheory.Over.instEssSurjObjPostOfFull instance

[F.Full] [F.EssSurj] : (Over.post (X := X) F).EssSurj

Full source

instance [F.Full] [F.EssSurj] : (Over.post (X := X) F).EssSurj where
  mem_essImage B := by
    obtain ⟨A', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.left
    obtain ⟨f, hf⟩ := F.map_surjective (e.hom ≫ B.hom)
    exact ⟨Over.mk f, ⟨Over.isoMk e⟩⟩

Essential Surjectivity of Pushforward Functor on Over Categories for Full and Essentially Surjective Functors

Informal description

Given a functor $F \colon T \to D$ that is full and essentially surjective, the pushforward functor $\mathrm{post}\,F \colon \mathrm{Over}\,X \to \mathrm{Over}\,(F(X))$ is also essentially surjective.

CategoryTheory.Over.instIsEquivalenceObjPost instance

[F.IsEquivalence] : (Over.post (X := X) F).IsEquivalence

Full source

instance [F.IsEquivalence] : (Over.post (X := X) F).IsEquivalence where

Equivalence of Over Categories Induced by Equivalence of Base Categories

Informal description

For any equivalence of categories $F \colon T \to D$ and any object $X$ in $T$, the pushforward functor $\mathrm{post}\,F \colon \mathrm{Over}\,X \to \mathrm{Over}\,(F(X))$ between over categories is also an equivalence of categories.

CategoryTheory.Functor.FullyFaithful.over definition

(h : F.FullyFaithful) : (post (X := X) F).FullyFaithful

Full source

/-- If `F` is fully faithful, then so is `Over.post F`. -/
def _root_.CategoryTheory.Functor.FullyFaithful.over (h : F.FullyFaithful) :
    (post (X := X) F).FullyFaithful where
  preimage {A B} f := Over.homMk (h.preimage f.left) <| h.map_injective (by simpa using Over.w f)

Fully faithfulness of pushforward functor between over categories

Informal description

Given a fully faithful functor $F \colon T \to D$ and an object $X$ in $T$, the pushforward functor $\mathrm{post}\,F \colon \mathrm{Over}\,X \to \mathrm{Over}\,(F(X))$ between over categories is also fully faithful. This means that for any two objects $A, B$ in $\mathrm{Over}\,X$ and any morphism $f \colon F(A) \to F(B)$ in $\mathrm{Over}\,(F(X))$, there exists a unique morphism $g \colon A \to B$ in $\mathrm{Over}\,X$ such that $F(g) = f$.

CategoryTheory.Over.postAdjunctionRight definition

{Y : D} {F : T ⥤ D} {G : D ⥤ T} (a : F ⊣ G) : post F ⋙ map (a.counit.app Y) ⊣ post G

Full source

/-- 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)`. -/
@[simps]
def postAdjunctionRight {Y : D} {F : T ⥤ D} {G : D ⥤ T} (a : F ⊣ G) :
    postpost F ⋙ map (a.counit.app Y)post F ⋙ map (a.counit.app Y) ⊣ post G where
  unit.app A := homMk <| a.unit.app A.left
  counit.app A := homMk <| a.counit.app A.left

Adjunction between post functors in over categories

Informal description

Given an adjunction $F \dashv G$ between functors $F \colon T \to D$ and $G \colon D \to T$, with counit $\epsilon \colon F \circ G \Rightarrow \text{id}_D$, the functor $\text{post}\,F \colon \text{Over}\,X \to \text{Over}\,(F(X))$ followed by the functor induced by $\epsilon_Y \colon F(G(Y)) \to Y$ is left adjoint to the functor $\text{post}\,G \colon \text{Over}\,Y \to \text{Over}\,(G(Y))$.

CategoryTheory.Over.isRightAdjoint_post instance

{Y : D} {G : D ⥤ T} [G.IsRightAdjoint] : (post (X := Y) G).IsRightAdjoint

Full source

instance isRightAdjoint_post {Y : D} {G : D ⥤ T} [G.IsRightAdjoint] :
    (post (X := Y) G).IsRightAdjoint :=
  let ⟨F, ⟨a⟩⟩ := ‹G.IsRightAdjoint›; ⟨_, ⟨postAdjunctionRight a⟩⟩

Left Adjoint Preservation by Pushforward Functor in Over Categories

Informal description

For any functor $G \colon D \to T$ that has a left adjoint, the pushforward functor $\mathrm{post}\,G \colon \mathrm{Over}\,Y \to \mathrm{Over}\,(G(Y))$ between over categories also has a left adjoint.

CategoryTheory.Over.postEquiv definition

(F : T ≌ D) : Over X ≌ Over (F.functor.obj X)

Full source

/-- An equivalence of categories induces an equivalence on over categories. -/
@[simps]
def postEquiv (F : T ≌ D) : OverOver X ≌ Over (F.functor.obj X) where
  functor := Over.post F.functor
  inverse := Over.post (X := F.functor.obj X) F.inverse ⋙ Over.map (F.unitIso.inv.app X)
  unitIso := NatIso.ofComponents (fun A ↦ Over.isoMk (F.unitIso.app A.left))
  counitIso := NatIso.ofComponents (fun A ↦ Over.isoMk (F.counitIso.app A.left))

Equivalence of over categories induced by an equivalence of categories

Informal description

Given an equivalence of categories $F \colon T \simeq D$, the functor $\mathrm{post}\,F$ induces an equivalence between the over category $\mathrm{Over}\,X$ in $T$ and the over category $\mathrm{Over}\,(F(X))$ in $D$. The equivalence is constructed as follows: - The forward functor maps an object $Y \to X$ in $\mathrm{Over}\,X$ to $F(Y) \to F(X)$ in $\mathrm{Over}\,(F(X))$. - The inverse functor is given by first applying $\mathrm{post}\,F^{-1}$ (where $F^{-1}$ is the inverse functor of the equivalence) and then composing with the inverse of the unit isomorphism at $X$. - The unit and counit natural isomorphisms are induced by the unit and counit isomorphisms of the original equivalence $F$, applied to the left components of the objects in the over categories.

CategoryTheory.Over.equivalenceOfIsTerminal definition

(hX : IsTerminal X) : Over X ≌ T

Full source

/-- If `X : T` is terminal, then the over category of `X` is equivalent to `T`. -/
@[simps]
def equivalenceOfIsTerminal (hX : IsTerminal X) : OverOver X ≌ T where
  functor := forget X
  inverse := { obj Y := mk (hX.from Y), map f := homMk f }
  unitIso := NatIso.ofComponents fun Y ↦ isoMk (.refl _) (hX.hom_ext _ _)
  counitIso := NatIso.ofComponents fun _ ↦ .refl _

Equivalence between over category of a terminal object and the original category

Informal description

If $X$ is a terminal object in a category $T$, then the over category $\mathrm{Over}\,X$ is equivalent to $T$ itself. The equivalence is given by: - The forgetful functor $\mathrm{forget}\,X \colon \mathrm{Over}\,X \to T$ which maps each object (a morphism $Y \to X$) to its domain $Y$. - The inverse functor which maps each object $Y$ in $T$ to the object $\mathrm{mk}\,(h_X.\mathrm{from}\,Y)$ in $\mathrm{Over}\,X$, where $h_X.\mathrm{from}\,Y$ is the unique morphism from $Y$ to $X$. - The unit and counit natural isomorphisms are given by identity morphisms and the universal property of terminal objects.

CategoryTheory.CostructuredArrow.toOver definition

(F : D ⥤ T) (X : T) : CostructuredArrow F X ⥤ Over X

Full source

/-- Reinterpreting an `F`-costructured arrow `F.obj d ⟶ X` as an arrow over `X` induces a functor
    `CostructuredArrow F X ⥤ Over X`. -/
@[simps!]
def toOver (F : D ⥤ T) (X : T) : CostructuredArrowCostructuredArrow F X ⥤ Over X :=
  CostructuredArrow.pre F (𝟭 T) X

Functor from costructured arrows to the over category

Informal description

Given a functor $F \colon D \to T$ and an object $X$ in $T$, the functor $\mathrm{toOver}\,F\,X$ maps each $F$-costructured arrow (i.e., a morphism $F(d) \to X$ for some $d \in D$) to the corresponding arrow in the over category $\mathrm{Over}\,X$. This functor is constructed by precomposing with $F$ and the identity functor on $T$.

CategoryTheory.CostructuredArrow.instFaithfulOverToOver instance

(F : D ⥤ T) (X : T) [F.Faithful] : (toOver F X).Faithful

Full source

instance (F : D ⥤ T) (X : T) [F.Faithful] : (toOver F X).Faithful :=
  show (CostructuredArrow.pre _ _ _).Faithful from inferInstance

Faithfulness of the Functor from Costructured Arrows to the Over Category

Informal description

For any faithful functor $F \colon D \to T$ and object $X$ in $T$, the functor $\mathrm{toOver}\,F\,X$ from costructured arrows to the over category is faithful.

CategoryTheory.CostructuredArrow.instFullOverToOver instance

(F : D ⥤ T) (X : T) [F.Full] : (toOver F X).Full

Full source

instance (F : D ⥤ T) (X : T) [F.Full] : (toOver F X).Full :=
  show (CostructuredArrow.pre _ _ _).Full from inferInstance

Fullness of the Functor from Costructured Arrows to the Over Category

Informal description

For any functor $F \colon D \to T$ that is full and any object $X$ in $T$, the functor $\mathrm{toOver}\,F\,X$ from the category of $F$-costructured arrows to the over category $\mathrm{Over}\,X$ is full.

CategoryTheory.CostructuredArrow.instEssSurjOverToOver instance

(F : D ⥤ T) (X : T) [F.EssSurj] : (toOver F X).EssSurj

Full source

instance (F : D ⥤ T) (X : T) [F.EssSurj] : (toOver F X).EssSurj :=
  show (CostructuredArrow.pre _ _ _).EssSurj from inferInstance

Essential Surjectivity of the Functor from Costructured Arrows to the Over Category

Informal description

For any essentially surjective functor $F \colon D \to T$ and any object $X$ in $T$, the induced functor $\mathrm{toOver}\,F\,X \colon \mathrm{CostructuredArrow}\,F\,X \to \mathrm{Over}\,X$ is essentially surjective. This means that every object in the over category $\mathrm{Over}\,X$ is isomorphic to an object coming from the category of $F$-costructured arrows via $\mathrm{toOver}\,F\,X$.

CategoryTheory.CostructuredArrow.isEquivalence_toOver instance

(F : D ⥤ T) (X : T) [F.IsEquivalence] : (toOver F X).IsEquivalence

Full source

/-- An equivalence `F` induces an equivalence `CostructuredArrow F X ≌ Over X`. -/
instance isEquivalence_toOver (F : D ⥤ T) (X : T) [F.IsEquivalence] :
    (toOver F X).IsEquivalence :=
  CostructuredArrow.isEquivalence_pre _ _ _

Equivalence of Costructured Arrows and Over Categories

Informal description

For any functor $F \colon D \to T$ that is an equivalence of categories and any object $X$ in $T$, the functor $\mathrm{toOver}\,F\,X$ from the category of $F$-costructured arrows to the over category $\mathrm{Over}\,X$ is also an equivalence of categories.

CategoryTheory.Under definition

(X : T)

Full source

/-- The under category has as objects arrows with domain `X` and as morphisms commutative
    triangles. -/
def Under (X : T) :=
  StructuredArrow X (𝟭 T)

Under category of an object

Informal description

The under category of an object $X$ in a category $T$ has as objects all morphisms with domain $X$ and as morphisms commutative triangles between these morphisms.

CategoryTheory.instCategoryUnder instance

(X : T) : Category (Under X)

Full source

instance (X : T) : Category (Under X) := commaCategory

Category Structure on the Under Category of an Object

Informal description

For any object $X$ in a category $T$, the under category $\mathrm{Under}\,X$ forms a category where: - Objects are morphisms in $T$ with domain $X$ - Morphisms are commutative triangles between these morphisms

CategoryTheory.Under.inhabited instance

[Inhabited T] : Inhabited (Under (default : T))

Full source

instance Under.inhabited [Inhabited T] : Inhabited (Under (default : T)) where
  default :=
    { left := default
      right := default
      hom := 𝟙 _ }

Inhabited Under Category of Default Object

Informal description

For any inhabited category $T$, the under category of the default object in $T$ is also inhabited.

CategoryTheory.Under.UnderMorphism.ext theorem

{X : T} {U V : Under X} {f g : U ⟶ V} (h : f.right = g.right) : f = g

Full source

@[ext]
theorem UnderMorphism.ext {X : T} {U V : Under X} {f g : U ⟶ V} (h : f.right = g.right) :
    f = g := by
  let ⟨_,b,_⟩ := f; let ⟨_,e,_⟩ := g
  congr; simp only [eq_iff_true_of_subsingleton]

Morphism Extensionality in Under Categories via Right Components

Informal description

For any object $X$ in a category $T$, and any two objects $U, V$ in the under category of $X$, if two morphisms $f, g : U \to V$ in the under category have equal right components ($f.\mathrm{right} = g.\mathrm{right}$), then $f = g$.

CategoryTheory.Under.under_left theorem

(U : Under X) : U.left = ⟨⟨⟩⟩

Full source

@[simp]
theorem under_left (U : Under X) : U.left = ⟨⟨⟩⟩ := by simp only

Left Component of Under Category Object is Singleton

Informal description

For any object $U$ in the under category of an object $X$ in a category $T$, the left component of $U$ is equal to the unique object of the singleton category $\mathrm{PUnit}$ (denoted by $\langle \langle \rangle \rangle$).

CategoryTheory.Under.id_right theorem

(U : Under X) : CommaMorphism.right (𝟙 U) = 𝟙 U.right

Full source

@[simp]
theorem id_right (U : Under X) : CommaMorphism.right (𝟙 U) = 𝟙 U.right :=
  rfl

Right Component of Identity Morphism in Under Category

Informal description

For any object $U$ in the under category of an object $X$ in a category $T$, the right component of the identity morphism on $U$ is equal to the identity morphism on the right component of $U$. That is, if $\mathrm{id}_U$ is the identity morphism on $U$, then $\mathrm{id}_U.\mathrm{right} = \mathrm{id}_{U.\mathrm{right}}$.

CategoryTheory.Under.comp_right theorem

(a b c : Under X) (f : a ⟶ b) (g : b ⟶ c) : (f ≫ g).right = f.right ≫ g.right

Full source

@[simp]
theorem comp_right (a b c : Under X) (f : a ⟶ b) (g : b ⟶ c) : (f ≫ g).right = f.right ≫ g.right :=
  rfl

Composition in Under Category Preserves Right Components

Informal description

For any three objects $a$, $b$, and $c$ in the under category of an object $X$ in a category $T$, and for any morphisms $f \colon a \to b$ and $g \colon b \to c$, the right component of the composition $f \circ g$ is equal to the composition of the right components of $f$ and $g$, i.e., $(f \circ g).\text{right} = f.\text{right} \circ g.\text{right}$.

CategoryTheory.Under.w theorem

{A B : Under X} (f : A ⟶ B) : A.hom ≫ f.right = B.hom

Full source

@[reassoc (attr := simp)]
theorem w {A B : Under X} (f : A ⟶ B) : A.hom ≫ f.right = B.hom := by have := f.w; aesop_cat

Commutativity condition for morphisms in the under category

Informal description

For any morphism $f \colon A \to B$ in the under category of an object $X$ in a category $T$, the diagram \[ \begin{array}{ccc} X & \xrightarrow{A.\text{hom}} & A.\text{right} \\ & \searrow & \downarrow f.\text{right} \\ & & B.\text{right} \end{array} \] commutes, i.e., $A.\text{hom} \circ f.\text{right} = B.\text{hom}$.

CategoryTheory.Under.mk definition

{X Y : T} (f : X ⟶ Y) : Under X

Full source

/-- To give an object in the under category, it suffices to give an arrow with domain `X`. -/
@[simps! right hom]
def mk {X Y : T} (f : X ⟶ Y) : Under X :=
  StructuredArrow.mk f

Object in the under category induced by a morphism

Informal description

Given a morphism $f \colon X \to Y$ in a category $T$, the object `Under.mk f` represents the object in the under category of $X$ corresponding to the morphism $f$.

CategoryTheory.Under.homMk_eta theorem

{U V : Under X} (f : U ⟶ V) (h) : homMk f.right h = f

Full source

@[simp]
lemma homMk_eta {U V : Under X} (f : U ⟶ V) (h) :
    homMk f.right h = f := by
  rfl

Eta Rule for Morphism Construction in Under Category

Informal description

For any morphism $f \colon U \to V$ in the under category of an object $X$ in a category $T$, and for any proof $h$ that $U.\text{hom} \circ f.\text{right} = V.\text{hom}$, the constructed morphism $\text{homMk}\,f.\text{right}\,h$ is equal to $f$.

CategoryTheory.Under.homMk_comp theorem

 {U V W : Under X} (f : U.right ⟶ V.right) (g : V.right ⟶ W.right) (w_f w_g) :
  homMk (f ≫ g) (by simp only [reassoc_of% w_f, w_g]) = homMk f w_f ≫ homMk g w_g

Full source

/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/
lemma homMk_comp {U V W : Under X} (f : U.right ⟶ V.right) (g : V.right ⟶ W.right) (w_f w_g) :
    homMk (f ≫ g) (by simp only [reassoc_of% w_f, w_g])  = homMkhomMk f w_f ≫ homMk g w_g := by
  ext
  simp

Composition of Constructed Morphisms in Under Category via Right Components

Informal description

For any objects $U, V, W$ in the under category of an object $X$ in a category $T$, and morphisms $f \colon U_{\text{right}} \to V_{\text{right}}$ and $g \colon V_{\text{right}} \to W_{\text{right}}$ in $T$ with commuting conditions $w_f$ and $w_g$ respectively, the constructed morphism $\text{homMk}(f \circ g)$ is equal to the composition of the constructed morphisms $\text{homMk}(f) \circ \text{homMk}(g)$.

CategoryTheory.Under.isoMk_hom_right theorem

{f g : Under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) : (isoMk hr hw).hom.right = hr.hom

Full source

@[simp]
theorem isoMk_hom_right {f g : Under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) :
    (isoMk hr hw).hom.right = hr.hom :=
  rfl

Right Component of Constructed Isomorphism in Under Category

Informal description

Given two objects $f$ and $g$ in the under category of $X$, and an isomorphism $hr : f_{\text{right}} \cong g_{\text{right}}$ between their right objects such that $f_{\text{hom}} \circ hr_{\text{hom}} = g_{\text{hom}}$, the right component of the isomorphism $\text{isoMk}(hr, hw)$ is equal to $hr_{\text{hom}}$.

CategoryTheory.Under.isoMk_inv_right theorem

{f g : Under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) : (isoMk hr hw).inv.right = hr.inv

Full source

@[simp]
theorem isoMk_inv_right {f g : Under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) :
    (isoMk hr hw).inv.right = hr.inv :=
  rfl

Right Component of Inverse in Under Category Isomorphism Construction

Informal description

Given two objects $f$ and $g$ in the under category of $X$, an isomorphism $hr : f_{\text{right}} \cong g_{\text{right}}$ between their right objects, and a commuting condition $f_{\text{hom}} \circ hr_{\text{hom}} = g_{\text{hom}}$, the right component of the inverse of the constructed isomorphism $\text{isoMk}\,hr\,hw$ equals the inverse of $hr$. That is, $(\text{isoMk}\,hr\,hw)^{-1}_{\text{right}} = hr^{-1}$.

CategoryTheory.Under.hom_right_inv_right theorem

{f g : Under X} (e : f ≅ g) : e.hom.right ≫ e.inv.right = 𝟙 f.right

Full source

@[reassoc (attr := simp)]
lemma hom_right_inv_right {f g : Under X} (e : f ≅ g) :
    e.hom.right ≫ e.inv.right = 𝟙 f.right := by
  simp [← Under.comp_right]

Right Component of Isomorphism in Under Category Composes with Its Inverse to Identity

Informal description

For any objects $f$ and $g$ in the under category of $X$, and any isomorphism $e : f \cong g$, the composition of the right component of $e$'s homomorphism with the right component of $e$'s inverse is equal to the identity morphism on $f$'s right object. That is, $e_{\text{hom},\text{right}} \circ e_{\text{inv},\text{right}} = \text{id}_{f_{\text{right}}}$.

CategoryTheory.Under.inv_right_hom_right theorem

{f g : Under X} (e : f ≅ g) : e.inv.right ≫ e.hom.right = 𝟙 g.right

Full source

@[reassoc (attr := simp)]
lemma inv_right_hom_right {f g : Under X} (e : f ≅ g) :
    e.inv.right ≫ e.hom.right = 𝟙 g.right := by
  simp [← Under.comp_right]

Inverse-Hom Composition in Under Category Yields Identity

Informal description

For any objects $f$ and $g$ in the under category of an object $X$, and for any isomorphism $e \colon f \cong g$, the composition of the right component of the inverse morphism $e^{-1}$ with the right component of $e$ equals the identity morphism on $g_{\text{right}}$, i.e., $e^{-1}_{\text{right}} \circ e_{\text{right}} = \text{id}_{g_{\text{right}}}$.

CategoryTheory.Under.forget definition

: Under X ⥤ T

Full source

/-- The forgetful functor mapping an arrow to its domain. -/
def forget : UnderUnder X ⥤ T :=
  Comma.snd _ _

Forgetful functor from under category to base category

Informal description

The forgetful functor from the under category of an object $X$ in a category $T$ to $T$ itself, which maps each object (a morphism with domain $X$) to its codomain in $T$, and each morphism (a commutative triangle) to the corresponding morphism between codomains in $T$.

CategoryTheory.Under.forget_obj theorem

{U : Under X} : (forget X).obj U = U.right

Full source

@[simp]
theorem forget_obj {U : Under X} : (forget X).obj U = U.right :=
  rfl

Forgetful Functor on Under Category Preserves Codomains

Informal description

For any object $U$ in the under category of $X$, the application of the forgetful functor to $U$ yields the codomain of the morphism defining $U$, i.e., $\text{forget}(X)(U) = U_{\text{right}}$.

CategoryTheory.Under.forget_map theorem

{U V : Under X} {f : U ⟶ V} : (forget X).map f = f.right

Full source

@[simp]
theorem forget_map {U V : Under X} {f : U ⟶ V} : (forget X).map f = f.right :=
  rfl

Forgetful Functor Maps Morphisms to Their Right Components in Under Category

Informal description

For any objects $U$ and $V$ in the under category of $X$ and any morphism $f \colon U \to V$ in this under category, the image of $f$ under the forgetful functor equals the right component of $f$, i.e., $(forget\,X).map\,f = f.right$.

CategoryTheory.Under.forgetCone definition

(X : T) : Limits.Cone (forget X)

Full source

/-- The natural cone over the forgetful functor `Under X ⥤ T` with cone point `X`. -/
@[simps]
def forgetCone (X : T) : Limits.Cone (forget X) :=
  { pt := X
    π := { app := Comma.hom } }

Natural cone over the forgetful functor of the under category

Informal description

For an object $X$ in a category $T$, the natural cone over the forgetful functor $\text{Under}(X) \to T$ has $X$ as its cone point. The components of the cone are given by the morphisms in the under category $\text{Under}(X)$.

CategoryTheory.Under.map definition

{Y : T} (f : X ⟶ Y) : Under Y ⥤ Under X

Full source

/-- A morphism `X ⟶ Y` induces a functor `Under Y ⥤ Under X` in the obvious way. -/
def map {Y : T} (f : X ⟶ Y) : UnderUnder Y ⥤ Under X :=
  Comma.mapLeft _ <| Discrete.natTrans fun _ => f

Functor induced by a morphism on under categories

Informal description

Given a morphism $f \colon X \to Y$ in a category $T$, the functor $\text{Under}(f) \colon \text{Under}(Y) \to \text{Under}(X)$ maps: - An object $U$ in $\text{Under}(Y)$ (i.e., a morphism $U \colon Y \to U.\text{right}$) to the object in $\text{Under}(X)$ given by the composition $f \circ U \colon X \to U.\text{right}$ - A morphism $\alpha \colon U \to V$ in $\text{Under}(Y)$ (i.e., a commutative triangle) to the corresponding morphism in $\text{Under}(X)$ induced by the same underlying morphism.

CategoryTheory.Under.map_obj_right theorem

: ((map f).obj U).right = U.right

Full source

@[simp]
theorem map_obj_right : ((map f).obj U).right = U.right :=
  rfl

Preservation of Right Component by Under Category Functor

Informal description

For any morphism $f \colon X \to Y$ in a category $T$ and any object $U$ in the under category $\mathrm{Under}(Y)$, the right component of the object obtained by applying the functor $\mathrm{Under}(f)$ to $U$ is equal to the right component of $U$. That is, $(\mathrm{Under}(f)(U)).\mathrm{right} = U.\mathrm{right}$.

CategoryTheory.Under.map_obj_hom theorem

: ((map f).obj U).hom = f ≫ U.hom

Full source

@[simp]
theorem map_obj_hom : ((map f).obj U).hom = f ≫ U.hom :=
  rfl

Morphism Component of Under Category Functor Image

Informal description

For a morphism $f \colon X \to Y$ in a category $T$ and an object $U$ in the under category $\mathrm{Under}(Y)$ (represented by a morphism $U.\mathrm{hom} \colon Y \to U.\mathrm{right}$), the morphism component of the image of $U$ under the functor $\mathrm{map}(f)$ is given by the composition $f \circ U.\mathrm{hom} \colon X \to U.\mathrm{right}$.

CategoryTheory.Under.map_map_right theorem

: ((map f).map g).right = g.right

Full source

@[simp]
theorem map_map_right : ((map f).map g).right = g.right :=
  rfl

Preservation of Right Component by Under Category Functor

Informal description

For any morphism $f \colon X \to Y$ in a category $T$ and any morphism $g \colon U \to V$ in the under category $\mathrm{Under}(Y)$, the right component of the morphism $\mathrm{map}(f).\mathrm{map}(g)$ in $\mathrm{Under}(X)$ equals the right component of $g$.

CategoryTheory.Under.mapIso definition

{Y : T} (f : X ≅ Y) : Under Y ≌ Under X

Full source

/-- If `f` is an isomorphism, `map f` is an equivalence of categories. -/
def mapIso {Y : T} (f : X ≅ Y) : UnderUnder Y ≌ Under X :=
  Comma.mapLeftIso _ <| Discrete.natIso fun _ ↦ f.symm

Equivalence of under categories induced by an isomorphism

Informal description

Given an isomorphism $f \colon X \cong Y$ in a category $T$, the functor $\mathrm{mapIso}\,f$ induces an equivalence of categories between the under category $\mathrm{Under}\,Y$ and the under category $\mathrm{Under}\,X$. This equivalence is constructed using the inverse isomorphism $f^{-1}$ to map objects and morphisms between the two under categories.

CategoryTheory.Under.mapIso_functor theorem

{Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom

Full source

@[simp] lemma mapIso_functor {Y : T} (f : X ≅ Y) : (mapIso f).functor = map f.hom := rfl

Functor Component of Under Category Equivalence Induced by Isomorphism

Informal description

Given an isomorphism $f \colon X \cong Y$ in a category $T$, the functor component of the equivalence $\mathrm{mapIso}\,f$ between the under categories $\mathrm{Under}\,Y$ and $\mathrm{Under}\,X$ is equal to the functor $\mathrm{map}\,f.\mathrm{hom}$ induced by the morphism $f.\mathrm{hom} \colon X \to Y$.

CategoryTheory.Under.mapIso_inverse theorem

{Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv

Full source

@[simp] lemma mapIso_inverse {Y : T} (f : X ≅ Y) : (mapIso f).inverse = map f.inv := rfl

Inverse of Under Category Equivalence Induced by Isomorphism

Informal description

Given an isomorphism $f \colon X \cong Y$ in a category $T$, the inverse functor of the equivalence $\mathrm{mapIso}\,f \colon \mathrm{Under}\,Y \simeq \mathrm{Under}\,X$ is equal to the functor $\mathrm{map}\,f^{-1} \colon \mathrm{Under}\,X \to \mathrm{Under}\,Y$ induced by the inverse isomorphism $f^{-1}$.

CategoryTheory.Under.mapId_eq theorem

(Y : T) : map (𝟙 Y) = 𝟭 _

Full source

/-- Mapping by the identity morphism is just the identity functor. -/
theorem mapId_eq (Y : T) : map (𝟙 Y) = 𝟭 _ := by
  fapply Functor.ext
  · intro x
    dsimp [Under, Under.map, Comma.mapLeft]
    simp only [Category.id_comp]
    exact rfl
  · intros x y u
    dsimp [Under, Under.map, Comma.mapLeft]
    simp

Identity Morphism Induces Identity Functor on Under Category

Informal description

For any object $Y$ in a category $T$, the functor $\mathrm{map}(\mathrm{id}_Y)$ induced by the identity morphism on $Y$ is equal to the identity functor on the under category $\mathrm{Under}(Y)$.

CategoryTheory.Under.mapId definition

(Y : T) : map (𝟙 Y) ≅ 𝟭 _

Full source

/-- Mapping by the identity morphism is just the identity functor. -/
@[simps!]
def mapId (Y : T) : mapmap (𝟙 Y) ≅ 𝟭 _ := eqToIso (mapId_eq Y)

Natural isomorphism between identity-induced functor and identity functor on under category

Informal description

For any object $Y$ in a category $T$, the functor $\mathrm{map}(\mathrm{id}_Y)$ induced by the identity morphism on $Y$ is naturally isomorphic to the identity functor on the under category $\mathrm{Under}(Y)$.

CategoryTheory.Under.mapForget_eq theorem

{X Y : T} (f : X ⟶ Y) : (map f) ⋙ (forget X) = (forget Y)

Full source

/-- Mapping by `f` and then forgetting is the same as forgetting. -/
theorem mapForget_eq {X Y : T} (f : X ⟶ Y) :
    (map f) ⋙ (forget X) = (forget Y) := by
  fapply Functor.ext
  · dsimp [Under, Under.map]; intro x; exact rfl
  · intros x y u; simp

Compatibility of Under-Category Functors: $\mathrm{map}\,f \circ \mathrm{forget}\,X = \mathrm{forget}\,Y$

Informal description

For any objects $X$ and $Y$ in a category $T$ and any morphism $f \colon X \to Y$, the composition of the functor $\mathrm{map}\,f \colon \mathrm{Under}\,Y \to \mathrm{Under}\,X$ with the forgetful functor $\mathrm{forget}\,X \colon \mathrm{Under}\,X \to T$ is equal to the forgetful functor $\mathrm{forget}\,Y \colon \mathrm{Under}\,Y \to T$.

CategoryTheory.Under.mapForget definition

{X Y : T} (f : X ⟶ Y) : (map f) ⋙ (forget X) ≅ (forget Y)

Full source

/-- The natural isomorphism arising from `mapForget_eq`. -/
def mapForget {X Y : T} (f : X ⟶ Y) :
    (map f) ⋙ (forget X)(map f) ⋙ (forget X) ≅ (forget Y) := eqToIso (mapForget_eq f)

Natural isomorphism from under-category functor composition equality

Informal description

For any objects $X$ and $Y$ in a category $T$ and any morphism $f \colon X \to Y$, there is a natural isomorphism between the composition of functors $\mathrm{map}\,f \circ \mathrm{forget}\,X$ and the forgetful functor $\mathrm{forget}\,Y$ in the under categories. This isomorphism arises from the equality $\mathrm{map}\,f \circ \mathrm{forget}\,X = \mathrm{forget}\,Y$ via the $\mathrm{eqToIso}$ construction.

CategoryTheory.Under.eqToHom_right theorem

{X : T} {U V : Under X} (e : U = V) : (eqToHom e).right = eqToHom (e ▸ rfl : U.right = V.right)

Full source

@[simp]
theorem eqToHom_right {X : T} {U V : Under X} (e : U = V) :
    (eqToHom e).right = eqToHom (e ▸ rfl : U.right = V.right) := by
  subst e; rfl

Right Component of Equality-Induced Morphism in Under Category

Informal description

For any object $X$ in a category $T$, and any two objects $U, V$ in the under category $\mathrm{Under}\,X$, given an equality $e : U = V$, the right component of the morphism $\mathrm{eqToHom}\,e$ is equal to $\mathrm{eqToHom}\,(e \triangleright \mathrm{rfl})$, where $e \triangleright \mathrm{rfl}$ is the induced equality $U.\mathrm{right} = V.\mathrm{right}$.

CategoryTheory.Under.mapComp_eq theorem

{X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) = (map g) ⋙ (map f)

Full source

/-- Mapping by the composite morphism `f ≫ g` is the same as mapping by `f` then by `g`. -/
theorem mapComp_eq {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    map (f ≫ g) = (map g) ⋙ (map f) := by
  fapply Functor.ext
  · simp [Under.map, Comma.mapLeft]
  · intro U V k
    ext
    simp

Functoriality of Under Categories with Respect to Composition: $\mathrm{map}(f \circ g) = \mathrm{map}(g) \circ \mathrm{map}(f)$

Informal description

For any objects $X, Y, Z$ in a category $T$ and morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, the functor induced by the composite morphism $f \circ g$ on the under categories is equal to the composition of the functors induced by $g$ followed by $f$. That is, $\mathrm{map}(f \circ g) = \mathrm{map}(g) \circ \mathrm{map}(f)$.

CategoryTheory.Under.mapComp definition

{Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) ≅ map g ⋙ map f

Full source

/-- The natural isomorphism arising from `mapComp_eq`. -/
@[simps!]
def mapComp {Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : mapmap (f ≫ g) ≅ map g ⋙ map f :=
  eqToIso (mapComp_eq f g)

Natural isomorphism for composition of under category functors

Informal description

For any objects $X, Y, Z$ in a category $T$ and morphisms $f \colon X \to Y$ and $g \colon Y \to Z$, there is a natural isomorphism between the functor $\mathrm{map}(f \circ g)$ and the composition of functors $\mathrm{map}(g) \circ \mathrm{map}(f)$ on the under categories. This isomorphism arises from the equality $\mathrm{map}(f \circ g) = \mathrm{map}(g) \circ \mathrm{map}(f)$ via the $\mathrm{eqToIso}$ construction.

CategoryTheory.Under.mapCongr definition

{X Y : T} (f g : X ⟶ Y) (h : f = g) : map f ≅ map g

Full source

/-- If `f = g`, then `map f` is naturally isomorphic to `map g`. -/
@[simps!]
def mapCongr {X Y : T} (f g : X ⟶ Y) (h : f = g) :
    mapmap f ≅ map g :=
  NatIso.ofComponents (fun A ↦ eqToIso (by rw [h]))

Natural isomorphism between under category functors induced by equal morphisms

Informal description

Given two morphisms $ f, g \colon X \to Y $ in a category $ T $ and an equality $ h \colon f = g $, the functors $ \text{map}\,f $ and $ \text{map}\,g $ from the under category of $ Y $ to the under category of $ X $ are naturally isomorphic. The natural isomorphism is constructed by applying the isomorphism induced by equality $ h $ to each object in the under category.

CategoryTheory.Under.mapFunctor definition

: Tᵒᵖ ⥤ Cat

Full source

/-- The functor defined by the under categories -/
@[simps] def mapFunctor : TᵒᵖTᵒᵖ  ⥤ Cat where
  obj X := Cat.of (Under X.unop)
  map f := map f.unop
  map_id X := mapId_eq X.unop
  map_comp f g := mapComp_eq (g.unop) (f.unop)

Functor of under categories

Informal description

The functor $\text{mapFunctor} \colon T^{\mathrm{op}} \to \mathrm{Cat}$ maps: - Each object $X$ in the opposite category $T^{\mathrm{op}}$ to the category $\mathrm{Under}\,X$ of objects under $X$ - Each morphism $f \colon X \to Y$ in $T^{\mathrm{op}}$ (which corresponds to $f \colon Y \to X$ in $T$) to the functor $\mathrm{Under}(f) \colon \mathrm{Under}\,Y \to \mathrm{Under}\,X$ that precomposes with $f$ This assembles all under categories into a single functor from $T^{\mathrm{op}}$ to the category of categories.

CategoryTheory.Under.forget_reflects_iso instance

: (forget X).ReflectsIsomorphisms

Full source

instance forget_reflects_iso : (forget X).ReflectsIsomorphisms where
  reflects {Y Z} f t := by
    let g : Z ⟶ Y := Under.homMk (inv ((Under.forget X).map f))
      ((IsIso.comp_inv_eq _).2 (Under.w f).symm)
    dsimp [forget] at t
    refine ⟨⟨g, ⟨?_,?_⟩⟩⟩
    repeat (ext; simp [g])

Forgetful Functor from Under Category Reflects Isomorphisms

Informal description

The forgetful functor from the under category of an object $X$ in a category $T$ to $T$ reflects isomorphisms. That is, if a morphism $f$ in the under category is mapped to an isomorphism in $T$ by the forgetful functor, then $f$ itself is an isomorphism in the under category.

CategoryTheory.Under.mkIdInitial definition

: Limits.IsInitial (mk (𝟙 X))

Full source

/-- The identity under `X` is initial. -/
noncomputable def mkIdInitial : Limits.IsInitial (mk (𝟙 X)) :=
  StructuredArrow.mkIdInitial

Initiality of the identity morphism in the under category

Informal description

The object in the under category of $X$ induced by the identity morphism $\mathrm{id}_X \colon X \to X$ is an initial object in the under category $\mathrm{Under}\,X$.

CategoryTheory.Under.forget_faithful instance

: (forget X).Faithful

Full source

instance forget_faithful : (forget X).Faithful where

-- TODO: Show the converse holds if `T` has binary coproducts.

Faithfulness of the Under Category Forgetful Functor

Informal description

The forgetful functor from the under category of an object $X$ in a category $T$ to $T$ itself is faithful. This means that for any two morphisms $f, g$ in the under category, if their images under the forgetful functor are equal in $T$, then $f = g$ in the under category.

CategoryTheory.Under.mono_of_mono_right theorem

{f g : Under X} (k : f ⟶ g) [hk : Mono k.right] : Mono k

Full source

/-- 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 mono_of_mono_right {f g : Under X} (k : f ⟶ g) [hk : Mono k.right] : Mono k :=
  (forget X).mono_of_mono_map hk

Monomorphism in Under Category Induced by Monomorphism on Right Component

Informal description

Let $X$ be an object in a category $T$, and let $f, g$ be objects in the under category $\mathrm{Under}\,X$ (i.e., morphisms in $T$ with domain $X$). For any morphism $k \colon f \to g$ in $\mathrm{Under}\,X$, if the right component $k.\mathrm{right}$ (the morphism between the codomains of $f$ and $g$) is a monomorphism in $T$, then $k$ is a monomorphism in $\mathrm{Under}\,X$.

CategoryTheory.Under.epi_of_epi_right theorem

{f g : Under X} (k : f ⟶ g) [hk : Epi k.right] : Epi k

Full source

/--
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.
-/
theorem epi_of_epi_right {f g : Under X} (k : f ⟶ g) [hk : Epi k.right] : Epi k :=
  (forget X).epi_of_epi_map hk

Epimorphism in Under Category Induced by Epimorphism in Base Category

Informal description

Let $X$ be an object in a category $T$, and let $f, g$ be objects in the under category $\mathrm{Under}\,X$ (i.e., $f \colon X \to Y$ and $g \colon X \to Z$ for some objects $Y, Z$ in $T$). Given a morphism $k \colon f \to g$ in $\mathrm{Under}\,X$ such that the right component $k.\mathrm{right} \colon Y \to Z$ is an epimorphism in $T$, then $k$ itself is an epimorphism in $\mathrm{Under}\,X$.

CategoryTheory.Under.epi_right_of_epi instance

{f g : Under X} (k : f ⟶ g) [Epi k] : Epi k.right

Full source

/--
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`.
-/
instance epi_right_of_epi {f g : Under X} (k : f ⟶ g) [Epi k] : Epi k.right := by
  refine ⟨fun {Y : T} l m a => ?_⟩
  let l' : g ⟶ mk (g.hom ≫ m) := homMk l (by
    dsimp; rw [← Under.w k, Category.assoc, a, Category.assoc])
  suffices l' = (homMk m) by apply congrArg CommaMorphism.right this
  rw [← cancel_epi k]; ext; apply a

Right Component of an Epimorphism in the Under Category is Epimorphic

Informal description

For any morphism $k \colon f \to g$ in the under category of an object $X$ in a category, if $k$ is an epimorphism, then its right component $k.\mathrm{right}$ is also an epimorphism.

CategoryTheory.Under.post definition

{X : T} (F : T ⥤ D) : Under X ⥤ Under (F.obj X)

Full source

/-- A functor `F : T ⥤ D` induces a functor `Under X ⥤ Under (F.obj X)` in the obvious way. -/
@[simps]
def post {X : T} (F : T ⥤ D) : UnderUnder X ⥤ Under (F.obj X) where
  obj Y := mk <| F.map Y.hom
  map f := Under.homMk (F.map f.right)
    (by simp only [Functor.id_obj, Functor.const_obj_obj, mk_right, mk_hom, ← F.map_comp, w])

Functor induced on under categories by post-composition with $F$

Informal description

Given a functor $F \colon T \to D$ and an object $X$ in $T$, the functor $\mathrm{post}\,F$ maps objects and morphisms in the under category $\mathrm{Under}\,X$ to those in $\mathrm{Under}\,(F.obj\,X)$ by applying $F$ to the underlying morphisms and commutative triangles. - For an object $Y$ in $\mathrm{Under}\,X$ (represented by a morphism $f \colon X \to Y$), the image under $\mathrm{post}\,F$ is the object in $\mathrm{Under}\,(F.obj\,X)$ represented by $F.map\,f \colon F.obj\,X \to F.obj\,Y$. - For a morphism $k \colon Y \to Z$ in $\mathrm{Under}\,X$ (represented by a commutative triangle), the image under $\mathrm{post}\,F$ is the morphism represented by the commutative triangle obtained by applying $F$ to each component of $k$.

CategoryTheory.Under.post_comp theorem

{E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) : post (X := X) (F ⋙ G) = post (X := X) F ⋙ post G

Full source

lemma post_comp {E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) :
    post (X := X) (F ⋙ G) = postpost (X := X) F ⋙ post G :=
  rfl

Functoriality of Post-Composition in Under Categories

Informal description

Let $T$, $D$, and $E$ be categories, and let $F \colon T \to D$ and $G \colon D \to E$ be functors. For any object $X$ in $T$, the functor $\mathrm{post}\,(F \circ G)$ on the under category $\mathrm{Under}\,X$ is equal to the composition of the functors $\mathrm{post}\,F$ and $\mathrm{post}\,G$. That is, $\mathrm{post}\,(F \circ G) = \mathrm{post}\,F \circ \mathrm{post}\,G$.

CategoryTheory.Under.postComp definition

{E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) : post (X := X) (F ⋙ G) ≅ post F ⋙ post G

Full source

/-- `post (F ⋙ G)` is isomorphic (actually equal) to `post F ⋙ post G`. -/
@[simps!]
def postComp {E : Type*} [Category E] (F : T ⥤ D) (G : D ⥤ E) :
    postpost (X := X) (F ⋙ G) ≅ post F ⋙ post G :=
  NatIso.ofComponents (fun X ↦ Iso.refl _)

Natural isomorphism between post-composition functors on under categories

Informal description

For any categories $T$, $D$, and $E$, and functors $F \colon T \to D$ and $G \colon D \to E$, the functor $\mathrm{post}(F \circ G)$ (where $\circ$ denotes functor composition) is naturally isomorphic to the composition $\mathrm{post}\,F \circ \mathrm{post}\,G$ of the individual post-composition functors on the under category of an object $X$ in $T$. Here, $\mathrm{post}\,F$ denotes the functor induced on under categories by post-composition with $F$, and the natural isomorphism is given by identity isomorphisms at each object.

CategoryTheory.Under.postMap definition

{F G : T ⥤ D} (e : F ⟶ G) : post (X := X) F ⟶ post G ⋙ map (e.app X)

Full source

/-- A natural transformation `F ⟶ G` induces a natural transformation on
`Under X` up to `Under.map`. -/
@[simps]
def postMap {F G : T ⥤ D} (e : F ⟶ G) : postpost (X := X) F ⟶ post G ⋙ map (e.app X) where
  app Y := Under.homMk (e.app Y.right)

Natural transformation induced on under categories by a natural transformation between functors

Informal description

Given a natural transformation $e \colon F \to G$ between functors $F, G \colon T \to D$, the induced natural transformation $\text{postMap}(e) \colon \text{post}(F) \to \text{post}(G) \circ \text{map}(e_X)$ on under categories is defined by: - For each object $Y$ in $\text{Under}(X)$, the component at $Y$ is the morphism in $\text{Under}(G(X))$ obtained by applying $e$ to the codomain of $Y$ (i.e., $e_{Y.\text{right}} \colon F(Y.\text{right}) \to G(Y.\text{right})$). Here $\text{post}(F)$ denotes the functor induced by post-composition with $F$, and $\text{map}(e_X)$ denotes the functor induced by the component of $e$ at $X$.

CategoryTheory.Under.postCongr definition

{F G : T ⥤ D} (e : F ≅ G) : post F ≅ post G ⋙ map (e.hom.app X)

Full source

/-- If `F` and `G` are naturally isomorphic, then `Under.post F` and `Under.post G` are also
naturally isomorphic up to `Under.map` -/
@[simps!]
def postCongr {F G : T ⥤ D} (e : F ≅ G) : postpost F ≅ post G ⋙ map (e.hom.app X) :=
  NatIso.ofComponents (fun A ↦ Under.isoMk (e.app A.right))

Natural isomorphism between post-composition functors induced by a natural isomorphism of functors

Informal description

Given a natural isomorphism $e \colon F \cong G$ between functors $F, G \colon T \to D$, the functors $\mathrm{post}\,F$ and $\mathrm{post}\,G \circ \mathrm{map}\,(e.hom.app\,X)$ from the under category $\mathrm{Under}\,X$ to $\mathrm{Under}\,(F.obj\,X)$ are naturally isomorphic. Here, $\mathrm{post}\,F$ and $\mathrm{post}\,G$ are the post-composition functors induced by $F$ and $G$ respectively, and $\mathrm{map}\,(e.hom.app\,X)$ is the functor induced by the component of $e$ at $X$.

CategoryTheory.Under.instFaithfulObjPost instance

[F.Faithful] : (Under.post (X := X) F).Faithful

Full source

instance [F.Faithful] : (Under.post (X := X) F).Faithful where
  map_injective {A B} f g h := by
    ext
    exact F.map_injective (congrArg CommaMorphism.right h)

Faithfulness of the Post-Composition Functor on Under Categories

Informal description

Given a faithful functor $F \colon T \to D$ and an object $X$ in $T$, the induced functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F.obj\,X)$ is faithful.

CategoryTheory.Under.instFullObjPostOfFaithful instance

[F.Faithful] [F.Full] : (Under.post (X := X) F).Full

Full source

instance [F.Faithful] [F.Full] : (Under.post (X := X) F).Full where
  map_surjective {A B} f := by
    obtain ⟨a, ha⟩ := F.map_surjective f.right
    dsimp at a
    have w : A.hom ≫ a = B.hom := F.map_injective <| by simpa [ha] using Under.w f
    exact ⟨Under.homMk a, by ext; simpa⟩

Fullness of the Post-Composition Functor on Under Categories for Faithful and Full Functors

Informal description

For any faithful and full functor $F \colon T \to D$ and any object $X$ in $T$, the induced functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F.obj\,X)$ is full.

CategoryTheory.Under.instEssSurjObjPostOfFull instance

[F.Full] [F.EssSurj] : (Under.post (X := X) F).EssSurj

Full source

instance [F.Full] [F.EssSurj] : (Under.post (X := X) F).EssSurj where
  mem_essImage B := by
    obtain ⟨B', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.right
    obtain ⟨f, hf⟩ := F.map_surjective (B.hom ≫ e.inv)
    exact ⟨Under.mk f, ⟨Under.isoMk e⟩⟩

Essential Surjectivity of the Post-Composition Functor on Under Categories

Informal description

Given a full and essentially surjective functor $F \colon T \to D$ and an object $X$ in $T$, the induced functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F.obj\,X)$ is essentially surjective.

CategoryTheory.Under.instIsEquivalenceObjPost instance

[F.IsEquivalence] : (Under.post (X := X) F).IsEquivalence

Full source

instance [F.IsEquivalence] : (Under.post (X := X) F).IsEquivalence where

Post-Composition Functor on Under Categories Preserves Equivalences

Informal description

For any equivalence of categories $F \colon T \to D$ and any object $X$ in $T$, the induced functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F.obj\,X)$ is also an equivalence of categories.

CategoryTheory.Functor.FullyFaithful.under definition

(h : F.FullyFaithful) : (post (X := X) F).FullyFaithful

Full source

/-- If `F` is fully faithful, then so is `Under.post F`. -/
def _root_.CategoryTheory.Functor.FullyFaithful.under (h : F.FullyFaithful) :
    (post (X := X) F).FullyFaithful where
  preimage {A B} f := Under.homMk (h.preimage f.right) <| h.map_injective (by simpa using Under.w f)

Fully faithfulness of the post-composition functor on under categories

Informal description

Given a fully faithful functor $F \colon T \to D$ and an object $X$ in $T$, the induced functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F.obj\,X)$ is also fully faithful. Specifically, for any two objects $A$ and $B$ in $\mathrm{Under}\,X$ (represented by morphisms $f_A \colon X \to A$ and $f_B \colon X \to B$), the functor $\mathrm{post}\,F$ induces a bijection between the morphisms $A \to B$ in $\mathrm{Under}\,X$ and the morphisms $F.obj\,A \to F.obj\,B$ in $\mathrm{Under}\,(F.obj\,X)$. The preimage of a morphism $g \colon F.obj\,A \to F.obj\,B$ under $\mathrm{post}\,F$ is constructed using the preimage of $g$ under $F$, which exists because $F$ is fully faithful.

CategoryTheory.Under.postAdjunctionLeft definition

{X : T} {F : T ⥤ D} {G : D ⥤ T} (a : F ⊣ G) : post F ⊣ post G ⋙ map (a.unit.app X)

Full source

/-- 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)`. -/
@[simps]
def postAdjunctionLeft {X : T} {F : T ⥤ D} {G : D ⥤ T} (a : F ⊣ G) :
    postpost F ⊣ post G ⋙ map (a.unit.app X) where
  unit.app A := homMk <| a.unit.app A.right
  counit.app A := homMk <| a.counit.app A.right

Adjunction between post-composition functors on under categories

Informal description

Given an adjunction $F \dashv G$ between functors $F \colon T \to D$ and $G \colon D \to T$ with unit $\eta$ and counit $\epsilon$, the functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F X)$ is left adjoint to the composition of $\mathrm{post}\,G$ with the functor $\mathrm{map}\,(\eta_X) \colon \mathrm{Under}\,(G F X) \to \mathrm{Under}\,X$. The unit and counit of this adjunction are defined as follows: - For an object $A$ in $\mathrm{Under}\,X$, the component of the unit at $A$ is given by $\eta_{A.\mathrm{right}}$. - For an object $A$ in $\mathrm{Under}\,(F X)$, the component of the counit at $A$ is given by $\epsilon_{A.\mathrm{right}}$.

CategoryTheory.Under.isLeftAdjoint_post instance

[F.IsLeftAdjoint] : (post (X := X) F).IsLeftAdjoint

Full source

instance isLeftAdjoint_post [F.IsLeftAdjoint] : (post (X := X) F).IsLeftAdjoint :=
  let ⟨G, ⟨a⟩⟩ := ‹F.IsLeftAdjoint›; ⟨_, ⟨postAdjunctionLeft a⟩⟩

Right Adjoint Preservation by Post-Composition on Under Categories

Informal description

For any functor $F \colon T \to D$ that has a right adjoint, the induced post-composition functor $\mathrm{post}\,F \colon \mathrm{Under}\,X \to \mathrm{Under}\,(F.obj\,X)$ also has a right adjoint.

CategoryTheory.Under.postEquiv definition

(F : T ≌ D) : Under X ≌ Under (F.functor.obj X)

Full source

/-- An equivalence of categories induces an equivalence on under categories. -/
@[simps]
def postEquiv (F : T ≌ D) : UnderUnder X ≌ Under (F.functor.obj X) where
  functor := post F.functor
  inverse := post (X := F.functor.obj X) F.inverse ⋙ Under.map (F.unitIso.hom.app X)
  unitIso := NatIso.ofComponents (fun A ↦ Under.isoMk (F.unitIso.app A.right))
  counitIso := NatIso.ofComponents (fun A ↦ Under.isoMk (F.counitIso.app A.right))

Equivalence of under categories induced by an equivalence of categories

Informal description

Given an equivalence of categories $F \colon T \simeq D$, the under category $\mathrm{Under}\,X$ of an object $X$ in $T$ is equivalent to the under category $\mathrm{Under}\,(F(X))$ in $D$. The equivalence is constructed as follows: - The forward functor maps objects and morphisms in $\mathrm{Under}\,X$ to those in $\mathrm{Under}\,(F(X))$ by applying $F$ to the underlying morphisms and commutative triangles. - The inverse functor is obtained by applying the inverse functor $F^{-1}$ of the equivalence $F$ to $\mathrm{Under}\,(F(X))$ and then composing with the map induced by the unit isomorphism of $F$ at $X$. - The unit and counit natural isomorphisms are constructed using the components of the unit and counit isomorphisms of $F$ applied to the codomains of the morphisms in the under categories.

CategoryTheory.Under.equivalenceOfIsInitial definition

(hX : IsInitial X) : Under X ≌ T

Full source

/-- If `X : T` is initial, then the under category of `X` is equivalent to `T`. -/
@[simps]
def equivalenceOfIsInitial (hX : IsInitial X) : UnderUnder X ≌ T where
  functor := forget X
  inverse := { obj Y := mk (hX.to Y), map f := homMk f }
  unitIso := NatIso.ofComponents fun Y ↦ isoMk (.refl _) (hX.hom_ext _ _)
  counitIso := NatIso.ofComponents fun _ ↦ .refl _

Equivalence between under category of initial object and base category

Informal description

If $X$ is an initial object in a category $T$, then the under category $\mathrm{Under}\,X$ is equivalent to $T$ itself. The equivalence is given by: - The forgetful functor $\mathrm{forget}\,X \colon \mathrm{Under}\,X \to T$ which maps each object (a morphism with domain $X$) to its codomain in $T$. - An inverse functor that sends each object $Y$ in $T$ to the object $\mathrm{mk}\,(h_X\!\cdot\!Y)$ in $\mathrm{Under}\,X$, where $h_X\!\cdot\!Y$ is the unique morphism from $X$ to $Y$. - Natural isomorphisms witnessing the equivalence, where the unit isomorphisms are constructed using the identity morphism and the counit isomorphisms are identity isomorphisms.

CategoryTheory.StructuredArrow.toUnder definition

(X : T) (F : D ⥤ T) : StructuredArrow X F ⥤ Under X

Full source

/-- Reinterpreting an `F`-structured arrow `X ⟶ F.obj d` as an arrow under `X` induces a functor
    `StructuredArrow X F ⥤ Under X`. -/
@[simps!]
def toUnder (X : T) (F : D ⥤ T) : StructuredArrowStructuredArrow X F ⥤ Under X :=
  StructuredArrow.pre X F (𝟭 T)

Functor from structured arrows to under category

Informal description

Given an object $X$ in a category $T$ and a functor $F \colon D \to T$, the functor $\mathrm{toUnder}$ maps an $F$-structured arrow $X \to F(d)$ (an object in $\mathrm{StructuredArrow}\,X\,F$) to the corresponding morphism in the under category $\mathrm{Under}\,X$.

CategoryTheory.StructuredArrow.instFaithfulUnderToUnder instance

(X : T) (F : D ⥤ T) [F.Faithful] : (toUnder X F).Faithful

Full source

instance (X : T) (F : D ⥤ T) [F.Faithful] : (toUnder X F).Faithful :=
  show (StructuredArrow.pre _ _ _).Faithful from inferInstance

Faithfulness of the Functor from Structured Arrows to Under Category

Informal description

For any object $X$ in a category $T$ and any faithful functor $F \colon D \to T$, the functor $\mathrm{toUnder}\,X\,F \colon \mathrm{StructuredArrow}\,X\,F \to \mathrm{Under}\,X$ is faithful. This means that for any two morphisms $f, g$ in $\mathrm{StructuredArrow}\,X\,F$, if $\mathrm{toUnder}\,X\,F(f) = \mathrm{toUnder}\,X\,F(g)$, then $f = g$.

CategoryTheory.StructuredArrow.instFullUnderToUnder instance

(X : T) (F : D ⥤ T) [F.Full] : (toUnder X F).Full

Full source

instance (X : T) (F : D ⥤ T) [F.Full] : (toUnder X F).Full :=
  show (StructuredArrow.pre _ _ _).Full from inferInstance

Fullness of the Structured Arrow to Under Category Functor for Full Functors

Informal description

For any object $X$ in a category $T$ and any full functor $F \colon D \to T$, the functor $\mathrm{toUnder}\,X\,F$ from structured arrows to the under category is full. That is, for any two objects $f \colon X \to F(d_1)$ and $g \colon X \to F(d_2)$ in $\mathrm{StructuredArrow}\,X\,F$, every morphism $\theta \colon f \to g$ in $\mathrm{Under}\,X$ is in the image of $\mathrm{toUnder}\,X\,F$.

CategoryTheory.StructuredArrow.instEssSurjUnderToUnder instance

(X : T) (F : D ⥤ T) [F.EssSurj] : (toUnder X F).EssSurj

Full source

instance (X : T) (F : D ⥤ T) [F.EssSurj] : (toUnder X F).EssSurj :=
  show (StructuredArrow.pre _ _ _).EssSurj from inferInstance

Essential Surjectivity of the Structured Arrow to Under Category Functor

Informal description

For any object $X$ in a category $T$ and any essentially surjective functor $F \colon D \to T$, the functor $\mathrm{toUnder}\,X\,F$ from the category of $F$-structured arrows to the under category of $X$ is essentially surjective.

CategoryTheory.StructuredArrow.isEquivalence_toUnder instance

(X : T) (F : D ⥤ T) [F.IsEquivalence] : (toUnder X F).IsEquivalence

Full source

/-- An equivalence `F` induces an equivalence `StructuredArrow X F ≌ Under X`. -/
instance isEquivalence_toUnder (X : T) (F : D ⥤ T) [F.IsEquivalence] :
    (toUnder X F).IsEquivalence :=
  StructuredArrow.isEquivalence_pre _ _ _

Equivalence between Structured Arrows and Under Category for Equivalences

Informal description

For any object $X$ in a category $T$ and an equivalence of categories $F \colon D \to T$, the functor $\mathrm{toUnder}\,X\,F$ from the category of $F$-structured arrows to the under category $\mathrm{Under}\,X$ is an equivalence of categories.

CategoryTheory.Functor.essImage.of_overPost theorem

{Y : Over (F.obj X)} : (Over.post F (X := X)).essImage Y → F.essImage Y.left

Full source

lemma essImage.of_overPost {Y : Over (F.obj X)} :
    (Over.post F (X := X)).essImage Y → F.essImage Y.left :=
  fun ⟨Z, ⟨e⟩⟩ ↦ ⟨Z.left, ⟨(Over.forget _).mapIso e⟩⟩

Essential Image Inclusion for Pushforward Functor on Over Categories

Informal description

For any object $Y$ in the over category $\mathrm{Over}(F(X))$, if $Y$ lies in the essential image of the pushforward functor $\mathrm{Over.post}\,F$, then the domain of $Y$ (denoted $Y.\mathrm{left}$) lies in the essential image of $F$.

CategoryTheory.Functor.essImage.of_underPost theorem

{Y : Under (F.obj X)} : (Under.post F (X := X)).essImage Y → F.essImage Y.right

Full source

lemma essImage.of_underPost {Y : Under (F.obj X)} :
    (Under.post F (X := X)).essImage Y → F.essImage Y.right :=
  fun ⟨Z, ⟨e⟩⟩ ↦ ⟨Z.right, ⟨(Under.forget _).mapIso e⟩⟩

Essential Image Property for Post-Composition Functor on Under Categories

Informal description

For any object $Y$ in the under category $\mathrm{Under}(F(X))$, if $Y$ lies in the essential image of the functor $\mathrm{Under.post}\,F$, then the codomain object $Y.\mathrm{right}$ lies in the essential image of $F$.

CategoryTheory.Functor.essImage_overPost theorem

[F.Full] {Y : Over (F.obj X)} : (Over.post F (X := X)).essImage Y ↔ F.essImage Y.left

Full source

/-- The essential image of `Over.post F` where `F` is full is the same as the essential image of
`F`. -/
@[simp] lemma essImage_overPost [F.Full] {Y : Over (F.obj X)} :
    (Over.post F (X := X)).essImage Y ↔ F.essImage Y.left where
  mp := .of_overPost
  mpr := fun ⟨Z, ⟨e⟩⟩ ↦ let ⟨f, hf⟩ := F.map_surjective (e.hom ≫ Y.hom); ⟨.mk f, ⟨Over.isoMk e⟩⟩

Essential Image Correspondence for Pushforward Functor on Over Categories

Informal description

Let $F \colon T \to D$ be a full functor between categories, and let $X$ be an object in $T$. For any object $Y$ in the over category $\mathrm{Over}(F(X))$, the following are equivalent: 1. $Y$ lies in the essential image of the pushforward functor $\mathrm{Over.post}\,F \colon \mathrm{Over}(X) \to \mathrm{Over}(F(X))$. 2. The domain object $Y.\mathrm{left}$ of $Y$ lies in the essential image of $F$.

CategoryTheory.Functor.essImage_underPost theorem

[F.Full] {Y : Under (F.obj X)} : (Under.post F (X := X)).essImage Y ↔ F.essImage Y.right

Full source

/-- The essential image of `Under.post F` where `F` is full is the same as the essential image of
`F`. -/
@[simp] lemma essImage_underPost [F.Full] {Y : Under (F.obj X)} :
    (Under.post F (X := X)).essImage Y ↔ F.essImage Y.right where
  mp := .of_underPost
  mpr := fun ⟨Z, ⟨e⟩⟩ ↦ let ⟨f, hf⟩ := F.map_surjective (Y.hom ≫ e.inv); ⟨.mk f, ⟨Under.isoMk e⟩⟩

Essential Image Correspondence for Post-Composition Functor on Under Categories

Informal description

For a full functor $F \colon T \to D$ and an object $X$ in $T$, an object $Y$ in the under category $\mathrm{Under}(F(X))$ lies in the essential image of the post-composition functor $\mathrm{Under.post}\,F$ if and only if the codomain object $Y.\mathrm{right}$ lies in the essential image of $F$.

CategoryTheory.Functor.toOver definition

 (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) : S ⥤ Over X

Full source

/-- 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. -/
@[simps! obj_left map_left]
def toOver (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) : S ⥤ Over X :=
  F.toCostructuredArrow (𝟭 _) X f h

Functor to the over category of $X$

Informal description

Given a functor $F \colon S \to T$ and an object $X$ in $T$, the construction `toOver` upgrades $F$ to a functor $S \to \mathrm{Over}\,X$ by providing, for each object $Y$ in $S$, a morphism $F(Y) \to X$ such that for any morphism $g \colon Y \to Z$ in $S$, the diagram \[ F(Y) \xrightarrow{F(g)} F(Z) \xrightarrow{f_Z} X \] commutes with the given morphism $f_Y \colon F(Y) \to X$.

CategoryTheory.Functor.toOverCompForget definition

 (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) :
  F.toOver X f h ⋙ Over.forget _ ≅ F

Full source

/-- Upgrading a functor `S ⥤ T` to a functor `S ⥤ Over X` and composing with the forgetful functor
    `Over X ⥤ T` recovers the original functor. -/
def toOverCompForget (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) : F.toOver X f h ⋙ Over.forget _F.toOver X f h ⋙ Over.forget _ ≅ F :=
  Iso.refl _

Natural isomorphism between composed functor and original functor in over category

Informal description

Given a functor $F \colon S \to T$, an object $X$ in $T$, and for each object $Y$ in $S$ a morphism $f_Y \colon F(Y) \to X$ such that for any morphism $g \colon Y \to Z$ in $S$ the diagram \[ F(Y) \xrightarrow{F(g)} F(Z) \xrightarrow{f_Z} X \] commutes with $f_Y$, then the composition of the upgraded functor $F.toOver\,X\,f\,h \colon S \to \mathrm{Over}\,X$ with the forgetful functor $\mathrm{Over}\,X \to T$ is naturally isomorphic to the original functor $F$.

CategoryTheory.Functor.toOver_comp_forget theorem

 (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X) (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) :
  F.toOver X f h ⋙ Over.forget _ = F

Full source

@[simp]
lemma toOver_comp_forget (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) : F.toOver X f h ⋙ Over.forget _ = F :=
  rfl

Composition of Induced Over Functor with Forgetful Functor Equals Original Functor

Informal description

Given a functor $F \colon S \to T$, an object $X$ in $T$, and for each object $Y$ in $S$ a morphism $f_Y \colon F(Y) \to X$ such that for any morphism $g \colon Y \to Z$ in $S$ the diagram \[ F(Y) \xrightarrow{F(g)} F(Z) \xrightarrow{f_Z} X \] commutes (i.e., $F(g) \circ f_Z = f_Y$), then the composition of the induced functor $F.toOver\,X\,f\,h \colon S \to \mathrm{Over}\,X$ with the forgetful functor $\mathrm{Over}.forget\,X \colon \mathrm{Over}\,X \to T$ is equal to $F$.

CategoryTheory.Functor.toUnder definition

 (F : S ⥤ T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z) : S ⥤ Under X

Full source

/-- 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. -/
@[simps! obj_right map_right]
def toUnder (F : S ⥤ T) (X : T) (f : (Y : S) → X ⟶ F.obj Y)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z) : S ⥤ Under X :=
  F.toStructuredArrow X (𝟭 _) f h

Functor to under category

Informal description

Given a functor $F \colon S \to T$ and an object $X$ in $T$, the function `toUnder` upgrades $F$ to a functor $S \to \mathrm{Under}\,X$ by providing, for each object $Y$ in $S$, a morphism $f_Y \colon X \to F(Y)$ such that for any morphism $g \colon Y \to Z$ in $S$, the diagram \[ \begin{tikzcd} X \arrow[r, "f_Y"] \arrow[dr, "f_Z"'] & F(Y) \arrow[d, "F(g)"] \\ & F(Z) \end{tikzcd} \] commutes (i.e., $f_Y \circ F(g) = f_Z$).

CategoryTheory.Functor.toUnderCompForget definition

 (F : S ⥤ T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z) :
  F.toUnder X f h ⋙ Under.forget _ ≅ F

Full source

/-- Upgrading a functor `S ⥤ T` to a functor `S ⥤ Under X` and composing with the forgetful functor
    `Under X ⥤ T` recovers the original functor. -/
def toUnderCompForget (F : S ⥤ T) (X : T) (f : (Y : S) → X ⟶ F.obj Y)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z) : F.toUnder X f h ⋙ Under.forget _F.toUnder X f h ⋙ Under.forget _ ≅ F :=
  Iso.refl _

Natural isomorphism between composed functor and original functor in under category

Informal description

Given a functor $F \colon S \to T$, an object $X$ in $T$, and for each object $Y$ in $S$ a morphism $f_Y \colon X \to F(Y)$ such that for any morphism $g \colon Y \to Z$ in $S$ the diagram commutes ($f_Y \circ F(g) = f_Z$), then the composition of the upgraded functor $F.toUnder\,X\,f\,h \colon S \to \mathrm{Under}\,X$ with the forgetful functor $\mathrm{Under}\,X \to T$ is naturally isomorphic to the original functor $F$.

CategoryTheory.Functor.toUnder_comp_forget theorem

 (F : S ⥤ T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z) :
  F.toUnder X f h ⋙ Under.forget _ = F

Full source

@[simp]
lemma toUnder_comp_forget (F : S ⥤ T) (X : T) (f : (Y : S) → X ⟶ F.obj Y)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), f Y ≫ F.map g = f Z) : F.toUnder X f h ⋙ Under.forget _ = F :=
  rfl

Composition of Induced Under Functor with Forgetful Functor Equals Original Functor

Informal description

Given a functor $F \colon S \to T$, an object $X$ in $T$, and for each object $Y$ in $S$ a morphism $f_Y \colon X \to F(Y)$ such that for any morphism $g \colon Y \to Z$ in $S$ the diagram \[ \begin{tikzcd} X \arrow[r, "f_Y"] \arrow[dr, "f_Z"'] & F(Y) \arrow[d, "F(g)"] \\ & F(Z) \end{tikzcd} \] commutes (i.e., $f_Y \circ F(g) = f_Z$), then the composition of the induced functor $F.\mathrm{toUnder}\,X\,f\,h \colon S \to \mathrm{Under}\,X$ with the forgetful functor $\mathrm{Under.forget} \colon \mathrm{Under}\,X \to T$ is equal to $F$ itself.

CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor definition

 (F : D ⥤ T) (Y : T) (X : D) : StructuredArrow X (StructuredArrow.proj Y F) ⥤ StructuredArrow Y (Under.forget X ⋙ F)

Full source

/-- A functor from the structured arrow category on the projection functor for any structured
arrow category. -/
@[simps!]
def ofStructuredArrowProjEquivalence.functor (F : D ⥤ T) (Y : T) (X : D) :
    StructuredArrowStructuredArrow X (StructuredArrow.proj Y F) ⥤ StructuredArrow Y (Under.forget X ⋙ F) :=
  Functor.toStructuredArrow
    (Functor.toUnder (StructuredArrow.projStructuredArrow.proj X _ ⋙ StructuredArrow.proj Y _) _
      (fun g => by exact g.hom) (fun m => by have := m.w; aesop_cat)) _ _
    (fun f => f.right.hom) (by simp)

Functor from structured arrow category over projection to structured arrow category over composition

Informal description

Given functors $F \colon D \to T$, an object $Y$ in $T$, and an object $X$ in $D$, the functor maps objects and morphisms from the structured arrow category over $X$ with respect to the projection functor $\text{StructuredArrow.proj}\,Y\,F$ to the structured arrow category over $Y$ with respect to the composition of the forgetful functor from the under category of $X$ with $F$.

CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse definition

 (F : D ⥤ T) (Y : T) (X : D) : StructuredArrow Y (Under.forget X ⋙ F) ⥤ StructuredArrow X (StructuredArrow.proj Y F)

Full source

/-- The inverse functor of `ofStructuredArrowProjEquivalence.functor`. -/
@[simps!]
def ofStructuredArrowProjEquivalence.inverse (F : D ⥤ T) (Y : T) (X : D) :
    StructuredArrowStructuredArrow Y (Under.forget X ⋙ F) ⥤ StructuredArrow X (StructuredArrow.proj Y F) :=
  Functor.toStructuredArrow
    (Functor.toStructuredArrow (StructuredArrow.projStructuredArrow.proj Y _ ⋙ Under.forget X) _ _
      (fun g => by exact g.hom) (fun m => by have := m.w; aesop_cat)) _ _
    (fun f => f.right.hom) (by simp)

Inverse functor for structured arrow equivalence

Informal description

Given functors $F \colon D \to T$, an object $Y$ in $T$, and an object $X$ in $D$, the inverse functor maps objects and morphisms from the structured arrow category over $Y$ with respect to the composition of the forgetful functor from the under category of $X$ with $F$ to the structured arrow category over $X$ with respect to the projection functor $\text{StructuredArrow.proj}\,Y\,F$.

CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence definition

 (F : D ⥤ T) (Y : T) (X : D) : StructuredArrow X (StructuredArrow.proj Y F) ≌ StructuredArrow Y (Under.forget X ⋙ F)

Full source

/-- Characterization of the structured arrow category on the projection functor of any
structured arrow category. -/
def ofStructuredArrowProjEquivalence (F : D ⥤ T) (Y : T) (X : D) :
    StructuredArrowStructuredArrow X (StructuredArrow.proj Y F) ≌ StructuredArrow Y (Under.forget X ⋙ F) where
  functor := ofStructuredArrowProjEquivalence.functor F Y X
  inverse := ofStructuredArrowProjEquivalence.inverse F Y X
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)

Equivalence between structured arrow categories over projection and composition

Informal description

Given a functor $F \colon D \to T$, an object $Y$ in $T$, and an object $X$ in $D$, there is an equivalence of categories between: 1. The structured arrow category over $X$ with respect to the projection functor $\text{StructuredArrow.proj}\,Y\,F$ 2. The structured arrow category over $Y$ with respect to the composition of the forgetful functor from the under category of $X$ with $F$ This equivalence is constructed via functors that preserve the categorical structure, with natural isomorphisms ensuring the equivalence conditions are satisfied.

CategoryTheory.StructuredArrow.ofDiagEquivalence.functor definition

(X : T × T) : StructuredArrow X (Functor.diag _) ⥤ StructuredArrow X.2 (Under.forget X.1)

Full source

/-- The canonical functor from the structured arrow category on the diagonal functor
`T ⥤ T × T` to the structured arrow category on `Under.forget`. -/
@[simps!]
def ofDiagEquivalence.functor (X : T × T) :
    StructuredArrowStructuredArrow X (Functor.diag _) ⥤ StructuredArrow X.2 (Under.forget X.1) :=
  Functor.toStructuredArrow
    (Functor.toUnder (StructuredArrow.proj X _) _
      (fun f => by exact f.hom.1) (fun m => by have := m.w; aesop_cat)) _ _
    (fun f => f.hom.2) (fun m => by have := m.w; aesop_cat)

Functor from structured arrows over diagonal to structured arrows over under category

Informal description

Given an object $X = (X_1, X_2)$ in the product category $T \times T$, the functor maps an object in the structured arrow category over the diagonal functor $\text{diag} \colon T \to T \times T$ to an object in the structured arrow category over the forgetful functor $\text{Under.forget} \colon \text{Under}\,X_1 \to T$. Specifically, it sends a morphism $f \colon X \to \text{diag}(Y)$ (where $Y \in T$) to the morphism $f_2 \colon X_2 \to Y$ in $T$, viewed as an object in $\text{Under}\,X_1$ via the canonical construction.

CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse definition

(X : T × T) : StructuredArrow X.2 (Under.forget X.1) ⥤ StructuredArrow X (Functor.diag _)

Full source

/-- The inverse functor of `ofDiagEquivalence.functor`. -/
@[simps!]
def ofDiagEquivalence.inverse (X : T × T) :
    StructuredArrowStructuredArrow X.2 (Under.forget X.1) ⥤ StructuredArrow X (Functor.diag _) :=
  Functor.toStructuredArrow (StructuredArrow.projStructuredArrow.proj _ _ ⋙ Under.forget _) _ _
    (fun f => (f.right.hom, f.hom)) (fun m => by have := m.w; aesop_cat)

Inverse functor of the diagonal-structured arrow equivalence

Informal description

Given a pair of objects $X = (X_1, X_2)$ in the product category $T \times T$, the inverse functor of the equivalence between: 1. The category of structured arrows over $X$ with respect to the diagonal functor $\text{diag} : T \to T \times T$ 2. The category of structured arrows over $X_2$ with respect to the forgetful functor $\text{Under.forget} : \text{Under}\,X_1 \to T$ This functor maps: - An object $(f : X_2 \to Y, \alpha)$ in the second category to the object $((f, \alpha) : X \to (Y, Y))$ in the first category - A morphism (commutative triangle) between such objects to the corresponding morphism in the first category

CategoryTheory.StructuredArrow.ofDiagEquivalence definition

(X : T × T) : StructuredArrow X (Functor.diag _) ≌ StructuredArrow X.2 (Under.forget X.1)

Full source

/-- Characterization of the structured arrow category on the diagonal functor `T ⥤ T × T`. -/
def ofDiagEquivalence (X : T × T) :
    StructuredArrowStructuredArrow X (Functor.diag _) ≌ StructuredArrow X.2 (Under.forget X.1) where
  functor := ofDiagEquivalence.functor X
  inverse := ofDiagEquivalence.inverse X
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)

Equivalence between structured arrows over diagonal and under categories

Informal description

For any pair of objects $X = (X_1, X_2)$ in the product category $T \times T$, there is an equivalence of categories between: 1. The category of structured arrows over $X$ with respect to the diagonal functor $\text{diag} \colon T \to T \times T$ 2. The category of structured arrows over $X_2$ with respect to the forgetful functor $\text{Under.forget} \colon \text{Under}\,X_1 \to T$ This equivalence is implemented by: - A functor that maps a morphism $f \colon X \to \text{diag}(Y)$ to $f_2 \colon X_2 \to Y$ viewed in $\text{Under}\,X_1$ - An inverse functor that maps a morphism $(f \colon X_2 \to Y, \alpha)$ to $((f, \alpha) \colon X \to (Y, Y))$ - Natural isomorphisms given by identity morphisms

CategoryTheory.StructuredArrow.ofDiagEquivalence' definition

(X : T × T) : StructuredArrow X (Functor.diag _) ≌ StructuredArrow X.1 (Under.forget X.2)

Full source

/-- A version of `StructuredArrow.ofDiagEquivalence` with the roles of the first and second
projection swapped. -/
-- noncomputability is only for performance
noncomputable def ofDiagEquivalence' (X : T × T) :
    StructuredArrowStructuredArrow X (Functor.diag _) ≌ StructuredArrow X.1 (Under.forget X.2) :=
  (ofDiagEquivalence X).trans <|
    (ofStructuredArrowProjEquivalence (𝟭 T) X.1 X.2).trans <|
    StructuredArrow.mapNatIso (Under.forget X.2).rightUnitor

Equivalence between structured arrows over diagonal and under categories (swapped version)

Informal description

For any pair of objects $X = (X_1, X_2)$ in the product category $T \times T$, there is an equivalence of categories between: 1. The category of structured arrows over $X$ with respect to the diagonal functor $\text{diag} \colon T \to T \times T$ 2. The category of structured arrows over $X_1$ with respect to the forgetful functor $\text{Under.forget} \colon \text{Under}\,X_2 \to T$ This equivalence is constructed by: - First applying the equivalence $\text{ofDiagEquivalence}$ between structured arrows over $X$ and structured arrows over $X_2$ with respect to $\text{Under.forget}\,X_1$ - Then composing with the equivalence $\text{ofStructuredArrowProjEquivalence}$ for the identity functor on $T$ - Finally applying a natural isomorphism involving the right unitor of the forgetful functor from $\text{Under}\,X_2$

CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor definition

(c : C) : StructuredArrow c (Comma.fst F G) ⥤ Comma (Under.forget c ⋙ F) G

Full source

/-- The functor used to define the equivalence `ofCommaSndEquivalence`. -/
@[simps]
def ofCommaSndEquivalenceFunctor (c : C) :
    StructuredArrowStructuredArrow c (Comma.fst F G) ⥤ Comma (Under.forget c ⋙ F) G where
  obj X := ⟨Under.mk X.hom, X.right.right, X.right.hom⟩
  map f := ⟨Under.homMk f.right.left (by simpa using f.w.symm), f.right.right, by simp⟩

Functor from structured arrows to comma categories via under categories

Informal description

The functor maps an object $X$ in the category of structured arrows over $c$ with respect to the first projection functor $\text{Comma.fst}\,F\,G$ to an object in the comma category $\text{Comma}\,(\text{Under.forget}\,c \circ F)\,G$, defined as $\langle \text{Under.mk}\,X.\text{hom}, X.\text{right}.\text{right}, X.\text{right}.\text{hom} \rangle$. For a morphism $f$, it maps to $\langle \text{Under.homMk}\,f.\text{right}.\text{left}, f.\text{right}.\text{right}, \text{by simp} \rangle$.

CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse definition

(c : C) : Comma (Under.forget c ⋙ F) G ⥤ StructuredArrow c (Comma.fst F G)

Full source

/-- The inverse functor used to define the equivalence `ofCommaSndEquivalence`. -/
@[simps!]
def ofCommaSndEquivalenceInverse (c : C) :
    CommaComma (Under.forget c ⋙ F) G ⥤ StructuredArrow c (Comma.fst F G) :=
  Functor.toStructuredArrow (Comma.preLeft (Under.forget c) F G) _ _
    (fun Y => Y.left.hom) (fun _ => by simp)

Inverse functor for the equivalence of structured arrows and comma categories

Informal description

The inverse functor used to define the equivalence between the category of structured arrows over $c$ with respect to the first projection functor $\text{Comma.fst}\,F\,G$ and the comma category of the composition of the forgetful functor from the under category of $c$ with $F$ and $G$. Specifically, this functor maps objects and morphisms from the comma category $\text{Comma}\,(\text{Under.forget}\,c \circ F)\,G$ back to the structured arrow category $\text{StructuredArrow}\,c\,(\text{Comma.fst}\,F\,G)$.

CategoryTheory.StructuredArrow.ofCommaSndEquivalence definition

(c : C) : StructuredArrow c (Comma.fst F G) ≌ Comma (Under.forget c ⋙ F) G

Full source

/-- 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`. -/
@[simps]
def ofCommaSndEquivalence (c : C) :
    StructuredArrowStructuredArrow c (Comma.fst F G) ≌ Comma (Under.forget c ⋙ F) G where
  functor := ofCommaSndEquivalenceFunctor F G c
  inverse := ofCommaSndEquivalenceInverse F G c
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _)

Equivalence between structured arrows and comma categories via under categories

Informal description

For any object $c$ in a category $C$, there is a canonical equivalence between: 1. The category of structured arrows over $c$ with respect to the first projection functor $\text{Comma.fst}\,F\,G \colon \text{Comma}\,F\,G \to F$, and 2. The comma category of the composition $\text{Under.forget}\,c \circ F \colon \text{Under}\,c \to T$ with $G$. This equivalence is constructed using the functor $\text{ofCommaSndEquivalenceFunctor}$ and its inverse $\text{ofCommaSndEquivalenceInverse}$, with both unit and counit isomorphisms being identity isomorphisms.

CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor definition

 (F : T ⥤ D) (Y : D) (X : T) :
  CostructuredArrow (CostructuredArrow.proj F Y) X ⥤ CostructuredArrow (Over.forget X ⋙ F) Y

Full source

/-- A functor from the costructured arrow category on the projection functor for any costructured
arrow category. -/
@[simps!]
def ofCostructuredArrowProjEquivalence.functor (F : T ⥤ D) (Y : D) (X : T) :
    CostructuredArrowCostructuredArrow (CostructuredArrow.proj F Y) X ⥤ CostructuredArrow (Over.forget X ⋙ F) Y :=
  Functor.toCostructuredArrow
    (Functor.toOver (CostructuredArrow.projCostructuredArrow.proj _ X ⋙ CostructuredArrow.proj F Y) _
      (fun g => by exact g.hom) (fun m => by have := m.w; aesop_cat)) _ _
    (fun f => f.left.hom) (by simp)

Functor from costructured arrow category of projection to costructured arrow category of composition

Informal description

Given a functor $F \colon T \to D$, an object $Y$ in $D$, and an object $X$ in $T$, the functor maps an object in the costructured arrow category of the projection functor $(F, Y)$ to an object in the costructured arrow category of the composition of the forgetful functor from the over category of $X$ with $F$. Specifically, it sends a morphism $g$ in the costructured arrow category to its underlying morphism in $D$, ensuring the appropriate commutativity conditions are satisfied.

CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse definition

 (F : T ⥤ D) (Y : D) (X : T) :
  CostructuredArrow (Over.forget X ⋙ F) Y ⥤ CostructuredArrow (CostructuredArrow.proj F Y) X

Full source

/-- The inverse functor of `ofCostructuredArrowProjEquivalence.functor`. -/
@[simps!]
def ofCostructuredArrowProjEquivalence.inverse (F : T ⥤ D) (Y : D) (X : T) :
    CostructuredArrowCostructuredArrow (Over.forget X ⋙ F) Y ⥤ CostructuredArrow (CostructuredArrow.proj F Y) X :=
  Functor.toCostructuredArrow
    (Functor.toCostructuredArrow (CostructuredArrow.projCostructuredArrow.proj _ Y ⋙ Over.forget X) _ _
      (fun g => by exact g.hom) (fun m => by have := m.w; aesop_cat)) _ _
    (fun f => f.left.hom) (by simp)

Inverse functor for costructured arrow projection equivalence

Informal description

Given a functor $F \colon T \to D$, an object $Y$ in $D$, and an object $X$ in $T$, the inverse functor of the equivalence between: 1. The category of costructured arrows from the projection functor $\mathrm{CostructuredArrow.proj}\,F\,Y$ to $X$, and 2. The category of costructured arrows from the composition of the forgetful functor $\mathrm{Over.forget}\,X$ with $F$ to $Y$. This functor maps objects and morphisms in the second category back to the first category, completing the equivalence.

CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence definition

 (F : T ⥤ D) (Y : D) (X : T) :
  CostructuredArrow (CostructuredArrow.proj F Y) X ≌ CostructuredArrow (Over.forget X ⋙ F) Y

Full source

/-- Characterization of the costructured arrow category on the projection functor of any
costructured arrow category. -/
def ofCostructuredArrowProjEquivalence (F : T ⥤ D) (Y : D) (X : T) :
    CostructuredArrowCostructuredArrow (CostructuredArrow.proj F Y) X
      ≌ CostructuredArrow (Over.forget X ⋙ F) Y where
  functor := ofCostructuredArrowProjEquivalence.functor F Y X
  inverse := ofCostructuredArrowProjEquivalence.inverse F Y X
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)

Equivalence between costructured arrow categories of projection and composition

Informal description

Given a functor $F \colon T \to D$, an object $Y$ in $D$, and an object $X$ in $T$, there is an equivalence of categories between: 1. The costructured arrow category of the projection functor $\mathrm{CostructuredArrow.proj}\,F\,Y$ at $X$, and 2. The costructured arrow category of the composition of the forgetful functor $\mathrm{Over.forget}\,X$ with $F$ at $Y$. This equivalence is established via functors that preserve the structure of the costructured arrows, with natural isomorphisms ensuring the equivalence conditions are satisfied.

CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor definition

(X : T × T) : CostructuredArrow (Functor.diag _) X ⥤ CostructuredArrow (Over.forget X.1) X.2

Full source

/-- The canonical functor from the costructured arrow category on the diagonal functor
`T ⥤ T × T` to the costructured arrow category on `Under.forget`. -/
@[simps!]
def ofDiagEquivalence.functor (X : T × T) :
    CostructuredArrowCostructuredArrow (Functor.diag _) X ⥤ CostructuredArrow (Over.forget X.1) X.2 :=
  Functor.toCostructuredArrow
    (Functor.toOver (CostructuredArrow.proj _ X) _
      (fun g => by exact g.hom.1) (fun m => by have := congrArg (·.1) m.w; aesop_cat))
    _ _
    (fun f => f.hom.2) (fun m => by have := congrArg (·.2) m.w; aesop_cat)

Functor from costructured arrows on diagonal to costructured arrows on forgetful functor

Informal description

Given an object $X = (X_1, X_2)$ in the product category $T \times T$, the functor maps from the costructured arrow category on the diagonal functor $\text{diag} \colon T \to T \times T$ at $X$ to the costructured arrow category on the forgetful functor $\text{Over.forget}\,X_1$ at $X_2$. More precisely, it sends an object $(Y, (f_1, f_2))$ in the costructured arrow category of $\text{diag}$ (where $Y \in T$ and $(f_1, f_2) \colon \text{diag}(Y) \to X$ is a morphism in $T \times T$) to the object $(Y, f_2)$ in the costructured arrow category of $\text{Over.forget}\,X_1$ (where $f_2 \colon Y \to X_2$ is a morphism in $T$).

CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse definition

(X : T × T) : CostructuredArrow (Over.forget X.1) X.2 ⥤ CostructuredArrow (Functor.diag _) X

Full source

/-- The inverse functor of `ofDiagEquivalence.functor`. -/
@[simps!]
def ofDiagEquivalence.inverse (X : T × T) :
    CostructuredArrowCostructuredArrow (Over.forget X.1) X.2 ⥤ CostructuredArrow (Functor.diag _) X :=
  Functor.toCostructuredArrow (CostructuredArrow.projCostructuredArrow.proj _ _ ⋙ Over.forget _) _ X
    (fun f => (f.left.hom, f.hom)) (fun m => by have := m.w; aesop_cat)

Inverse functor for diagonal equivalence of costructured arrows

Informal description

Given an object $X = (X_1, X_2)$ in the product category $T \times T$, the inverse functor of the equivalence between the costructured arrow category of the diagonal functor at $X$ and the costructured arrow category of the forgetful functor from the over category of $X_1$ applied to $X_2$. This functor maps objects and morphisms in the costructured arrow category of the forgetful functor back to the costructured arrow category of the diagonal functor.

CategoryTheory.CostructuredArrow.ofDiagEquivalence definition

(X : T × T) : CostructuredArrow (Functor.diag _) X ≌ CostructuredArrow (Over.forget X.1) X.2

Full source

/-- Characterization of the costructured arrow category on the diagonal functor `T ⥤ T × T`. -/
def ofDiagEquivalence (X : T × T) :
    CostructuredArrowCostructuredArrow (Functor.diag _) X ≌ CostructuredArrow (Over.forget X.1) X.2 where
  functor := ofDiagEquivalence.functor X
  inverse := ofDiagEquivalence.inverse X
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)

Equivalence between costructured arrow categories of diagonal and forgetful functors

Informal description

For any object $X = (X_1, X_2)$ in the product category $T \times T$, there is an equivalence of categories between: 1. The costructured arrow category of the diagonal functor $\text{diag} \colon T \to T \times T$ at $X$, whose objects are pairs $(Y, (f_1, f_2))$ where $Y \in T$ and $(f_1, f_2) \colon (Y, Y) \to (X_1, X_2)$ is a morphism in $T \times T$, 2. The costructured arrow category of the forgetful functor from the over category of $X_1$ at $X_2$, whose objects are pairs $(Y, f_2)$ where $Y \in T$ and $f_2 \colon Y \to X_2$ is a morphism in $T$. This equivalence is established via functors that preserve the underlying objects and morphisms appropriately.

CategoryTheory.CostructuredArrow.ofDiagEquivalence' definition

(X : T × T) : CostructuredArrow (Functor.diag _) X ≌ CostructuredArrow (Over.forget X.2) X.1

Full source

/-- A version of `CostructuredArrow.ofDiagEquivalence` with the roles of the first and second
projection swapped. -/
-- noncomputability is only for performance
noncomputable def ofDiagEquivalence' (X : T × T) :
    CostructuredArrowCostructuredArrow (Functor.diag _) X ≌ CostructuredArrow (Over.forget X.2) X.1 :=
  (ofDiagEquivalence X).trans <|
    (ofCostructuredArrowProjEquivalence (𝟭 T) X.1 X.2).trans <|
    CostructuredArrow.mapNatIso (Over.forget X.2).rightUnitor

Equivalence between costructured arrow categories of diagonal and swapped forgetful functors

Informal description

For any object $ X = (X_1, X_2) $ in the product category $ T \times T $, there is an equivalence of categories between: 1. The costructured arrow category of the diagonal functor $ \text{diag} \colon T \to T \times T $ at $ X $, whose objects are pairs $ (Y, (f_1, f_2)) $ where $ Y \in T $ and $ (f_1, f_2) \colon (Y, Y) \to (X_1, X_2) $ is a morphism in $ T \times T $, 2. The costructured arrow category of the forgetful functor from the over category of $ X_2 $ at $ X_1 $, whose objects are pairs $ (Y, f_1) $ where $ Y \in T $ and $ f_1 \colon Y \to X_1 $ is a morphism in $ T $. This equivalence is constructed by composing three equivalences: - The equivalence from the diagonal functor to the forgetful functor from the over category of $ X_1 $ at $ X_2 $, - The equivalence swapping the roles of $ X_1 $ and $ X_2 $, - The natural isomorphism given by the right unitor of the forgetful functor from the over category of $ X_2 $.

CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor definition

(c : C) : CostructuredArrow (Comma.fst F G) c ⥤ Comma (Over.forget c ⋙ F) G

Full source

/-- The functor used to define the equivalence `ofCommaFstEquivalence`. -/
@[simps]
def ofCommaFstEquivalenceFunctor (c : C) :
    CostructuredArrowCostructuredArrow (Comma.fst F G) c ⥤ Comma (Over.forget c ⋙ F) G where
  obj X := ⟨Over.mk X.hom, X.left.right, X.left.hom⟩
  map f := ⟨Over.homMk f.left.left (by simpa using f.w), f.left.right, by simp⟩

Functor from costructured arrows to comma category via over category

Informal description

Given an object $c$ in a category $C$, the functor maps an object $X$ in the costructured arrow category $\mathrm{CostructuredArrow}\,(\mathrm{Comma.fst}\,F\,G)\,c$ to an object in the comma category $\mathrm{Comma}\,(\mathrm{Over.forget}\,c \circ F)\,G$. Specifically, for each object $X$, the functor constructs an object in the comma category consisting of: 1. An object in the over category of $c$ obtained via $\mathrm{Over.mk}\,X.\mathrm{hom}$, 2. The object $X.\mathrm{left}.\mathrm{right}$, 3. The morphism $X.\mathrm{left}.\mathrm{hom}$. For a morphism $f$ in the costructured arrow category, the functor constructs a morphism in the comma category using $\mathrm{Over.homMk}$ applied to $f.\mathrm{left}.\mathrm{left}$ and a proof of commutativity derived from $f.\mathrm{w}$.

CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse definition

(c : C) : Comma (Over.forget c ⋙ F) G ⥤ CostructuredArrow (Comma.fst F G) c

Full source

/-- The inverse functor used to define the equivalence `ofCommaFstEquivalence`. -/
@[simps!]
def ofCommaFstEquivalenceInverse (c : C) :
    CommaComma (Over.forget c ⋙ F) G ⥤ CostructuredArrow (Comma.fst F G) c :=
  Functor.toCostructuredArrow (Comma.preLeft (Over.forget c) F G) _ _
    (fun Y => Y.left.hom) (fun _ => by simp)

Inverse functor for equivalence between costructured arrows and comma category via over category

Informal description

Given an object $c$ in a category $C$, the inverse functor maps an object $Y$ in the comma category $\mathrm{Comma}\,(\mathrm{Over.forget}\,c \circ F)\,G$ to an object in the costructured arrow category $\mathrm{CostructuredArrow}\,(\mathrm{Comma.fst}\,F\,G)\,c$. Specifically, for each object $Y$, the functor constructs an object in the costructured arrow category consisting of: 1. The object $Y.\mathrm{left}$ in the over category of $c$, 2. The object $Y.\mathrm{right}$, 3. The morphism $Y.\mathrm{hom}$. For a morphism $f$ in the comma category, the functor constructs a morphism in the costructured arrow category using the left component of $f$ and a proof of commutativity derived from $f$'s properties.

CategoryTheory.CostructuredArrow.ofCommaFstEquivalence definition

(c : C) : CostructuredArrow (Comma.fst F G) c ≌ Comma (Over.forget c ⋙ F) G

Full source

/-- 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`. -/
@[simps]
def ofCommaFstEquivalence (c : C) :
    CostructuredArrowCostructuredArrow (Comma.fst F G) c ≌ Comma (Over.forget c ⋙ F) G where
  functor := ofCommaFstEquivalenceFunctor F G c
  inverse := ofCommaFstEquivalenceInverse F G c
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _)

Equivalence between costructured arrows and comma category via over category

Informal description

For any object $c$ in a category $C$, there is a canonical equivalence between: 1. The costructured arrow category with codomain $c$ on the functor $\mathrm{Comma.fst}\,F\,G : \mathrm{Comma}\,F\,G \to F$, and 2. The comma category over the composition $\mathrm{Over.forget}\,c \circ F : \mathrm{Over}\,c \to T$ and $G$. This equivalence consists of: - A functor mapping objects and morphisms from the costructured arrow category to the comma category, - An inverse functor mapping in the opposite direction, - Natural isomorphisms (unit and counit) that are identity isomorphisms at each component.

CategoryTheory.Over.opEquivOpUnder definition

: Over (op X) ≌ (Under X)ᵒᵖ

Full source

/-- The canonical equivalence between over and under categories by reversing structure arrows. -/
@[simps]
def Over.opEquivOpUnder : OverOver (op X) ≌ (Under X)ᵒᵖ where
  functor.obj Y := ⟨Under.mk Y.hom.unop⟩
  functor.map {Z Y} f := ⟨Under.homMk (f.left.unop) (by dsimp; rw [← unop_comp, Over.w])⟩
  inverse.obj Y := Over.mk (Y.unop.hom.op)
  inverse.map {Z Y} f := Over.homMk f.unop.right.op <| by dsimp; rw [← Under.w f.unop, op_comp]
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Equivalence between over category of $\mathrm{op}\,X$ and opposite under category of $X$

Informal description

The canonical equivalence between the over category of the opposite object $\mathrm{op}\,X$ and the opposite of the under category of $X$. Specifically: - The functor maps an object $(Y \to \mathrm{op}\,X)$ in $\mathrm{Over}\,(\mathrm{op}\,X)$ to the object $(X \to Y)$ in $(\mathrm{Under}\,X)^{\mathrm{op}}$. - The inverse functor maps an object $(X \to Y)$ in $(\mathrm{Under}\,X)^{\mathrm{op}}$ back to $(Y \to \mathrm{op}\,X)$ in $\mathrm{Over}\,(\mathrm{op}\,X)$. - The unit and counit isomorphisms are both identity isomorphisms.

CategoryTheory.Under.opEquivOpOver definition

: Under (op X) ≌ (Over X)ᵒᵖ

Full source

/-- The canonical equivalence between under and over categories by reversing structure arrows. -/
@[simps]
def Under.opEquivOpOver : UnderUnder (op X) ≌ (Over X)ᵒᵖ where
  functor.obj Y := ⟨Over.mk Y.hom.unop⟩
  functor.map {Z Y} f := ⟨Over.homMk (f.right.unop) (by dsimp; rw [← unop_comp, Under.w])⟩
  inverse.obj Y := Under.mk (Y.unop.hom.op)
  inverse.map {Z Y} f := Under.homMk f.unop.left.op <| by dsimp; rw [← Over.w f.unop, op_comp]
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Equivalence between under category of $\mathrm{op}\,X$ and opposite of over category of $X$

Informal description

The canonical equivalence between the under category of the opposite object $\mathrm{op}\,X$ and the opposite of the over category of $X$. Specifically: - The functor maps an object $Y$ in $\mathrm{Under}\,(\mathrm{op}\,X)$ to $\mathrm{Over.mk}\,(Y.\mathrm{hom}.\mathrm{unop})$ in $(\mathrm{Over}\,X)^{\mathrm{op}}$. - The inverse functor maps an object $Y$ in $(\mathrm{Over}\,X)^{\mathrm{op}}$ to $\mathrm{Under.mk}\,(Y.\mathrm{unop}.\mathrm{hom}.\mathrm{op})$ in $\mathrm{Under}\,(\mathrm{op}\,X)$. - The unit and counit isomorphisms are both identity isomorphisms.

CategoryTheory.Over.opToOpUnder definition

: Over (op X) ⥤ (Under X)ᵒᵖ

Full source

/-- The canonical functor by reversing structure arrows. -/
@[deprecated Over.opEquivOpUnder (since := "2025-04-08")]
def Over.opToOpUnder : OverOver (op X) ⥤ (Under X)ᵒᵖ := (Over.opEquivOpUnder X).functor

Functor from over category of $\mathrm{op}\,X$ to opposite under category of $X$

Informal description

The canonical functor from the over category of the opposite object $\mathrm{op}\,X$ to the opposite of the under category of $X$. This functor maps an object $(Y \to \mathrm{op}\,X)$ in $\mathrm{Over}\,(\mathrm{op}\,X)$ to the object $(X \to Y)$ in $(\mathrm{Under}\,X)^{\mathrm{op}}$, and similarly for morphisms.

CategoryTheory.Under.opToOverOp definition

: (Under X)ᵒᵖ ⥤ Over (op X)

Full source

/-- The canonical functor by reversing structure arrows. -/
@[deprecated Over.opEquivOpUnder (since := "2025-04-08")]
def Under.opToOverOp : (Under X)ᵒᵖ(Under X)ᵒᵖ ⥤ Over (op X) := (Over.opEquivOpUnder X).inverse

Functor from opposite under category to over category of opposite object

Informal description

The functor from the opposite of the under category of $X$ to the over category of the opposite object $\mathrm{op}\,X$. This functor is part of the equivalence between these two categories, where: - Objects $(X \to Y)$ in $(\mathrm{Under}\,X)^{\mathrm{op}}$ are mapped to $(Y \to \mathrm{op}\,X)$ in $\mathrm{Over}\,(\mathrm{op}\,X)$ - Morphisms are correspondingly transformed to maintain the categorical structure

CategoryTheory.Under.opToOpOver definition

: Under (op X) ⥤ (Over X)ᵒᵖ

Full source

/-- The canonical functor by reversing structure arrows. -/
@[deprecated Under.opEquivOpOver (since := "2025-04-08")]
def Under.opToOpOver : UnderUnder (op X) ⥤ (Over X)ᵒᵖ := (Under.opEquivOpOver X).functor

Functor from under category of opposite object to opposite over category

Informal description

The canonical functor from the under category of the opposite object $\mathrm{op}\,X$ to the opposite of the over category of $X$. This functor is part of an equivalence between these two categories, where: - Objects $(Y \to \mathrm{op}\,X)$ in $\mathrm{Under}\,(\mathrm{op}\,X)$ are mapped to $(X \to Y)$ in $(\mathrm{Over}\,X)^{\mathrm{op}}$ - Morphisms are correspondingly transformed to maintain the categorical structure

CategoryTheory.Over.opToUnderOp definition

: (Over X)ᵒᵖ ⥤ Under (op X)

Full source

/-- The canonical functor by reversing structure arrows. -/
@[deprecated Under.opEquivOpOver (since := "2025-04-08")]
def Over.opToUnderOp : (Over X)ᵒᵖ(Over X)ᵒᵖ ⥤ Under (op X) := (Under.opEquivOpOver X).inverse

Functor from opposite over category to under category of opposite object

Informal description

The functor from the opposite of the over category of $X$ to the under category of the opposite object $\mathrm{op}\,X$. This functor is part of the equivalence between these two categories, where: - Objects $(Y \to X)$ in $(\mathrm{Over}\,X)^{\mathrm{op}}$ are mapped to $(\mathrm{op}\,X \to Y)$ in $\mathrm{Under}\,(\mathrm{op}\,X)$ - Morphisms are correspondingly transformed to maintain the categorical structure

Tags