Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

CategoryTheory.StructuredArrow definition

(S : D) (T : C ⥤ D)

Full source

/-- The category of `T`-structured arrows with domain `S : D` (here `T : C ⥤ D`),
has as its objects `D`-morphisms of the form `S ⟶ T Y`, for some `Y : C`,
and morphisms `C`-morphisms `Y ⟶ Y'` making the obvious triangle commute.
-/
-- We explicitly come from `PUnit.{1}` here to obtain the correct universe for morphisms of
-- structured arrows.
def StructuredArrow (S : D) (T : C ⥤ D) :=
  Comma (Functor.fromPUnit.{0} S) T

Category of $T$-structured arrows with domain $S$

Informal description

For a functor $T \colon C \to D$ and an object $S \colon D$, the category of $T$-structured arrows with domain $S$ has as objects the morphisms $S \to T(Y)$ in $D$ for some $Y \colon C$, and as morphisms the $C$-morphisms $Y \to Y'$ making the obvious triangle commute.

CategoryTheory.instCategoryStructuredArrow instance

(S : D) (T : C ⥤ D) : Category (StructuredArrow S T)

Full source

instance (S : D) (T : C ⥤ D) : Category (StructuredArrow S T) := commaCategory

Category of $T$-Structured Arrows with Domain $S$

Informal description

For any functor $T \colon C \to D$ and object $S \colon D$, the category of $T$-structured arrows with domain $S$ forms a category. The objects are morphisms $S \to T(Y)$ in $D$ for some $Y \colon C$, and the morphisms are $C$-morphisms $Y \to Y'$ making the obvious triangle commute.

CategoryTheory.StructuredArrow.proj definition

(S : D) (T : C ⥤ D) : StructuredArrow S T ⥤ C

Full source

/-- The obvious projection functor from structured arrows. -/
@[simps!]
def proj (S : D) (T : C ⥤ D) : StructuredArrowStructuredArrow S T ⥤ C :=
  Comma.snd _ _

Projection functor from structured arrows

Informal description

The projection functor from the category of $T$-structured arrows with domain $S$ to the category $C$, which maps each structured arrow $(S \to T(Y))$ to its target object $Y$ in $C$.

CategoryTheory.StructuredArrow.hom_ext theorem

{X Y : StructuredArrow S T} (f g : X ⟶ Y) (h : f.right = g.right) : f = g

Full source

@[ext]
lemma hom_ext {X Y : StructuredArrow S T} (f g : X ⟶ Y) (h : f.right = g.right) : f = g :=
  CommaMorphism.ext (Subsingleton.elim _ _) h

Extensionality of Morphisms in the Category of $T$-Structured Arrows

Informal description

For any two morphisms $f, g \colon X \to Y$ in the category of $T$-structured arrows with domain $S$, if their underlying morphisms in $C$ are equal (i.e., $f_{\mathrm{right}} = g_{\mathrm{right}}$), then $f = g$.

CategoryTheory.StructuredArrow.hom_eq_iff theorem

{X Y : StructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.right = g.right

Full source

@[simp]
theorem hom_eq_iff {X Y : StructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.right = g.right :=
  ⟨fun h ↦ by rw [h], hom_ext _ _⟩

Equality of Morphisms in Structured Arrow Category via Underlying Morphisms

Informal description

For any two morphisms $f, g \colon X \to Y$ in the category of $T$-structured arrows with domain $S$, $f$ equals $g$ if and only if their underlying morphisms in $C$ are equal (i.e., $f_{\mathrm{right}} = g_{\mathrm{right}}$).

CategoryTheory.StructuredArrow.mk definition

(f : S ⟶ T.obj Y) : StructuredArrow S T

Full source

/-- Construct a structured arrow from a morphism. -/
def mk (f : S ⟶ T.obj Y) : StructuredArrow S T :=
  ⟨⟨⟨⟩⟩, Y, f⟩

Construction of a $T$-structured arrow from a morphism

Informal description

Given a morphism $f \colon S \to T(Y)$ in the category $D$, where $T \colon C \to D$ is a functor and $Y$ is an object in $C$, this constructs a $T$-structured arrow with domain $S$ and codomain $Y$.

CategoryTheory.StructuredArrow.mk_left theorem

(f : S ⟶ T.obj Y) : (mk f).left = ⟨⟨⟩⟩

Full source

@[simp]
theorem mk_left (f : S ⟶ T.obj Y) : (mk f).left = ⟨⟨⟩⟩ :=
  rfl

Left Component of Structured Arrow is Trivial

Informal description

For any morphism $f \colon S \to T(Y)$ in the category $D$, where $T \colon C \to D$ is a functor and $Y$ is an object in $C$, the left component of the structured arrow constructed from $f$ is the unique object of the singleton category $\mathrm{PUnit}$.

CategoryTheory.StructuredArrow.mk_right theorem

(f : S ⟶ T.obj Y) : (mk f).right = Y

Full source

@[simp]
theorem mk_right (f : S ⟶ T.obj Y) : (mk f).right = Y :=
  rfl

Right Component of Structured Arrow Construction Equals Codomain

Informal description

Given a morphism $f \colon S \to T(Y)$ in the category $D$, where $T \colon C \to D$ is a functor and $Y$ is an object in $C$, the right component of the structured arrow constructed from $f$ is equal to $Y$.

CategoryTheory.StructuredArrow.mk_hom_eq_self theorem

(f : S ⟶ T.obj Y) : (mk f).hom = f

Full source

@[simp]
theorem mk_hom_eq_self (f : S ⟶ T.obj Y) : (mk f).hom = f :=
  rfl

Structured Arrow Construction Preserves Morphism

Informal description

Given a morphism $f \colon S \to T(Y)$ in a category $D$, where $T \colon C \to D$ is a functor and $Y$ is an object in $C$, the homomorphism associated with the structured arrow constructed from $f$ is equal to $f$ itself. In other words, if we form a structured arrow from $f$, then its underlying morphism is exactly $f$.

CategoryTheory.StructuredArrow.w theorem

{A B : StructuredArrow S T} (f : A ⟶ B) : A.hom ≫ T.map f.right = B.hom

Full source

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

Commutativity of Morphisms in the Category of $T$-Structured Arrows

Informal description

For any two objects $A$ and $B$ in the category of $T$-structured arrows with domain $S$, and any morphism $f \colon A \to B$, the diagram commutes in the sense that the composite morphism $A.\text{hom} \circ T(f.\text{right})$ equals $B.\text{hom}$.

CategoryTheory.StructuredArrow.comp_right theorem

{X Y Z : StructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).right = f.right ≫ g.right

Full source

@[simp]
theorem comp_right {X Y Z : StructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).right = f.right ≫ g.right := rfl

Composition of Right Components in Structured Arrows

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the category of $T$-structured arrows with domain $S$, 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).\mathrm{right} = f.\mathrm{right} \circ g.\mathrm{right}$.

CategoryTheory.StructuredArrow.id_right theorem

(X : StructuredArrow S T) : (𝟙 X : X ⟶ X).right = 𝟙 X.right

Full source

@[simp]
theorem id_right (X : StructuredArrow S T) : (𝟙 X : X ⟶ X).right = 𝟙 X.right := rfl

Right Component of Identity Morphism in Structured Arrow Category

Informal description

For any object $X$ in the category of $T$-structured arrows with domain $S$, the right component of the identity morphism $\mathrm{id}_X$ is equal to the identity morphism on the right component of $X$, i.e., $(\mathrm{id}_X)_{\mathrm{right}} = \mathrm{id}_{X_{\mathrm{right}}}$.

CategoryTheory.StructuredArrow.eqToHom_right theorem

{X Y : StructuredArrow S T} (h : X = Y) : (eqToHom h).right = eqToHom (by rw [h])

Full source

@[simp]
theorem eqToHom_right {X Y : StructuredArrow S T} (h : X = Y) :
    (eqToHom h).right = eqToHom (by rw [h]) := by
  subst h
  simp only [eqToHom_refl, id_right]

Right Component of Equality Morphism in Structured Arrow Category

Informal description

For any two objects $X$ and $Y$ in the category of $T$-structured arrows with domain $S$, given an equality $h : X = Y$, the right component of the morphism $\text{eqToHom}\,h$ is equal to $\text{eqToHom}$ applied to the equality obtained by rewriting with $h$.

CategoryTheory.StructuredArrow.left_eq_id theorem

{X Y : StructuredArrow S T} (f : X ⟶ Y) : f.left = 𝟙 X.left

Full source

@[simp]
theorem left_eq_id {X Y : StructuredArrow S T} (f : X ⟶ Y) : f.left = 𝟙 X.left := rfl

Left Component of Morphism in Structured Arrow Category is Identity

Informal description

For any morphism $f \colon X \to Y$ in the category of $T$-structured arrows with domain $S$, the left component of $f$ is equal to the identity morphism on $X.left$, i.e., $f.left = \mathrm{id}_{X.left}$.

CategoryTheory.StructuredArrow.homMk_surjective theorem

 {f f' : StructuredArrow S T} (φ : f ⟶ f') :
  ∃ (ψ : f.right ⟶ f'.right) (hψ : f.hom ≫ T.map ψ = f'.hom), φ = StructuredArrow.homMk ψ hψ

Full source

theorem homMk_surjective {f f' : StructuredArrow S T} (φ : f ⟶ f') :
    ∃ (ψ : f.right ⟶ f'.right) (hψ : f.hom ≫ T.map ψ = f'.hom),
      φ = StructuredArrow.homMk ψ hψ :=
  ⟨φ.right, StructuredArrow.w φ, rfl⟩

Surjectivity of Morphism Construction in Structured Arrow Category

Informal description

For any morphism $\phi \colon f \to f'$ in the category of $T$-structured arrows with domain $S$, there exists a morphism $\psi \colon f.\text{right} \to f'.\text{right}$ in $C$ such that the diagram commutes, i.e., $f.\text{hom} \circ T(\psi) = f'.\text{hom}$, and $\phi$ is equal to the structured arrow morphism constructed from $\psi$ and this commutativity condition.

CategoryTheory.StructuredArrow.homMk' definition

(f : StructuredArrow S T) (g : f.right ⟶ Y') : f ⟶ mk (f.hom ≫ T.map g)

Full source

/-- Given a structured arrow `X ⟶ T(Y)`, and an arrow `Y ⟶ Y'`, we can construct a morphism of
    structured arrows given by `(X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y'))`. -/
@[simps]
def homMk' (f : StructuredArrow S T) (g : f.right ⟶ Y') : f ⟶ mk (f.hom ≫ T.map g) where
  left := 𝟙 _
  right := g

Morphism of structured arrows induced by a morphism in $C$

Informal description

Given a $T$-structured arrow $f \colon S \to T(Y)$ and a morphism $g \colon Y \to Y'$ in $C$, this constructs a morphism of structured arrows from $f$ to the composition $f \circ T(g) \colon S \to T(Y')$. The morphism is defined such that the left component is the identity on $S$ and the right component is $g$.

CategoryTheory.StructuredArrow.homMk'_id theorem

(f : StructuredArrow S T) : homMk' f (𝟙 f.right) = eqToHom (by aesop_cat)

Full source

lemma homMk'_id (f : StructuredArrow S T) : homMk' f (𝟙 f.right) = eqToHom (by aesop_cat) := by
  ext
  simp [eqToHom_right]

Identity Morphism Construction in Structured Arrow Category via $\mathrm{homMk'}$

Informal description

For any $T$-structured arrow $f$ with domain $S$, the morphism $\mathrm{homMk'}\,f\,(\mathrm{id}_{f.\mathrm{right}})$ is equal to the identity morphism constructed via $\mathrm{eqToHom}$ (with the equality proof handled automatically by `aesop_cat`).

CategoryTheory.StructuredArrow.homMk'_mk_id theorem

(f : S ⟶ T.obj Y) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp)

Full source

lemma homMk'_mk_id (f : S ⟶ T.obj Y) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp) :=
  homMk'_id _

Identity Morphism in Structured Arrow Category via $\mathrm{homMk'}$ and $\mathrm{mk}$

Informal description

For any morphism $f \colon S \to T(Y)$ in the category $D$, where $T \colon C \to D$ is a functor and $Y$ is an object in $C$, the morphism $\mathrm{homMk'}\,(\mathrm{mk}\,f)\,(\mathrm{id}_Y)$ in the category of $T$-structured arrows is equal to the identity morphism constructed via $\mathrm{eqToHom}$ (with the equality proof handled by simplification).

CategoryTheory.StructuredArrow.homMk'_comp theorem

 (f : StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') :
  homMk' f (g ≫ g') = homMk' f g ≫ homMk' (mk (f.hom ≫ T.map g)) g' ≫ eqToHom (by simp)

Full source

lemma homMk'_comp (f : StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') :
    homMk' f (g ≫ g') = homMk'homMk' f g ≫ homMk' (mk (f.hom ≫ T.map g)) g' ≫ eqToHom (by simp) := by
  ext
  simp [eqToHom_right]

Composition Law for Morphisms in the Category of $T$-Structured Arrows

Informal description

Given a $T$-structured arrow $f \colon S \to T(Y)$ and morphisms $g \colon Y \to Y'$ and $g' \colon Y' \to Y''$ in $C$, the morphism $\mathrm{homMk'}\,f\,(g \circ g')$ in the category of $T$-structured arrows is equal to the composition of: 1. $\mathrm{homMk'}\,f\,g$, 2. $\mathrm{homMk'}\,(\mathrm{mk}\,(f_{\mathrm{hom}} \circ T(g)))\,g'$, and 3. the morphism induced by equality (via $\mathrm{eqToHom}$) from the simplification of the diagram.

CategoryTheory.StructuredArrow.homMk'_mk_comp theorem

 (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
  homMk' (mk f) (g ≫ g') = homMk' (mk f) g ≫ homMk' (mk (f ≫ T.map g)) g' ≫ eqToHom (by simp)

Full source

lemma homMk'_mk_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
    homMk' (mk f) (g ≫ g') = homMk'homMk' (mk f) g ≫ homMk' (mk (f ≫ T.map g)) g' ≫ eqToHom (by simp) :=
  homMk'_comp _ _ _

Composition Law for Morphisms in the Category of $T$-Structured Arrows via $\mathrm{homMk'}$ and $\mathrm{mk}$

Informal description

Given a morphism $f \colon S \to T(Y)$ in category $D$ (where $T \colon C \to D$ is a functor) and morphisms $g \colon Y \to Y'$ and $g' \colon Y' \to Y''$ in category $C$, the morphism $\mathrm{homMk'}\,(\mathrm{mk}\,f)\,(g \circ g')$ in the category of $T$-structured arrows is equal to the composition of: 1. $\mathrm{homMk'}\,(\mathrm{mk}\,f)\,g$, 2. $\mathrm{homMk'}\,(\mathrm{mk}\,(f \circ T(g)))\,g'$, and 3. the morphism induced by equality (via $\mathrm{eqToHom}$) from the simplification of the diagram.

CategoryTheory.StructuredArrow.mkPostcomp definition

(f : S ⟶ T.obj Y) (g : Y ⟶ Y') : mk f ⟶ mk (f ≫ T.map g)

Full source

/-- Variant of `homMk'` where both objects are applications of `mk`. -/
@[simps]
def mkPostcomp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : mkmk f ⟶ mk (f ≫ T.map g) where
  left := 𝟙 _
  right := g

Postcomposition morphism in the category of $T$-structured arrows

Informal description

Given a morphism $f \colon S \to T(Y)$ in category $D$ (where $T \colon C \to D$ is a functor) and a morphism $g \colon Y \to Y'$ in category $C$, this constructs a morphism in the category of $T$-structured arrows from the object represented by $f$ to the object represented by the composition $f \circ T(g)$.

CategoryTheory.StructuredArrow.mkPostcomp_id theorem

(f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by simp)

Full source

lemma mkPostcomp_id (f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by simp) := by simp

Identity Postcomposition in Structured Arrow Category Yields Identity Morphism

Informal description

Given a morphism $f \colon S \to T(Y)$ in the category $D$, where $T \colon C \to D$ is a functor and $Y$ is an object in $C$, the postcomposition morphism in the category of $T$-structured arrows with the identity morphism $\mathrm{id}_Y$ is equal to the identity morphism constructed via $\mathrm{eqToHom}$ (after simplification).

CategoryTheory.StructuredArrow.mkPostcomp_comp theorem

 (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
  mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom (by simp)

Full source

lemma mkPostcomp_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
    mkPostcomp f (g ≫ g') = mkPostcompmkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom (by simp) := by
  simp

Composition Law for Postcomposition in $T$-Structured Arrow Category

Informal description

Given a morphism $f \colon S \to T(Y)$ in category $D$ (where $T \colon C \to D$ is a functor) and morphisms $g \colon Y \to Y'$ and $g' \colon Y' \to Y''$ in category $C$, the postcomposition morphism in the category of $T$-structured arrows satisfies: \[ \text{mkPostcomp}\,f\,(g \circ g') = \text{mkPostcomp}\,f\,g \circ \text{mkPostcomp}\,(f \circ T(g))\,g' \circ \text{eqToHom}\,(\text{by simp}) \]

CategoryTheory.StructuredArrow.ext theorem

{A B : StructuredArrow S T} (f g : A ⟶ B) : f.right = g.right → f = g

Full source

theorem ext {A B : StructuredArrow S T} (f g : A ⟶ B) : f.right = g.right → f = g :=
  CommaMorphism.ext (Subsingleton.elim _ _)

Extensionality of Morphisms in $T$-Structured Arrow Category via Right Components

Informal description

For any two morphisms $f, g \colon A \to B$ in the category of $T$-structured arrows with domain $S$, if the right components of $f$ and $g$ are equal (i.e., $f_{\text{right}} = g_{\text{right}}$), then $f = g$.

CategoryTheory.StructuredArrow.ext_iff theorem

{A B : StructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.right = g.right

Full source

theorem ext_iff {A B : StructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.right = g.right :=
  ⟨fun h => h ▸ rfl, ext f g⟩

Morphism Equality Criterion in $T$-Structured Arrow Category via Right Components

Informal description

For any two morphisms $f, g \colon A \to B$ in the category of $T$-structured arrows with domain $S$, the equality $f = g$ holds if and only if their right components are equal, i.e., $f_{\text{right}} = g_{\text{right}}$.

CategoryTheory.StructuredArrow.proj_faithful instance

: (proj S T).Faithful

Full source

instance proj_faithful : (proj S T).Faithful where
  map_injective {_ _} := ext

Faithfulness of the Projection Functor from Structured Arrows

Informal description

The projection functor from the category of $T$-structured arrows with domain $S$ to the category $C$ is faithful. That is, for any two morphisms $f, g$ in the structured arrow category, if their images under the projection functor are equal, then $f = g$.

CategoryTheory.StructuredArrow.mono_of_mono_right theorem

{A B : StructuredArrow S T} (f : A ⟶ B) [h : Mono f.right] : Mono f

Full source

/-- The converse of this is true with additional assumptions, see `mono_iff_mono_right`. -/
theorem mono_of_mono_right {A B : StructuredArrow S T} (f : A ⟶ B) [h : Mono f.right] : Mono f :=
  (proj S T).mono_of_mono_map h

Monomorphism in Structured Arrow Category Induced by Monomorphism in Right Component

Informal description

Let $T \colon C \to D$ be a functor and $S$ an object in $D$. For any morphism $f \colon A \to B$ in the category of $T$-structured arrows with domain $S$, if the right component $f_{\text{right}} \colon A_{\text{right}} \to B_{\text{right}}$ is a monomorphism in $C$, then $f$ itself is a monomorphism in the category of $T$-structured arrows.

CategoryTheory.StructuredArrow.epi_of_epi_right theorem

{A B : StructuredArrow S T} (f : A ⟶ B) [h : Epi f.right] : Epi f

Full source

theorem epi_of_epi_right {A B : StructuredArrow S T} (f : A ⟶ B) [h : Epi f.right] : Epi f :=
  (proj S T).epi_of_epi_map h

Epimorphism in Structured Arrow Category Induced by Epimorphism in Base Category

Informal description

Let $T \colon C \to D$ be a functor and $S \colon D$ an object. For any morphism $f \colon A \to B$ in the category of $T$-structured arrows with domain $S$, if the underlying morphism $f_{\text{right}} \colon A_{\text{right}} \to B_{\text{right}}$ in $C$ is an epimorphism, then $f$ itself is an epimorphism in the structured arrow category.

CategoryTheory.StructuredArrow.mono_homMk instance

{A B : StructuredArrow S T} (f : A.right ⟶ B.right) (w) [h : Mono f] : Mono (homMk f w)

Full source

instance mono_homMk {A B : StructuredArrow S T} (f : A.right ⟶ B.right) (w) [h : Mono f] :
    Mono (homMk f w) :=
  (proj S T).mono_of_mono_map h

Monomorphisms in the Category of Structured Arrows Induced by Monomorphisms in the Target Category

Informal description

For any two objects $A$ and $B$ in the category of $T$-structured arrows with domain $S$, and a morphism $f \colon A.\mathrm{right} \to B.\mathrm{right}$ in $C$ that is a monomorphism, the induced morphism $\mathrm{homMk}(f, w)$ in the structured arrow category is also a monomorphism.

CategoryTheory.StructuredArrow.epi_homMk instance

{A B : StructuredArrow S T} (f : A.right ⟶ B.right) (w) [h : Epi f] : Epi (homMk f w)

Full source

instance epi_homMk {A B : StructuredArrow S T} (f : A.right ⟶ B.right) (w) [h : Epi f] :
    Epi (homMk f w) :=
  (proj S T).epi_of_epi_map h

Epimorphisms in the Category of Structured Arrows Induced by Epimorphisms in $C$

Informal description

For any two $T$-structured arrows $A$ and $B$ with domain $S$, and a morphism $f \colon A.\mathrm{right} \to B.\mathrm{right}$ in $C$ that is an epimorphism, the induced morphism $\mathrm{homMk}\,f\,w$ in the category of $T$-structured arrows is also an epimorphism.

CategoryTheory.StructuredArrow.eta definition

(f : StructuredArrow S T) : f ≅ mk f.hom

Full source

/-- Eta rule for structured arrows. -/
@[simps! hom_right inv_right]
def eta (f : StructuredArrow S T) : f ≅ mk f.hom :=
  isoMk (Iso.refl _)

Isomorphism between a structured arrow and its construction from underlying morphism

Informal description

For any $T$-structured arrow $f$ with domain $S$, there is an isomorphism between $f$ and the structured arrow constructed from its underlying morphism $f.hom \colon S \to T(Y)$. This isomorphism is given by the identity morphism on the object $Y$ in $C$.

CategoryTheory.StructuredArrow.mk_surjective theorem

(f : StructuredArrow S T) : ∃ (Y : C) (g : S ⟶ T.obj Y), f = mk g

Full source

lemma mk_surjective (f : StructuredArrow S T) :
    ∃ (Y : C) (g : S ⟶ T.obj Y), f = mk g :=
  ⟨_, _, eq_mk f⟩

Surjectivity of Structured Arrow Construction

Informal description

For any $T$-structured arrow $f$ with domain $S$, there exists an object $Y$ in $C$ and a morphism $g \colon S \to T(Y)$ in $D$ such that $f$ is equal to the structured arrow constructed from $g$.

CategoryTheory.StructuredArrow.map definition

(f : S ⟶ S') : StructuredArrow S' T ⥤ StructuredArrow S T

Full source

/-- A morphism between source objects `S ⟶ S'`
contravariantly induces a functor between structured arrows,
`StructuredArrow S' T ⥤ StructuredArrow S T`.

Ideally this would be described as a 2-functor from `D`
(promoted to a 2-category with equations as 2-morphisms)
to `Cat`.
-/
@[simps!]
def map (f : S ⟶ S') : StructuredArrowStructuredArrow S' T ⥤ StructuredArrow S T :=
  Comma.mapLeft _ ((Functor.const _).map f)

Precomposition functor on structured arrows

Informal description

Given a morphism $f \colon S \to S'$ in the category $D$, the functor $\text{StructuredArrow.map}(f)$ maps a $T$-structured arrow with source $S'$ to a $T$-structured arrow with source $S$ by precomposing with $f$. More precisely, for any functor $T \colon C \to D$, the functor $\text{StructuredArrow.map}(f)$ sends an object $(S' \to T(Y))$ in $\text{StructuredArrow}(S', T)$ to the object $(S \to S' \to T(Y))$ in $\text{StructuredArrow}(S, T)$, and similarly for morphisms.

CategoryTheory.StructuredArrow.map_mk theorem

{f : S' ⟶ T.obj Y} (g : S ⟶ S') : (map g).obj (mk f) = mk (g ≫ f)

Full source

@[simp]
theorem map_mk {f : S' ⟶ T.obj Y} (g : S ⟶ S') : (map g).obj (mk f) = mk (g ≫ f) :=
  rfl

Functoriality of Precomposition on Structured Arrows: $\text{map}(g)(\text{mk}(f)) = \text{mk}(g \circ f)$

Informal description

Given a morphism $f \colon S' \to T(Y)$ in category $D$ and a morphism $g \colon S \to S'$ in $D$, the application of the precomposition functor $\text{map}(g)$ to the structured arrow $\text{mk}(f)$ yields the structured arrow $\text{mk}(g \circ f)$.

CategoryTheory.StructuredArrow.map_id theorem

{f : StructuredArrow S T} : (map (𝟙 S)).obj f = f

Full source

@[simp]
theorem map_id {f : StructuredArrow S T} : (map (𝟙 S)).obj f = f := by
  rw [eq_mk f]
  simp

Identity Precomposition Preserves Structured Arrows

Informal description

For any $T$-structured arrow $f$ with domain $S$, the application of the precomposition functor induced by the identity morphism $\mathrm{id}_S$ to $f$ yields $f$ itself, i.e., $\mathrm{map}(\mathrm{id}_S)(f) = f$.

CategoryTheory.StructuredArrow.map_comp theorem

{f : S ⟶ S'} {f' : S' ⟶ S''} {h : StructuredArrow S'' T} : (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)

Full source

@[simp]
theorem map_comp {f : S ⟶ S'} {f' : S' ⟶ S''} {h : StructuredArrow S'' T} :
    (map (f ≫ f')).obj h = (map f).obj ((map f').obj h) := by
  rw [eq_mk h]
  simp

Functoriality of Precomposition: $\text{map}(f \circ f') = \text{map}(f) \circ \text{map}(f')$ on Structured Arrows

Informal description

Given morphisms $f \colon S \to S'$ and $f' \colon S' \to S''$ in category $D$, and a $T$-structured arrow $h$ with domain $S''$, the precomposition functor $\text{map}(f \circ f')$ applied to $h$ is equal to the composition of the precomposition functors $\text{map}(f)$ and $\text{map}(f')$ applied to $h$.

CategoryTheory.StructuredArrow.mapIso definition

(i : S ≅ S') : StructuredArrow S T ≌ StructuredArrow S' T

Full source

/-- An isomorphism `S ≅ S'` induces an equivalence `StructuredArrow S T ≌ StructuredArrow S' T`. -/
@[simps!]
def mapIso (i : S ≅ S') : StructuredArrowStructuredArrow S T ≌ StructuredArrow S' T :=
  Comma.mapLeftIso _ ((Functor.const _).mapIso i)

Equivalence of structured arrow categories induced by domain isomorphism

Informal description

Given an isomorphism $i \colon S \cong S'$ in the category $\mathcal{D}$, there is an equivalence of categories between the category of $T$-structured arrows with domain $S$ and the category of $T$-structured arrows with domain $S'$.

CategoryTheory.StructuredArrow.mapNatIso definition

(i : T ≅ T') : StructuredArrow S T ≌ StructuredArrow S T'

Full source

/-- A natural isomorphism `T ≅ T'` induces an equivalence
    `StructuredArrow S T ≌ StructuredArrow S T'`. -/
@[simps!]
def mapNatIso (i : T ≅ T') : StructuredArrowStructuredArrow S T ≌ StructuredArrow S T' :=
  Comma.mapRightIso _ i

Equivalence of structured arrow categories induced by a natural isomorphism

Informal description

Given a natural isomorphism $i \colon T \cong T'$ between functors $T, T' \colon C \to D$, there is an equivalence of categories between the category of $T$-structured arrows with domain $S$ and the category of $T'$-structured arrows with domain $S$. This equivalence is induced by post-composing with the natural isomorphism $i$.

CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms instance

: (proj S T).ReflectsIsomorphisms

Full source

instance proj_reflectsIsomorphisms : (proj S T).ReflectsIsomorphisms where
  reflects {Y Z} f t :=
    ⟨⟨StructuredArrow.homMk
        (inv ((proj S T).map f))
        (by rw [Functor.map_inv, IsIso.comp_inv_eq]; simp),
      by constructor <;> apply CommaMorphism.ext <;> dsimp at t ⊢ <;> simp⟩⟩

Projection Functor Reflects Isomorphisms in Structured Arrows

Informal description

The projection functor from the category of $T$-structured arrows with domain $S$ to the category $C$ reflects isomorphisms. That is, if a morphism $f$ in the category of $T$-structured arrows is mapped to an isomorphism in $C$ by the projection functor, then $f$ itself is an isomorphism.

CategoryTheory.StructuredArrow.mkIdInitial definition

[T.Full] [T.Faithful] : IsInitial (mk (𝟙 (T.obj Y)))

Full source

/-- The identity structured arrow is initial. -/
noncomputable def mkIdInitial [T.Full] [T.Faithful] : IsInitial (mk (𝟙 (T.obj Y))) where
  desc c := homMk (T.preimage c.pt.hom)
  uniq c m _ := by
    apply CommaMorphism.ext
    · simp
    · apply T.map_injective
      simpa only [homMk_right, T.map_preimage, ← w m] using (Category.id_comp _).symm

Initiality of the identity structured arrow under full and faithful functors

Informal description

For a full and faithful functor $T \colon C \to D$ and an object $Y \colon C$, the identity structured arrow $\mathrm{mk}(\mathrm{id}_{T(Y)})$ is an initial object in the category of $T$-structured arrows with domain $T(Y)$. Here, the identity structured arrow is constructed from the identity morphism $\mathrm{id}_{T(Y)} \colon T(Y) \to T(Y)$, and its initiality means that for any other structured arrow $c$ with domain $T(Y)$, there exists a unique morphism from $\mathrm{mk}(\mathrm{id}_{T(Y)})$ to $c$ in the category of $T$-structured arrows.

CategoryTheory.StructuredArrow.pre definition

(S : D) (F : B ⥤ C) (G : C ⥤ D) : StructuredArrow S (F ⋙ G) ⥤ StructuredArrow S G

Full source

/-- The functor `(S, F ⋙ G) ⥤ (S, G)`. -/
@[simps!]
def pre (S : D) (F : B ⥤ C) (G : C ⥤ D) : StructuredArrowStructuredArrow S (F ⋙ G) ⥤ StructuredArrow S G :=
  Comma.preRight _ F G

Precomposition functor for structured arrows

Informal description

Given a functor $F \colon B \to C$, a functor $G \colon C \to D$, and an object $S \colon D$, the functor $\text{pre}\,S\,F\,G$ maps from the category of $(F \comp G)$-structured arrows with domain $S$ to the category of $G$-structured arrows with domain $S$.

CategoryTheory.StructuredArrow.instFaithfulCompPre instance

(S : D) (F : B ⥤ C) (G : C ⥤ D) [F.Faithful] : (pre S F G).Faithful

Full source

instance (S : D) (F : B ⥤ C) (G : C ⥤ D) [F.Faithful] : (pre S F G).Faithful :=
  show (Comma.preRight _ _ _).Faithful from inferInstance

Faithfulness of Precomposition Functor for Structured Arrows

Informal description

For any functor $F \colon B \to C$, functor $G \colon C \to D$, and object $S \colon D$, if $F$ is faithful, then the precomposition functor $\text{pre}\,S\,F\,G$ from the category of $(F \comp G)$-structured arrows with domain $S$ to the category of $G$-structured arrows with domain $S$ is also faithful.

CategoryTheory.StructuredArrow.instFullCompPre instance

(S : D) (F : B ⥤ C) (G : C ⥤ D) [F.Full] : (pre S F G).Full

Full source

instance (S : D) (F : B ⥤ C) (G : C ⥤ D) [F.Full] : (pre S F G).Full :=
  show (Comma.preRight _ _ _).Full from inferInstance

Fullness of Precomposition Functor for Structured Arrows

Informal description

For any functor $F \colon B \to C$ that is full, a functor $G \colon C \to D$, and an object $S \colon D$, the precomposition functor $\text{pre}\,S\,F\,G$ from the category of $(F \comp G)$-structured arrows with domain $S$ to the category of $G$-structured arrows with domain $S$ is full.

CategoryTheory.StructuredArrow.instEssSurjCompPre instance

(S : D) (F : B ⥤ C) (G : C ⥤ D) [F.EssSurj] : (pre S F G).EssSurj

Full source

instance (S : D) (F : B ⥤ C) (G : C ⥤ D) [F.EssSurj] : (pre S F G).EssSurj :=
  show (Comma.preRight _ _ _).EssSurj from inferInstance

Essential Surjectivity of Precomposition Functor for Structured Arrows

Informal description

For any essentially surjective functor $F \colon B \to C$, functor $G \colon C \to D$, and object $S \colon D$, the precomposition functor $\text{pre}\,S\,F\,G$ from the category of $(F \comp G)$-structured arrows with domain $S$ to the category of $G$-structured arrows with domain $S$ is essentially surjective.

CategoryTheory.StructuredArrow.isEquivalence_pre instance

(S : D) (F : B ⥤ C) (G : C ⥤ D) [F.IsEquivalence] : (pre S F G).IsEquivalence

Full source

/-- If `F` is an equivalence, then so is the functor `(S, F ⋙ G) ⥤ (S, G)`. -/
instance isEquivalence_pre (S : D) (F : B ⥤ C) (G : C ⥤ D) [F.IsEquivalence] :
    (pre S F G).IsEquivalence :=
  Comma.isEquivalence_preRight _ _ _

Equivalence of Precomposition Functors for Structured Arrows

Informal description

For any object $S$ in a category $D$, and functors $F \colon B \to C$ and $G \colon C \to D$, if $F$ is an equivalence of categories, then the precomposition functor $\text{pre}\,S\,F\,G$ from the category of $(F \comp G)$-structured arrows with domain $S$ to the category of $G$-structured arrows with domain $S$ is also an equivalence of categories.

CategoryTheory.StructuredArrow.post definition

(S : C) (F : B ⥤ C) (G : C ⥤ D) : StructuredArrow S F ⥤ StructuredArrow (G.obj S) (F ⋙ G)

Full source

/-- The functor `(S, F) ⥤ (G(S), F ⋙ G)`. -/
@[simps]
def post (S : C) (F : B ⥤ C) (G : C ⥤ D) :
    StructuredArrowStructuredArrow S F ⥤ StructuredArrow (G.obj S) (F ⋙ G) where
  obj X := StructuredArrow.mk (G.map X.hom)
  map f := StructuredArrow.homMk f.right (by simp [Functor.comp_map, ← G.map_comp, ← f.w])

Postcomposition functor for structured arrows

Informal description

Given functors $F \colon B \to C$ and $G \colon C \to D$, and an object $S \colon C$, the functor $\mathrm{post}(S, F, G)$ maps a $F$-structured arrow $X$ with domain $S$ to a $(F \circ G)$-structured arrow with domain $G(S)$. Specifically, it sends an object $(X, f \colon S \to F(X))$ to $(X, G(f) \colon G(S) \to (F \circ G)(X))$, and a morphism $\phi \colon X \to X'$ (which must satisfy $F(\phi) \circ f = f'$) to $\phi$ (which then satisfies $(F \circ G)(\phi) \circ G(f) = G(f')$ by functoriality).

CategoryTheory.StructuredArrow.instFaithfulObjCompPost instance

(S : C) (F : B ⥤ C) (G : C ⥤ D) : (post S F G).Faithful

Full source

instance (S : C) (F : B ⥤ C) (G : C ⥤ D) : (post S F G).Faithful where
  map_injective {_ _} _ _ h := by simpa [ext_iff] using h

Faithfulness of the Postcomposition Functor for Structured Arrows

Informal description

For any object $S$ in a category $C$, and functors $F \colon B \to C$ and $G \colon C \to D$, the postcomposition functor $\mathrm{post}(S, F, G)$ from the category of $F$-structured arrows with domain $S$ to the category of $(F \circ G)$-structured arrows with domain $G(S)$ is faithful. This means that for any two morphisms $\phi, \psi \colon X \to X'$ in the category of $F$-structured arrows, if $\mathrm{post}(S, F, G)(\phi) = \mathrm{post}(S, F, G)(\psi)$, then $\phi = \psi$.

CategoryTheory.StructuredArrow.instFullObjCompPostOfFaithful instance

(S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Faithful] : (post S F G).Full

Full source

instance (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Faithful] : (post S F G).Full where
  map_surjective f := ⟨homMk f.right (G.map_injective (by simpa using f.w.symm)), by simp⟩

Fullness of Postcomposition Functor for Structured Arrows under Faithful Functors

Informal description

For any functors $F \colon B \to C$ and $G \colon C \to D$, and an object $S \colon C$, if $G$ is faithful, then the postcomposition functor $\mathrm{post}(S, F, G) \colon \mathrm{StructuredArrow}\,S\,F \to \mathrm{StructuredArrow}\,(G(S))\,(F \circ G)$ is full.

CategoryTheory.StructuredArrow.instEssSurjObjCompPostOfFull instance

(S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] : (post S F G).EssSurj

Full source

instance (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] : (post S F G).EssSurj where
  mem_essImage h := ⟨mk (G.preimage h.hom), ⟨isoMk (Iso.refl _) (by simp)⟩⟩

Essential Surjectivity of Postcomposition Functor for Full Functors

Informal description

For any functor $G \colon C \to D$ that is full, and any functor $F \colon B \to C$ and object $S \colon C$, the postcomposition functor $\mathrm{post}(S, F, G) \colon \mathrm{StructuredArrow}\,S\,F \to \mathrm{StructuredArrow}\,(G(S))\,(F \circ G)$ is essentially surjective. This means that every object in the target category $\mathrm{StructuredArrow}\,(G(S))\,(F \circ G)$ is isomorphic to an object coming from the source category $\mathrm{StructuredArrow}\,S\,F$ via $\mathrm{post}(S, F, G)$.

CategoryTheory.StructuredArrow.isEquivalence_post instance

(S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] [G.Faithful] : (post S F G).IsEquivalence

Full source

/-- If `G` is fully faithful, then `post S F G : (S, F) ⥤ (G(S), F ⋙ G)` is an equivalence. -/
instance isEquivalence_post (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] [G.Faithful] :
    (post S F G).IsEquivalence where

Equivalence of Structured Arrow Categories under Fully Faithful Functors

Informal description

For any functors $F \colon B \to C$ and $G \colon C \to D$, and an object $S \colon C$, if $G$ is fully faithful, then the postcomposition functor $\mathrm{post}(S, F, G) \colon \mathrm{StructuredArrow}\,S\,F \to \mathrm{StructuredArrow}\,(G(S))\,(F \circ G)$ is an equivalence of categories.

CategoryTheory.StructuredArrow.map₂ definition

: StructuredArrow L R ⥤ StructuredArrow L' R'

Full source

/-- The functor `StructuredArrow L R ⥤ StructuredArrow L' R'` that is deduced from
a natural transformation `R ⋙ G ⟶ F ⋙ R'` and a morphism `L' ⟶ G.obj L.` -/
@[simps!]
def map₂ : StructuredArrowStructuredArrow L R ⥤ StructuredArrow L' R' :=
  Comma.map (F₁ := 𝟭 (Discrete PUnit)) (Discrete.natTrans (fun _ => α)) β

Functor between structured arrow categories induced by a natural transformation and a morphism

Informal description

The functor `StructuredArrow.map₂` transforms a structured arrow category `StructuredArrow L R` into another structured arrow category `StructuredArrow L' R'` using a natural transformation `α : R ⋙ G ⟶ F ⋙ R'` and a morphism `β : L' ⟶ G.obj L`. This functor is constructed by applying the comma category construction to the identity functor on the singleton category, the natural transformation `α`, and the morphism `β`.

CategoryTheory.StructuredArrow.faithful_map₂ instance

[F.Faithful] : (map₂ α β).Faithful

Full source

instance faithful_map₂ [F.Faithful] : (map₂ α β).Faithful := by
  apply Comma.faithful_map

Faithfulness of the Structured Arrow Functor Induced by a Natural Transformation

Informal description

Given a faithful functor $F$, the functor $\text{map}_2(\alpha, \beta)$ between structured arrow categories is faithful.

CategoryTheory.StructuredArrow.full_map₂ instance

[G.Faithful] [F.Full] [IsIso α] [IsIso β] : (map₂ α β).Full

Full source

instance full_map₂ [G.Faithful] [F.Full] [IsIso α] [IsIso β] : (map₂ α β).Full := by
  apply Comma.full_map

Fullness of the Structured Arrow Functor Induced by Isomorphisms and a Faithful Functor

Informal description

Given a natural transformation $\alpha \colon R \circ G \Rightarrow F \circ R'$ and a morphism $\beta \colon L' \to G(L)$ in a category, where $G$ is faithful, $F$ is full, and both $\alpha$ and $\beta$ are isomorphisms, the functor $\text{map}_2(\alpha, \beta) \colon \text{StructuredArrow}(L, R) \to \text{StructuredArrow}(L', R')$ is full. This means that for any two objects $X, Y$ in $\text{StructuredArrow}(L, R)$ and any morphism $f \colon \text{map}_2(\alpha, \beta)(X) \to \text{map}_2(\alpha, \beta)(Y)$ in $\text{StructuredArrow}(L', R')$, there exists a morphism $g \colon X \to Y$ such that $\text{map}_2(\alpha, \beta)(g) = f$.

CategoryTheory.StructuredArrow.essSurj_map₂ instance

[F.EssSurj] [G.Full] [IsIso α] [IsIso β] : (map₂ α β).EssSurj

Full source

instance essSurj_map₂ [F.EssSurj] [G.Full] [IsIso α] [IsIso β] : (map₂ α β).EssSurj := by
  apply Comma.essSurj_map

Essential Surjectivity of the Structured Arrow Functor Induced by Isomorphisms and an Essentially Surjective Functor

Informal description

Given a natural transformation $\alpha \colon R \circ G \Rightarrow F \circ R'$ and a morphism $\beta \colon L' \to G(L)$ in a category, where $F$ is essentially surjective, $G$ is full, and both $\alpha$ and $\beta$ are isomorphisms, the functor $\text{map}_2(\alpha, \beta) \colon \text{StructuredArrow}(L, R) \to \text{StructuredArrow}(L', R')$ is essentially surjective. This means that for every object $Y$ in $\text{StructuredArrow}(L', R')$, there exists an object $X$ in $\text{StructuredArrow}(L, R)$ such that $\text{map}_2(\alpha, \beta)(X)$ is isomorphic to $Y$.

CategoryTheory.StructuredArrow.isEquivalenceMap₂ instance

[F.IsEquivalence] [G.Faithful] [G.Full] [IsIso α] [IsIso β] : (map₂ α β).IsEquivalence

Full source

noncomputable instance isEquivalenceMap₂
    [F.IsEquivalence] [G.Faithful] [G.Full] [IsIso α] [IsIso β] :
    (map₂ α β).IsEquivalence := by
  apply Comma.isEquivalenceMap

Equivalence of Structured Arrow Categories under Isomorphisms and Fully Faithful Functors

Informal description

Given functors $F \colon C \to D$ and $G \colon D' \to D$, a natural isomorphism $\alpha \colon R \circ G \Rightarrow F \circ R'$, and a morphism $\beta \colon L' \to G(L)$ which are both isomorphisms, if $F$ is an equivalence of categories and $G$ is fully faithful, then the functor $\text{map}_2(\alpha, \beta) \colon \text{StructuredArrow}(L, R) \to \text{StructuredArrow}(L', R')$ is an equivalence of categories.

CategoryTheory.StructuredArrow.map₂CompMap₂Iso definition

 {C' : Type u₆} [Category.{v₆} C'] {D' : Type u₅} [Category.{v₅} D'] {L'' : D'} {R'' : C' ⥤ D'} {F' : C' ⥤ C}
  {G' : D' ⥤ D} (α' : L ⟶ G'.obj L'') (β' : R'' ⋙ G' ⟶ F' ⋙ R) :
  map₂ α' β' ⋙ map₂ α β ≅
    map₂ (α ≫ G.map α')
      ((Functor.associator _ _ _).inv ≫
        whiskerRight β' _ ≫ (Functor.associator _ _ _).hom ≫ whiskerLeft _ β ≫ (Functor.associator _ _ _).inv)

Full source

/-- The composition of two applications of `map₂` is naturally isomorphic to a single such one. -/
def map₂CompMap₂Iso {C' : Type u₆} [Category.{v₆} C'] {D' : Type u₅} [Category.{v₅} D']
    {L'' : D'} {R'' : C' ⥤ D'} {F' : C' ⥤ C} {G' : D' ⥤ D} (α' : L ⟶ G'.obj L'')
    (β' : R'' ⋙ G'R'' ⋙ G' ⟶ F' ⋙ R) :
    map₂map₂ α' β' ⋙ map₂ α βmap₂ α' β' ⋙ map₂ α β ≅
    map₂ (α ≫ G.map α')
      ((Functor.associator _ _ _).inv ≫ whiskerRight β' _ ≫ (Functor.associator _ _ _).hom ≫
        whiskerLeft _ β ≫ (Functor.associator _ _ _).inv) :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _))

Natural isomorphism between compositions of structured arrow functors

Informal description

Given categories $C'$ and $D'$, objects $L''$ in $D'$ and $R''$ a functor from $C'$ to $D'$, and functors $F' : C' \to C$ and $G' : D' \to D$, the composition of the functors `map₂ α' β'` and `map₂ α β` is naturally isomorphic to the functor `map₂ (α ≫ G.map α')` applied to a composite natural transformation constructed from $\beta'$ and $\beta$ via whiskering and associator isomorphisms.

CategoryTheory.StructuredArrow.postIsoMap₂ definition

(S : C) (F : B ⥤ C) (G : C ⥤ D) : post S F G ≅ map₂ (F := 𝟭 _) (𝟙 _) (𝟙 (F ⋙ G))

Full source

/-- `StructuredArrow.post` is a special case of `StructuredArrow.map₂` up to natural isomorphism. -/
def postIsoMap₂ (S : C) (F : B ⥤ C) (G : C ⥤ D) :
    postpost S F G ≅ map₂ (F := 𝟭 _) (𝟙 _) (𝟙 (F ⋙ G)) :=
  NatIso.ofComponents fun _ => isoMkisoMk <| Iso.refl _

Natural isomorphism between postcomposition and map₂ functors for structured arrows

Informal description

For a functor $F \colon B \to C$, a functor $G \colon C \to D$, and an object $S \colon C$, the postcomposition functor $\mathrm{post}(S, F, G)$ is naturally isomorphic to the functor $\mathrm{map}_2$ applied to the identity natural transformation on the identity functor and the identity morphism on $F \circ G$. More precisely, the natural isomorphism $\mathrm{postIsoMap}_2(S, F, G)$ provides an isomorphism between the functor $\mathrm{post}(S, F, G)$ and the functor $\mathrm{map}_2$ constructed using the identity natural transformation $\mathbb{1}_{\mathbb{1}_C}$ and the identity morphism $\mathbb{1}_{F \circ G}$. This isomorphism is componentwise given by the identity isomorphism on each object in the structured arrow category.

CategoryTheory.StructuredArrow.mapIsoMap₂ definition

{S S' : D} (f : S ⟶ S') : map (T := T) f ≅ map₂ (F := 𝟭 _) (G := 𝟭 _) f (𝟙 T)

Full source

/-- `StructuredArrow.map` is a special case of `StructuredArrow.map₂` up to natural isomorphism. -/
def mapIsoMap₂ {S S' : D} (f : S ⟶ S') : mapmap (T := T) f ≅ map₂ (F := 𝟭 _) (G := 𝟭 _) f (𝟙 T) :=
  NatIso.ofComponents fun _ => isoMkisoMk <| Iso.refl _

Natural isomorphism between `StructuredArrow.map` and `StructuredArrow.map₂` for identity transformations

Informal description

For any morphism $ f : S \to S' $ in the category $ D $, the functor $ \text{StructuredArrow.map}(f) $ is naturally isomorphic to the functor $ \text{StructuredArrow.map₂} $ applied to the identity natural transformation on the identity functor and the morphism $ f $. More precisely, given a functor $ T : C \to D $, the natural isomorphism $ \text{mapIsoMap₂}(f) $ provides an isomorphism between the functor $ \text{StructuredArrow.map}(f) $ and the functor $ \text{StructuredArrow.map₂} $ constructed using the identity natural transformation $ \mathbb{1}_T $ and the morphism $ f $. This isomorphism is componentwise given by the identity isomorphism on each object in the structured arrow category.

CategoryTheory.StructuredArrow.preIsoMap₂ definition

(S : D) (F : B ⥤ C) (G : C ⥤ D) : pre S F G ≅ map₂ (G := 𝟭 _) (𝟙 _) (𝟙 (F ⋙ G))

Full source

/-- `StructuredArrow.pre` is a special case of `StructuredArrow.map₂` up to natural isomorphism. -/
def preIsoMap₂ (S : D) (F : B ⥤ C) (G : C ⥤ D) :
    prepre S F G ≅ map₂ (G := 𝟭 _) (𝟙 _) (𝟙 (F ⋙ G)) :=
  NatIso.ofComponents fun _ => isoMkisoMk <| Iso.refl _

Natural isomorphism between precomposition and map₂ functors for structured arrows

Informal description

For a functor $F \colon B \to C$, a functor $G \colon C \to D$, and an object $S \colon D$, the precomposition functor $\text{pre}\,S\,F\,G$ from the category of $(F \comp G)$-structured arrows with domain $S$ to the category of $G$-structured arrows with domain $S$ is naturally isomorphic to the functor $\text{map}_2$ applied to the identity natural transformation on $F \comp G$ and the identity morphism on $F \comp G$.

CategoryTheory.StructuredArrow.IsUniversal abbrev

(f : StructuredArrow S T)

Full source

/-- A structured arrow is called universal if it is initial. -/
abbrev IsUniversal (f : StructuredArrow S T) := IsInitial f

Universal Property of a $T$-Structured Arrow

Informal description

A $T$-structured arrow $f \colon S \to T(Y)$ is called *universal* if it is an initial object in the category of $T$-structured arrows with domain $S$.

CategoryTheory.StructuredArrow.IsUniversal.uniq theorem

(h : IsUniversal f) (η : f ⟶ g) : η = h.to g

Full source

theorem uniq (h : IsUniversal f) (η : f ⟶ g) : η = h.to g :=
  h.hom_ext η (h.to g)

Uniqueness of Morphisms from Universal $T$-Structured Arrow

Informal description

Let $f \colon S \to T(Y)$ be a universal $T$-structured arrow (i.e., an initial object in the category of $T$-structured arrows with domain $S$). Then for any morphism $\eta \colon f \to g$ in this category, $\eta$ is equal to the unique morphism from $f$ to $g$ induced by the initiality of $f$.

CategoryTheory.StructuredArrow.IsUniversal.desc definition

(h : IsUniversal f) (g : StructuredArrow S T) : f.right ⟶ g.right

Full source

/-- The family of morphisms out of a universal arrow. -/
def desc (h : IsUniversal f) (g : StructuredArrow S T) : f.right ⟶ g.right :=
  (h.to g).right

Universal morphism induced by a universal structured arrow

Informal description

Given a universal $T$-structured arrow $f \colon S \to T(Y)$ (where $T \colon C \to D$ is a functor and $S \in D$), and another $T$-structured arrow $g \colon S \to T(Y')$, the function returns the unique morphism $Y \to Y'$ in $C$ that makes the diagram commute (i.e., satisfies $f.hom ≫ T.map (desc) = g.hom$).

CategoryTheory.StructuredArrow.IsUniversal.fac theorem

(h : IsUniversal f) (g : StructuredArrow S T) : f.hom ≫ T.map (h.desc g) = g.hom

Full source

/-- Any structured arrow factors through a universal arrow. -/
@[reassoc (attr := simp)]
theorem fac (h : IsUniversal f) (g : StructuredArrow S T) :
    f.hom ≫ T.map (h.desc g) = g.hom :=
  Category.id_comp g.hom ▸ (h.to g).w.symm

Universal Property Factorization for Structured Arrows

Informal description

Let $T \colon C \to D$ be a functor, $S$ an object in $D$, and $f \colon S \to T(Y)$ a universal $T$-structured arrow. Then for any other $T$-structured arrow $g \colon S \to T(Y')$, the composition of $f$ with $T$ applied to the induced morphism $h.desc(g) \colon Y \to Y'$ equals $g$, i.e., the following diagram commutes: $$ f \xrightarrow{\text{hom}} T(Y) \xrightarrow{T(h.desc(g))} T(Y') = g $$

CategoryTheory.StructuredArrow.IsUniversal.hom_desc theorem

(h : IsUniversal f) {c : C} (η : f.right ⟶ c) : η = h.desc (mk <| f.hom ≫ T.map η)

Full source

theorem hom_desc (h : IsUniversal f) {c : C} (η : f.right ⟶ c) :
    η = h.desc (mk <| f.hom ≫ T.map η) :=
  let g := mk <| f.hom ≫ T.map η
  congrArg CommaMorphism.right (h.hom_ext (homMk η rfl : f ⟶ g) (h.to g))

Universal Property of Structured Arrows: Morphism Factorization

Informal description

Given a universal $T$-structured arrow $f \colon S \to T(Y)$ (where $T \colon C \to D$ is a functor and $S \in D$), and a morphism $\eta \colon Y \to c$ in $C$, the morphism $\eta$ is equal to the unique morphism induced by the universal property of $f$ applied to the structured arrow constructed from $f.hom \circ T(\eta)$.

CategoryTheory.StructuredArrow.IsUniversal.hom_ext theorem

(h : IsUniversal f) {c : C} {η η' : f.right ⟶ c} (w : f.hom ≫ T.map η = f.hom ≫ T.map η') : η = η'

Full source

/-- Two morphisms out of a universal `T`-structured arrow are equal if their image under `T` are
equal after precomposing the universal arrow. -/
theorem hom_ext (h : IsUniversal f) {c : C} {η η' : f.right ⟶ c}
    (w : f.hom ≫ T.map η = f.hom ≫ T.map η') : η = η' := by
  rw [h.hom_desc η, h.hom_desc η', w]

Uniqueness of Morphisms from Universal Structured Arrows via Precomposition

Informal description

Let $T \colon C \to D$ be a functor, $S$ an object in $D$, and $f \colon S \to T(Y)$ a universal $T$-structured arrow. For any object $c$ in $C$ and any two morphisms $\eta, \eta' \colon Y \to c$ in $C$, if the compositions $f.hom \circ T(\eta)$ and $f.hom \circ T(\eta')$ are equal, then $\eta = \eta'$.

CategoryTheory.StructuredArrow.IsUniversal.existsUnique theorem

(h : IsUniversal f) (g : StructuredArrow S T) : ∃! η : f.right ⟶ g.right, f.hom ≫ T.map η = g.hom

Full source

theorem existsUnique (h : IsUniversal f) (g : StructuredArrow S T) :
    ∃! η : f.right ⟶ g.right, f.hom ≫ T.map η = g.hom :=
  ⟨h.desc g, h.fac g, fun f w ↦ h.hom_ext <| by simp [w]⟩

Unique Factorization Property of Universal Structured Arrows

Informal description

Let $T \colon C \to D$ be a functor, $S$ an object in $D$, and $f \colon S \to T(Y)$ a universal $T$-structured arrow. Then for any other $T$-structured arrow $g \colon S \to T(Y')$, there exists a unique morphism $\eta \colon Y \to Y'$ in $C$ such that the following diagram commutes: $$ f \xrightarrow{\text{hom}} T(Y) \xrightarrow{T(\eta)} T(Y') = g $$

CategoryTheory.CostructuredArrow definition

(S : C ⥤ D) (T : D)

Full source

/-- The category of `S`-costructured arrows with target `T : D` (here `S : C ⥤ D`),
has as its objects `D`-morphisms of the form `S Y ⟶ T`, for some `Y : C`,
and morphisms `C`-morphisms `Y ⟶ Y'` making the obvious triangle commute.
-/
-- We explicitly come from `PUnit.{1}` here to obtain the correct universe for morphisms of
-- costructured arrows.
def CostructuredArrow (S : C ⥤ D) (T : D) :=
  Comma S (Functor.fromPUnit.{0} T)

Category of $S$-costructured arrows over $T$

Informal description

The category of $S$-costructured arrows with target $T : D$ (where $S : C \to D$ is a functor) has as its objects $D$-morphisms of the form $S(Y) \to T$ for some $Y \in C$, and morphisms are $C$-morphisms $Y \to Y'$ making the obvious triangle commute.

CategoryTheory.instCategoryCostructuredArrow instance

(S : C ⥤ D) (T : D) : Category (CostructuredArrow S T)

Full source

instance (S : C ⥤ D) (T : D) : Category (CostructuredArrow S T) := commaCategory

Category of Costructured Arrows

Informal description

For any functor $S : C \to D$ and object $T : D$, the category of $S$-costructured arrows with target $T$ is a well-defined category. Its objects are morphisms $S(Y) \to T$ for some $Y \in C$, and morphisms are $C$-morphisms $Y \to Y'$ making the obvious triangle commute.

CategoryTheory.CostructuredArrow.proj definition

(S : C ⥤ D) (T : D) : CostructuredArrow S T ⥤ C

Full source

/-- The obvious projection functor from costructured arrows. -/
@[simps!]
def proj (S : C ⥤ D) (T : D) : CostructuredArrowCostructuredArrow S T ⥤ C :=
  Comma.fst _ _

Projection functor from costructured arrows

Informal description

The projection functor from the category of $S$-costructured arrows with target $T$ to the category $C$, which maps each object $(S(Y) \to T)$ to $Y$ and each morphism (a commutative triangle) to its underlying morphism in $C$.

CategoryTheory.CostructuredArrow.hom_ext theorem

{X Y : CostructuredArrow S T} (f g : X ⟶ Y) (h : f.left = g.left) : f = g

Full source

@[ext]
lemma hom_ext {X Y : CostructuredArrow S T} (f g : X ⟶ Y) (h : f.left = g.left) : f = g :=
  CommaMorphism.ext h (Subsingleton.elim _ _)

Equality of Morphisms in Costructured Arrows via Underlying Morphisms

Informal description

For any two morphisms $f, g : X \to Y$ in the category of $S$-costructured arrows over $T$, if the underlying morphisms $f.\mathrm{left}$ and $g.\mathrm{left}$ in $C$ are equal, then $f = g$.

CategoryTheory.CostructuredArrow.hom_eq_iff theorem

{X Y : CostructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.left = g.left

Full source

@[simp]
theorem hom_eq_iff {X Y : CostructuredArrow S T} (f g : X ⟶ Y) : f = g ↔ f.left = g.left :=
  ⟨fun h ↦ by rw [h], hom_ext _ _⟩

Equality of Morphisms in Costructured Arrows via Underlying Morphisms

Informal description

For any two morphisms $f, g \colon X \to Y$ in the category of $S$-costructured arrows over $T$, the equality $f = g$ holds if and only if their underlying morphisms $f.\mathrm{left}$ and $g.\mathrm{left}$ in $C$ are equal.

CategoryTheory.CostructuredArrow.mk definition

(f : S.obj Y ⟶ T) : CostructuredArrow S T

Full source

/-- Construct a costructured arrow from a morphism. -/
def mk (f : S.obj Y ⟶ T) : CostructuredArrow S T :=
  ⟨Y, ⟨⟨⟩⟩, f⟩

Construction of an $S$-costructured arrow over $T$

Informal description

Given a functor $S : C \to D$, an object $Y$ in $C$, and a morphism $f : S(Y) \to T$ in $D$, the function constructs an object in the category of $S$-costructured arrows over $T$, which consists of the object $Y$ and the morphism $f$.

CategoryTheory.CostructuredArrow.mk_left theorem

(f : S.obj Y ⟶ T) : (mk f).left = Y

Full source

@[simp]
theorem mk_left (f : S.obj Y ⟶ T) : (mk f).left = Y :=
  rfl

Left Component of Costructured Arrow Construction is Source Object

Informal description

For any morphism $f \colon S(Y) \to T$ in the category $D$, where $S \colon C \to D$ is a functor and $Y$ is an object in $C$, the left component of the costructured arrow constructed from $f$ is equal to $Y$.

CategoryTheory.CostructuredArrow.mk_right theorem

(f : S.obj Y ⟶ T) : (mk f).right = ⟨⟨⟩⟩

Full source

@[simp]
theorem mk_right (f : S.obj Y ⟶ T) : (mk f).right = ⟨⟨⟩⟩ :=
  rfl

Right Component of Costructured Arrow Construction is Terminal Object

Informal description

Given a functor $S \colon C \to D$, an object $Y$ in $C$, and a morphism $f \colon S(Y) \to T$ in $D$, the right component of the costructured arrow constructed from $f$ is equal to the unique element of the terminal object $\langle \langle \rangle \rangle$ in the discrete category over the singleton type.

CategoryTheory.CostructuredArrow.mk_hom_eq_self theorem

(f : S.obj Y ⟶ T) : (mk f).hom = f

Full source

@[simp]
theorem mk_hom_eq_self (f : S.obj Y ⟶ T) : (mk f).hom = f :=
  rfl

Morphism Component of Costructured Arrow Construction

Informal description

For a functor $S \colon C \to D$, an object $Y$ in $C$, and a morphism $f \colon S(Y) \to T$ in $D$, the morphism component of the costructured arrow constructed from $f$ is equal to $f$ itself.

CategoryTheory.CostructuredArrow.w theorem

{A B : CostructuredArrow S T} (f : A ⟶ B) : S.map f.left ≫ B.hom = A.hom

Full source

@[reassoc]
theorem w {A B : CostructuredArrow S T} (f : A ⟶ B) : S.map f.left ≫ B.hom = A.hom := by simp

Commutativity condition for morphisms in the category of costructured arrows

Informal description

For any morphism $f \colon A \to B$ in the category of $S$-costructured arrows with target $T$, the diagram commutes: $S(f_{\text{left}}) \circ B_{\text{hom}} = A_{\text{hom}}$, where $f_{\text{left}}$ is the underlying morphism in $C$ and $A_{\text{hom}}$, $B_{\text{hom}}$ are the defining morphisms of the objects $A$ and $B$.

CategoryTheory.CostructuredArrow.comp_left theorem

{X Y Z : CostructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).left = f.left ≫ g.left

Full source

@[simp]
theorem comp_left {X Y Z : CostructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).left = f.left ≫ g.left := rfl

Composition of Left Components in Costructured Arrows

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the category of $S$-costructured arrows with target $T$, 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.CostructuredArrow.id_left theorem

(X : CostructuredArrow S T) : (𝟙 X : X ⟶ X).left = 𝟙 X.left

Full source

@[simp]
theorem id_left (X : CostructuredArrow S T) : (𝟙 X : X ⟶ X).left = 𝟙 X.left := rfl

Identity Morphism Preserves Left Component in Costructured Arrows

Informal description

For any object $X$ in the category of $S$-costructured arrows with target $T$, the left component of the identity morphism $\mathrm{id}_X$ is equal to the identity morphism on the left component of $X$, i.e., $(\mathrm{id}_X)_{\mathrm{left}} = \mathrm{id}_{X_{\mathrm{left}}}$.

CategoryTheory.CostructuredArrow.eqToHom_left theorem

{X Y : CostructuredArrow S T} (h : X = Y) : (eqToHom h).left = eqToHom (by rw [h])

Full source

@[simp]
theorem eqToHom_left {X Y : CostructuredArrow S T} (h : X = Y) :
    (eqToHom h).left = eqToHom (by rw [h]) := by
  subst h
  simp only [eqToHom_refl, id_left]

Left Component Preservation of Equality Morphism in Costructured Arrows

Informal description

For any objects $X$ and $Y$ in the category of $S$-costructured arrows with target $T$, and any equality $h : X = Y$ between them, the left component of the morphism $\text{eqToHom}(h)$ is equal to $\text{eqToHom}$ applied to the equality obtained by rewriting with $h$.

CategoryTheory.CostructuredArrow.right_eq_id theorem

{X Y : CostructuredArrow S T} (f : X ⟶ Y) : f.right = 𝟙 X.right

Full source

@[simp]
theorem right_eq_id {X Y : CostructuredArrow S T} (f : X ⟶ Y) : f.right = 𝟙 X.right := rfl

Right Component of Costructured Arrow Morphism is Identity

Informal description

For any morphism $f \colon X \to Y$ in the category of $S$-costructured arrows with target $T$, the right component of $f$ is equal to the identity morphism on $X.\mathrm{right}$, i.e., $f.\mathrm{right} = \mathrm{id}_{X.\mathrm{right}}$.

CategoryTheory.CostructuredArrow.homMk_surjective theorem

 {f f' : CostructuredArrow S T} (φ : f ⟶ f') :
  ∃ (ψ : f.left ⟶ f'.left) (hψ : S.map ψ ≫ f'.hom = f.hom), φ = CostructuredArrow.homMk ψ hψ

Full source

theorem homMk_surjective {f f' : CostructuredArrow S T} (φ : f ⟶ f') :
    ∃ (ψ : f.left ⟶ f'.left) (hψ : S.map ψ ≫ f'.hom = f.hom),
      φ = CostructuredArrow.homMk ψ hψ :=
  ⟨φ.left, CostructuredArrow.w φ, rfl⟩

Surjectivity of Morphism Construction in Costructured Arrows

Informal description

For any morphism $\varphi \colon f \to f'$ in the category of $S$-costructured arrows with target $T$, there exists a morphism $\psi \colon f_{\text{left}} \to f'_{\text{left}}$ in $C$ such that $S(\psi) \circ f'_{\text{hom}} = f_{\text{hom}}$ and $\varphi$ is equal to the morphism constructed from $\psi$ via `CostructuredArrow.homMk`.

CategoryTheory.CostructuredArrow.homMk' definition

(f : CostructuredArrow S T) (g : Y' ⟶ f.left) : mk (S.map g ≫ f.hom) ⟶ f

Full source

/-- Given a costructured arrow `S(Y) ⟶ X`, and an arrow `Y' ⟶ Y'`, we can construct a morphism of
    costructured arrows given by `(S(Y) ⟶ X) ⟶ (S(Y') ⟶ S(Y) ⟶ X)`. -/
@[simps]
def homMk' (f : CostructuredArrow S T) (g : Y' ⟶ f.left) : mkmk (S.map g ≫ f.hom) ⟶ f where
  left := g
  right := 𝟙 _

Morphism of costructured arrows induced by precomposition

Informal description

Given a costructured arrow $f \colon S(Y) \to T$ and a morphism $g \colon Y' \to Y$ in the category $C$, this constructs a morphism of costructured arrows from $(S(Y') \to S(Y) \to T)$ to $(S(Y) \to T)$, where the left component is $g$ and the right component is the identity morphism.

CategoryTheory.CostructuredArrow.homMk'_id theorem

(f : CostructuredArrow S T) : homMk' f (𝟙 f.left) = eqToHom (by aesop_cat)

Full source

lemma homMk'_id (f : CostructuredArrow S T) : homMk' f (𝟙 f.left) = eqToHom (by aesop_cat) := by
  ext
  simp [eqToHom_left]

Identity Morphism Property for $\mathrm{homMk'}$ in Costructured Arrows

Informal description

For any $S$-costructured arrow $f$ with target $T$, the morphism $\mathrm{homMk'}(f, \mathrm{id}_{f.\mathrm{left}})$ is equal to the identity morphism constructed via $\mathrm{eqToHom}$ (using categorical automation).

CategoryTheory.CostructuredArrow.homMk'_mk_id theorem

(f : S.obj Y ⟶ T) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp)

Full source

lemma homMk'_mk_id (f : S.obj Y ⟶ T) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp) :=
  homMk'_id _

Identity Morphism Property for $\mathrm{homMk'}$ Applied to Constructed Costructured Arrows

Informal description

For any morphism $f \colon S(Y) \to T$ in the category $D$, the morphism $\mathrm{homMk'}(\mathrm{mk}(f), \mathrm{id}_Y)$ in the category of $S$-costructured arrows over $T$ is equal to the identity morphism constructed via $\mathrm{eqToHom}$ (using simplification).

CategoryTheory.CostructuredArrow.homMk'_comp theorem

 (f : CostructuredArrow S T) (g : Y' ⟶ f.left) (g' : Y'' ⟶ Y') :
  homMk' f (g' ≫ g) = eqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f.hom)) g' ≫ homMk' f g

Full source

lemma homMk'_comp (f : CostructuredArrow S T) (g : Y' ⟶ f.left) (g' : Y'' ⟶ Y') :
    homMk' f (g' ≫ g) = eqToHomeqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f.hom)) g' ≫ homMk' f g := by
  ext
  simp [eqToHom_left]

Composition Law for Morphisms in the Category of $S$-Costructured Arrows

Informal description

Let $S : C \to D$ be a functor, $T$ an object in $D$, and $f \colon S(Y) \to T$ a morphism in $D$ (viewed as an object in the category of $S$-costructured arrows over $T$). For any morphisms $g \colon Y' \to Y$ and $g' \colon Y'' \to Y'$ in $C$, the morphism $\text{homMk'}(f, g' \circ g)$ in the category of $S$-costructured arrows over $T$ is equal to the composition of: 1. The isomorphism $\text{eqToHom}$ (induced by the equality obtained via simplification), 2. The morphism $\text{homMk'}(\text{mk}(S(g) \circ f), g')$, and 3. The morphism $\text{homMk'}(f, g)$. In other words, the following diagram commutes: \[ \text{homMk'}(f, g' \circ g) = \text{eqToHom}(\text{by simp}) \circ \text{homMk'}(\text{mk}(S(g) \circ f), g') \circ \text{homMk'}(f, g) \]

CategoryTheory.CostructuredArrow.homMk'_mk_comp theorem

 (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
  homMk' (mk f) (g' ≫ g) = eqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f)) g' ≫ homMk' (mk f) g

Full source

lemma homMk'_mk_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
    homMk' (mk f) (g' ≫ g) = eqToHomeqToHom (by simp) ≫ homMk' (mk (S.map g ≫ f)) g' ≫ homMk' (mk f) g :=
  homMk'_comp _ _ _

Composition Law for Morphisms in the Category of $S$-Costructured Arrows

Informal description

Let $S \colon C \to D$ be a functor, $Y$ an object in $C$, and $f \colon S(Y) \to T$ a morphism in $D$. For any morphisms $g \colon Y' \to Y$ and $g' \colon Y'' \to Y'$ in $C$, the following equality holds in the category of $S$-costructured arrows over $T$: \[ \text{homMk'}(\text{mk}(f), g' \circ g) = \text{eqToHom}(\text{by simp}) \circ \text{homMk'}(\text{mk}(S(g) \circ f), g') \circ \text{homMk'}(\text{mk}(f), g) \] where $\text{homMk'}$ constructs a morphism of costructured arrows, $\text{mk}$ constructs an object of costructured arrows, and $\text{eqToHom}$ is the morphism induced by an equality.

CategoryTheory.CostructuredArrow.mkPrecomp definition

(f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : mk (S.map g ≫ f) ⟶ mk f

Full source

/-- Variant of `homMk'` where both objects are applications of `mk`. -/
@[simps]
def mkPrecomp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : mkmk (S.map g ≫ f) ⟶ mk f where
  left := g
  right := 𝟙 _

Precomposition morphism in the category of $S$-costructured arrows over $T$

Informal description

Given a functor $S : C \to D$, an object $Y$ in $C$, a morphism $f : S(Y) \to T$ in $D$, and a morphism $g : Y' \to Y$ in $C$, the function constructs a morphism in the category of $S$-costructured arrows over $T$ from the object $(Y', S(g) \circ f)$ to the object $(Y, f)$. The morphism consists of $g$ on the left component and the identity morphism on the right component.

CategoryTheory.CostructuredArrow.mkPrecomp_id theorem

(f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by simp)

Full source

lemma mkPrecomp_id (f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by simp) := by simp

Identity Precomposition in Costructured Arrows Equals Identity Morphism

Informal description

Given a functor $S \colon C \to D$, an object $Y$ in $C$, and a morphism $f \colon S(Y) \to T$ in $D$, the precomposition morphism $\mathrm{mkPrecomp}(f, \mathrm{id}_Y)$ in the category of $S$-costructured arrows over $T$ is equal to the identity morphism (up to the equality witness $\mathrm{eqToHom}$).

CategoryTheory.CostructuredArrow.mkPrecomp_comp theorem

 (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
  mkPrecomp f (g' ≫ g) = eqToHom (by simp) ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g

Full source

lemma mkPrecomp_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
    mkPrecomp f (g' ≫ g) = eqToHomeqToHom (by simp) ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g := by
  simp

Composition Law for Precomposition Morphisms in Costructured Arrows

Informal description

Given a functor $S : C \to D$, an object $Y$ in $C$, a morphism $f : S(Y) \to T$ in $D$, and morphisms $g : Y' \to Y$ and $g' : Y'' \to Y'$ in $C$, the precomposition morphism $\text{mkPrecomp}(f, g' \circ g)$ in the category of $S$-costructured arrows over $T$ is equal to the composition of the equality morphism $\text{eqToHom}$ (obtained by simplifying the expression) with $\text{mkPrecomp}(S(g) \circ f, g')$ and $\text{mkPrecomp}(f, g)$.

CategoryTheory.CostructuredArrow.ext theorem

{A B : CostructuredArrow S T} (f g : A ⟶ B) (h : f.left = g.left) : f = g

Full source

theorem ext {A B : CostructuredArrow S T} (f g : A ⟶ B) (h : f.left = g.left) : f = g :=
  CommaMorphism.ext h (Subsingleton.elim _ _)

Extensionality of Morphisms in Costructured Arrows Category

Informal description

For any two morphisms $f, g \colon A \to B$ in the category of $S$-costructured arrows over $T$, if the underlying morphisms $f.\mathrm{left}$ and $g.\mathrm{left}$ in $C$ are equal, then $f = g$.

CategoryTheory.CostructuredArrow.ext_iff theorem

{A B : CostructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.left = g.left

Full source

theorem ext_iff {A B : CostructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.left = g.left :=
  ⟨fun h => h ▸ rfl, ext f g⟩

Extensionality of Morphisms in Costructured Arrows Category via Underlying Morphisms

Informal description

For any two morphisms $f, g \colon A \to B$ in the category of $S$-costructured arrows over $T$, $f = g$ if and only if their underlying morphisms $f.\mathrm{left}$ and $g.\mathrm{left}$ in $C$ are equal.

CategoryTheory.CostructuredArrow.proj_faithful instance

: (proj S T).Faithful

Full source

instance proj_faithful : (proj S T).Faithful where map_injective {_ _} := ext

Faithfulness of the Projection Functor from Costructured Arrows

Informal description

The projection functor from the category of $S$-costructured arrows with target $T$ to the category $C$ is faithful. That is, for any two morphisms $f, g \colon A \to B$ in the category of $S$-costructured arrows, if their images under the projection functor are equal in $C$, then $f = g$.

CategoryTheory.CostructuredArrow.mono_of_mono_left theorem

{A B : CostructuredArrow S T} (f : A ⟶ B) [h : Mono f.left] : Mono f

Full source

theorem mono_of_mono_left {A B : CostructuredArrow S T} (f : A ⟶ B) [h : Mono f.left] : Mono f :=
  (proj S T).mono_of_mono_map h

Monomorphism in Costructured Arrows Category Induced by Monomorphism in Base Category

Informal description

Let $S : C \to D$ be a functor and $T$ an object in $D$. For any morphism $f : A \to B$ in the category of $S$-costructured arrows over $T$, if the underlying morphism $f.\mathrm{left} : A.\mathrm{left} \to B.\mathrm{left}$ in $C$ is a monomorphism, then $f$ itself is a monomorphism in the category of $S$-costructured arrows.

CategoryTheory.CostructuredArrow.epi_of_epi_left theorem

{A B : CostructuredArrow S T} (f : A ⟶ B) [h : Epi f.left] : Epi f

Full source

/-- The converse of this is true with additional assumptions, see `epi_iff_epi_left`. -/
theorem epi_of_epi_left {A B : CostructuredArrow S T} (f : A ⟶ B) [h : Epi f.left] : Epi f :=
  (proj S T).epi_of_epi_map h

Epimorphism in Costructured Arrows from Epimorphism in Base Category

Informal description

Let $S : C \to D$ be a functor and $T$ an object in $D$. For any morphism $f : A \to B$ in the category of $S$-costructured arrows over $T$, if the underlying morphism $f.\mathrm{left} : A.\mathrm{left} \to B.\mathrm{left}$ in $C$ is an epimorphism, then $f$ is an epimorphism in the category of $S$-costructured arrows over $T$.

CategoryTheory.CostructuredArrow.mono_homMk instance

{A B : CostructuredArrow S T} (f : A.left ⟶ B.left) (w) [h : Mono f] : Mono (homMk f w)

Full source

instance mono_homMk {A B : CostructuredArrow S T} (f : A.left ⟶ B.left) (w) [h : Mono f] :
    Mono (homMk f w) :=
  (proj S T).mono_of_mono_map h

Monomorphisms in Costructured Arrows Induced by Monomorphisms in the Base Category

Informal description

For any morphism $f \colon A.\mathrm{left} \to B.\mathrm{left}$ in the category $C$ between objects of $S$-costructured arrows with target $T$, if $f$ is a monomorphism in $C$, then the induced morphism $\mathrm{homMk}\,f\,w$ in the category of $S$-costructured arrows is also a monomorphism.

CategoryTheory.CostructuredArrow.epi_homMk instance

{A B : CostructuredArrow S T} (f : A.left ⟶ B.left) (w) [h : Epi f] : Epi (homMk f w)

Full source

instance epi_homMk {A B : CostructuredArrow S T} (f : A.left ⟶ B.left) (w) [h : Epi f] :
    Epi (homMk f w) :=
  (proj S T).epi_of_epi_map h

Epimorphisms in the Category of Costructured Arrows Induced by Epimorphisms in the Base Category

Informal description

Given two objects $A$ and $B$ in the category of $S$-costructured arrows over $T$, and a morphism $f : A.\text{left} \to B.\text{left}$ in $C$ that is an epimorphism, the induced morphism $\text{homMk}(f, w)$ in the category of $S$-costructured arrows is also an epimorphism.

CategoryTheory.CostructuredArrow.eta definition

(f : CostructuredArrow S T) : f ≅ mk f.hom

Full source

/-- Eta rule for costructured arrows. -/
@[simps! hom_left inv_left]
def eta (f : CostructuredArrow S T) : f ≅ mk f.hom :=
  isoMk (Iso.refl _)

Canonical isomorphism between a costructured arrow and its construction from underlying morphism

Informal description

For any object $f$ in the category of $S$-costructured arrows over $T$, there is a canonical isomorphism between $f$ and the object constructed from its underlying morphism $f.hom : S(Y) \to T$ via the `mk` constructor. This isomorphism is given by the identity morphism on the underlying object $Y$ in $C$.

CategoryTheory.CostructuredArrow.mk_surjective theorem

(f : CostructuredArrow S T) : ∃ (Y : C) (g : S.obj Y ⟶ T), f = mk g

Full source

lemma mk_surjective (f : CostructuredArrow S T) :
    ∃ (Y : C) (g : S.obj Y ⟶ T), f = mk g :=
  ⟨_, _, eq_mk f⟩

Surjectivity of Construction for Costructured Arrows

Informal description

For any object $f$ in the category of $S$-costructured arrows over $T$, there exists an object $Y$ in $C$ and a morphism $g : S(Y) \to T$ in $D$ such that $f$ is isomorphic to the object constructed from $g$ via the `mk` function.

CategoryTheory.CostructuredArrow.map definition

(f : T ⟶ T') : CostructuredArrow S T ⥤ CostructuredArrow S T'

Full source

/-- A morphism between target objects `T ⟶ T'`
covariantly induces a functor between costructured arrows,
`CostructuredArrow S T ⥤ CostructuredArrow S T'`.

Ideally this would be described as a 2-functor from `D`
(promoted to a 2-category with equations as 2-morphisms)
to `Cat`.
-/
@[simps!]
def map (f : T ⟶ T') : CostructuredArrowCostructuredArrow S T ⥤ CostructuredArrow S T' :=
  Comma.mapRight _ ((Functor.const _).map f)

Functor induced by morphism on costructured arrows

Informal description

Given a morphism $f : T \to T'$ in category $D$, the functor $\text{map}\,f$ from the category of $S$-costructured arrows with target $T$ to the category of $S$-costructured arrows with target $T'$ is defined by post-composing each structured arrow with $f$. Specifically, it sends an object $(Y, g : S(Y) \to T)$ to $(Y, g \circ f : S(Y) \to T')$.

CategoryTheory.CostructuredArrow.map_mk theorem

{f : S.obj Y ⟶ T} (g : T ⟶ T') : (map g).obj (mk f) = mk (f ≫ g)

Full source

@[simp]
theorem map_mk {f : S.obj Y ⟶ T} (g : T ⟶ T') : (map g).obj (mk f) = mk (f ≫ g) :=
  rfl

Functoriality of Costructured Arrow Construction under Post-Composition

Informal description

Given a morphism $f : S(Y) \to T$ in category $D$ and a morphism $g : T \to T'$ in $D$, the application of the functor $\text{map}\,g$ to the object $\text{mk}\,f$ in the category of $S$-costructured arrows over $T$ yields the object $\text{mk}\,(f \circ g)$ in the category of $S$-costructured arrows over $T'$.

CategoryTheory.CostructuredArrow.map_id theorem

{f : CostructuredArrow S T} : (map (𝟙 T)).obj f = f

Full source

@[simp]
theorem map_id {f : CostructuredArrow S T} : (map (𝟙 T)).obj f = f := by
  rw [eq_mk f]
  simp

Identity Morphism Preserves Costructured Arrows

Informal description

For any object $f$ in the category of $S$-costructured arrows with target $T$, the functor $\text{map}$ applied to the identity morphism $\text{id}_T$ maps $f$ to itself, i.e., $(\text{map}\, \text{id}_T)(f) = f$.

CategoryTheory.CostructuredArrow.map_comp theorem

{f : T ⟶ T'} {f' : T' ⟶ T''} {h : CostructuredArrow S T} : (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)

Full source

@[simp]
theorem map_comp {f : T ⟶ T'} {f' : T' ⟶ T''} {h : CostructuredArrow S T} :
    (map (f ≫ f')).obj h = (map f').obj ((map f).obj h) := by
  rw [eq_mk h]
  simp

Functoriality of Costructured Arrow Mapping under Composition

Informal description

For any morphisms $f \colon T \to T'$ and $f' \colon T' \to T''$ in category $D$, and any object $h$ in the category of $S$-costructured arrows with target $T$, the functor $\text{map}$ satisfies: \[ \text{map}(f \circ f').obj\,h = \text{map}(f').obj\,(\text{map}(f).obj\,h) \]

CategoryTheory.CostructuredArrow.mapIso definition

(i : T ≅ T') : CostructuredArrow S T ≌ CostructuredArrow S T'

Full source

/-- An isomorphism `T ≅ T'` induces an equivalence
    `CostructuredArrow S T ≌ CostructuredArrow S T'`. -/
@[simps!]
def mapIso (i : T ≅ T') : CostructuredArrowCostructuredArrow S T ≌ CostructuredArrow S T' :=
  Comma.mapRightIso _ ((Functor.const _).mapIso i)

Equivalence of costructured arrow categories induced by target isomorphism

Informal description

Given an isomorphism $i \colon T \cong T'$ in category $D$, there is an equivalence of categories between the category of $S$-costructured arrows with target $T$ and the category of $S$-costructured arrows with target $T'$.

CategoryTheory.CostructuredArrow.mapNatIso definition

(i : S ≅ S') : CostructuredArrow S T ≌ CostructuredArrow S' T

Full source

/-- A natural isomorphism `S ≅ S'` induces an equivalence
    `CostrucutredArrow S T ≌ CostructuredArrow S' T`. -/
@[simps!]
def mapNatIso (i : S ≅ S') : CostructuredArrowCostructuredArrow S T ≌ CostructuredArrow S' T :=
  Comma.mapLeftIso _ i

Equivalence of Costructured Arrow Categories Induced by Natural Isomorphism

Informal description

A natural isomorphism $i \colon S \cong S'$ between functors $S, S' \colon C \to D$ induces an equivalence of categories between the category of $S$-costructured arrows with target $T$ and the category of $S'$-costructured arrows with target $T$.

CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms instance

: (proj S T).ReflectsIsomorphisms

Full source

instance proj_reflectsIsomorphisms : (proj S T).ReflectsIsomorphisms where
  reflects {Y Z} f t :=
    ⟨⟨CostructuredArrow.homMk
        (inv ((proj S T).map f))
        (by rw [Functor.map_inv, IsIso.inv_comp_eq]; simp),
      by constructor <;> ext <;> dsimp at t ⊢ <;> simp⟩⟩

Projection Functor Reflects Isomorphisms in Costructured Arrows

Informal description

The projection functor $\mathrm{proj} : \mathrm{CostructuredArrow}\,S\,T \to C$ reflects isomorphisms. That is, if a morphism $f$ in $\mathrm{CostructuredArrow}\,S\,T$ is mapped to an isomorphism in $C$ by $\mathrm{proj}$, then $f$ itself is an isomorphism.

CategoryTheory.CostructuredArrow.mkIdTerminal definition

[S.Full] [S.Faithful] : IsTerminal (mk (𝟙 (S.obj Y)))

Full source

/-- The identity costructured arrow is terminal. -/
noncomputable def mkIdTerminal [S.Full] [S.Faithful] : IsTerminal (mk (𝟙 (S.obj Y))) where
  lift c := homMk (S.preimage c.pt.hom)
  uniq := by
    rintro c m -
    ext
    apply S.map_injective
    simpa only [homMk_left, S.map_preimage, ← w m] using (Category.comp_id _).symm

Terminality of the identity costructured arrow under a fully faithful functor

Informal description

Given a fully faithful functor $S : C \to D$ and an object $Y \in C$, the identity morphism $𝟙 (S(Y))$ in $D$ forms a terminal object in the category of $S$-costructured arrows with target $S(Y)$. More precisely, for any object $(X, f : S(X) \to S(Y))$ in this category, there exists a unique morphism from $(X, f)$ to $(Y, 𝟙 (S(Y)))$ given by the $S$-preimage of $f$ (which exists because $S$ is fully faithful), and this morphism makes the appropriate triangle commute.

CategoryTheory.CostructuredArrow.pre definition

(F : B ⥤ C) (G : C ⥤ D) (S : D) : CostructuredArrow (F ⋙ G) S ⥤ CostructuredArrow G S

Full source

/-- The functor `(F ⋙ G, S) ⥤ (G, S)`. -/
@[simps!]
def pre (F : B ⥤ C) (G : C ⥤ D) (S : D) : CostructuredArrowCostructuredArrow (F ⋙ G) S ⥤ CostructuredArrow G S :=
  Comma.preLeft F G _

Precomposition functor for costructured arrows

Informal description

The functor $\text{pre}(F, G, S)$ maps an object $(Y, f : (F \circ G)(Y) \to S)$ in the category of $(F \circ G)$-costructured arrows over $S$ to the object $(F(Y), f)$ in the category of $G$-costructured arrows over $S$, and similarly for morphisms.

CategoryTheory.CostructuredArrow.instFaithfulCompPre instance

(F : B ⥤ C) (G : C ⥤ D) (S : D) [F.Faithful] : (pre F G S).Faithful

Full source

instance (F : B ⥤ C) (G : C ⥤ D) (S : D) [F.Faithful] : (pre F G S).Faithful :=
  show (Comma.preLeft _ _ _).Faithful from inferInstance

Faithfulness of Precomposition Functor for Costructured Arrows

Informal description

For any faithful functor $F : B \to C$, functor $G : C \to D$, and object $S : D$, the precomposition functor $\text{pre}(F, G, S) : \text{CostructuredArrow}(F \circ G, S) \to \text{CostructuredArrow}(G, S)$ is faithful. This means that for any two morphisms $g_1, g_2$ in $\text{CostructuredArrow}(F \circ G, S)$, if $\text{pre}(F, G, S)(g_1) = \text{pre}(F, G, S)(g_2)$, then $g_1 = g_2$.

CategoryTheory.CostructuredArrow.instFullCompPre instance

(F : B ⥤ C) (G : C ⥤ D) (S : D) [F.Full] : (pre F G S).Full

Full source

instance (F : B ⥤ C) (G : C ⥤ D) (S : D) [F.Full] : (pre F G S).Full :=
  show (Comma.preLeft _ _ _).Full from inferInstance

Fullness of Precomposition Functor for Costructured Arrows

Informal description

For any full functor $F : B \to C$, functor $G : C \to D$, and object $S : D$, the precomposition functor $\text{pre}(F, G, S) : \text{CostructuredArrow}(F \circ G, S) \to \text{CostructuredArrow}(G, S)$ is full. This means that for any two objects $(Y, f)$ and $(Y', f')$ in $\text{CostructuredArrow}(F \circ G, S)$, and any morphism $g : (F(Y), f) \to (F(Y'), f')$ in $\text{CostructuredArrow}(G, S)$, there exists a morphism $h : (Y, f) \to (Y', f')$ in $\text{CostructuredArrow}(F \circ G, S)$ such that $\text{pre}(F, G, S)(h) = g$.

CategoryTheory.CostructuredArrow.instEssSurjCompPre instance

(F : B ⥤ C) (G : C ⥤ D) (S : D) [F.EssSurj] : (pre F G S).EssSurj

Full source

instance (F : B ⥤ C) (G : C ⥤ D) (S : D) [F.EssSurj] : (pre F G S).EssSurj :=
  show (Comma.preLeft _ _ _).EssSurj from inferInstance

Essential Surjectivity of Precomposition Functor for Costructured Arrows

Informal description

For any essentially surjective functor $F \colon B \to C$, the precomposition functor $\text{pre}(F, G, S) \colon \text{CostructuredArrow}(F \circ G, S) \to \text{CostructuredArrow}(G, S)$ is essentially surjective.

CategoryTheory.CostructuredArrow.isEquivalence_pre instance

(F : B ⥤ C) (G : C ⥤ D) (S : D) [F.IsEquivalence] : (pre F G S).IsEquivalence

Full source

/-- If `F` is an equivalence, then so is the functor `(F ⋙ G, S) ⥤ (G, S)`. -/
instance isEquivalence_pre (F : B ⥤ C) (G : C ⥤ D) (S : D) [F.IsEquivalence] :
    (pre F G S).IsEquivalence :=
  Comma.isEquivalence_preLeft _ _ _

Equivalence of Precomposition Functors for Costructured Arrows

Informal description

For any functors $F \colon B \to C$ and $G \colon C \to D$, and object $S \in D$, if $F$ is an equivalence of categories, then the precomposition functor $\text{pre}(F, G, S) \colon \text{CostructuredArrow}(F \circ G, S) \to \text{CostructuredArrow}(G, S)$ is also an equivalence of categories.

CategoryTheory.CostructuredArrow.post definition

(F : B ⥤ C) (G : C ⥤ D) (S : C) : CostructuredArrow F S ⥤ CostructuredArrow (F ⋙ G) (G.obj S)

Full source

/-- The functor `(F, S) ⥤ (F ⋙ G, G(S))`. -/
@[simps]
def post (F : B ⥤ C) (G : C ⥤ D) (S : C) :
    CostructuredArrowCostructuredArrow F S ⥤ CostructuredArrow (F ⋙ G) (G.obj S) where
  obj X := CostructuredArrow.mk (G.map X.hom)
  map f := CostructuredArrow.homMk f.left (by simp [Functor.comp_map, ← G.map_comp, ← f.w])

Postcomposition functor for costructured arrows

Informal description

Given functors $F : B \to C$ and $G : C \to D$, and an object $S : C$, the functor $\text{post}(F, G, S)$ maps an $F$-costructured arrow $X$ over $S$ to the $(F \circ G)$-costructured arrow over $G(S)$ obtained by applying $G$ to the morphism $X.\text{hom}$.

CategoryTheory.CostructuredArrow.instFaithfulCompObjPost instance

(F : B ⥤ C) (G : C ⥤ D) (S : C) : (post F G S).Faithful

Full source

instance (F : B ⥤ C) (G : C ⥤ D) (S : C) : (post F G S).Faithful where
  map_injective {_ _} _ _ h := by simpa [ext_iff] using h

Faithfulness of the Postcomposition Functor for Costructured Arrows

Informal description

For any functors $F \colon B \to C$ and $G \colon C \to D$, and object $S \in C$, the postcomposition functor $\text{post}(F, G, S) \colon \text{CostructuredArrow}(F, S) \to \text{CostructuredArrow}(F \circ G, G(S))$ is faithful. This means that it reflects the equality of morphisms in the category of $F$-costructured arrows over $S$.

CategoryTheory.CostructuredArrow.instFullCompObjPostOfFaithful instance

(F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Faithful] : (post F G S).Full

Full source

instance (F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Faithful] : (post F G S).Full where
  map_surjective f := ⟨homMk f.left (G.map_injective (by simpa using f.w)), by simp⟩

Fullness of Postcomposition Functor for Costructured Arrows with Faithful Functor

Informal description

For any faithful functor $G : C \to D$ and functor $F : B \to C$, the postcomposition functor $\text{post}(F, G, S) : \text{CostructuredArrow}(F, S) \to \text{CostructuredArrow}(F \circ G, G(S))$ is full.

CategoryTheory.CostructuredArrow.instEssSurjCompObjPostOfFull instance

(F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Full] : (post F G S).EssSurj

Full source

instance (F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Full] : (post F G S).EssSurj where
  mem_essImage h := ⟨mk (G.preimage h.hom), ⟨isoMk (Iso.refl _) (by simp)⟩⟩

Essential Surjectivity of Postcomposition Functor for Costructured Arrows under Full Functors

Informal description

For any functors $F \colon B \to C$ and $G \colon C \to D$, and any object $S \in C$, if $G$ is full, then the postcomposition functor $\text{post}(F, G, S) \colon \text{CostructuredArrow}(F, S) \to \text{CostructuredArrow}(F \circ G, G(S))$ is essentially surjective.

CategoryTheory.CostructuredArrow.isEquivalence_post instance

(S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] [G.Faithful] : (post F G S).IsEquivalence

Full source

/-- If `G` is fully faithful, then `post F G S : (F, S) ⥤ (F ⋙ G, G(S))` is an equivalence. -/
instance isEquivalence_post (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] [G.Faithful] :
    (post F G S).IsEquivalence where

Equivalence of Costructured Arrow Categories under Postcomposition with Fully Faithful Functor

Informal description

For any fully faithful functor $G : C \to D$ and functor $F : B \to C$, the postcomposition functor $\text{post}(F, G, S) : \text{CostructuredArrow}(F, S) \to \text{CostructuredArrow}(F \circ G, G(S))$ is an equivalence of categories.

CategoryTheory.CostructuredArrow.map₂ definition

: CostructuredArrow S T ⥤ CostructuredArrow U V

Full source

/-- The functor `CostructuredArrow S T ⥤ CostructuredArrow U V` that is deduced from
a natural transformation `F ⋙ U ⟶ S ⋙ G` and a morphism `G.obj T ⟶ V` -/
@[simps!]
def map₂ : CostructuredArrowCostructuredArrow S T ⥤ CostructuredArrow U V :=
  Comma.map (F₂ := 𝟭 (Discrete PUnit)) α (Discrete.natTrans (fun _ => β))

Functor between costructured arrow categories induced by natural transformation and morphism

Informal description

Given a natural transformation $\alpha \colon F \circ U \Rightarrow S \circ G$ and a morphism $\beta \colon G(T) \to V$, the functor $\text{map}_2$ maps objects and morphisms from the category of $S$-costructured arrows with target $T$ to the category of $U$-costructured arrows with target $V$. Specifically, it sends an object $(Y, f \colon S(Y) \to T)$ to $(Y, \alpha_Y \circ S(f) \circ \beta)$ and a morphism $g \colon Y \to Y'$ to $g$ itself, ensuring the resulting diagram commutes.

CategoryTheory.CostructuredArrow.faithful_map₂ instance

[F.Faithful] : (map₂ α β).Faithful

Full source

instance faithful_map₂ [F.Faithful] : (map₂ α β).Faithful := by
  apply Comma.faithful_map

Faithfulness of the Induced Functor on Costructured Arrows

Informal description

Given a faithful functor $F$, the functor $\text{map}_2$ between categories of costructured arrows is faithful. That is, if two morphisms in the source category are mapped to the same morphism by $\text{map}_2$, then they must be equal.

CategoryTheory.CostructuredArrow.full_map₂ instance

[G.Faithful] [F.Full] [IsIso α] [IsIso β] : (map₂ α β).Full

Full source

instance full_map₂ [G.Faithful] [F.Full] [IsIso α] [IsIso β] : (map₂ α β).Full := by
  apply Comma.full_map

Fullness of the Functor between Costructured Arrow Categories under Isomorphisms

Informal description

Given a natural transformation $\alpha \colon F \circ U \Rightarrow S \circ G$ and a morphism $\beta \colon G(T) \to V$, where $F$ is a full functor, $G$ is a faithful functor, and both $\alpha$ and $\beta$ are isomorphisms, the functor $\text{map}_2 \colon \text{CostructuredArrow}\,S\,T \to \text{CostructuredArrow}\,U\,V$ is full. This means that for any two objects $(Y, f)$ and $(Y', f')$ in $\text{CostructuredArrow}\,S\,T$, and any morphism $g \colon (Y, \alpha_Y \circ S(f) \circ \beta) \to (Y', \alpha_{Y'} \circ S(f') \circ \beta)$ in $\text{CostructuredArrow}\,U\,V$, there exists a morphism $h \colon (Y, f) \to (Y', f')$ in $\text{CostructuredArrow}\,S\,T$ such that $\text{map}_2(h) = g$.

CategoryTheory.CostructuredArrow.essSurj_map₂ instance

[F.EssSurj] [G.Full] [IsIso α] [IsIso β] : (map₂ α β).EssSurj

Full source

instance essSurj_map₂ [F.EssSurj] [G.Full] [IsIso α] [IsIso β] : (map₂ α β).EssSurj := by
  apply Comma.essSurj_map

Essential Surjectivity of the Functor between Costructured Arrow Categories

Informal description

Given a natural transformation $\alpha \colon F \circ U \Rightarrow S \circ G$ and a morphism $\beta \colon G(T) \to V$ where $F$ is essentially surjective, $G$ is full, and both $\alpha$ and $\beta$ are isomorphisms, the functor $\text{map}_2 \colon \text{CostructuredArrow}\,S\,T \to \text{CostructuredArrow}\,U\,V$ is essentially surjective.

CategoryTheory.CostructuredArrow.isEquivalenceMap₂ instance

[F.IsEquivalence] [G.Faithful] [G.Full] [IsIso α] [IsIso β] : (map₂ α β).IsEquivalence

Full source

noncomputable instance isEquivalenceMap₂
    [F.IsEquivalence] [G.Faithful] [G.Full] [IsIso α] [IsIso β] :
    (map₂ α β).IsEquivalence := by
  apply Comma.isEquivalenceMap

Equivalence of Costructured Arrow Categories Induced by Equivalence and Fully Faithful Functor

Informal description

Given functors $F \colon B \to C$ and $G \colon C \to D$, a natural isomorphism $\alpha \colon F \circ U \Rightarrow S \circ G$, and an isomorphism $\beta \colon G(T) \to V$, if $F$ is an equivalence of categories and $G$ is fully faithful, then the functor $\text{map}_2 \colon \text{CostructuredArrow}\,S\,T \to \text{CostructuredArrow}\,U\,V$ induced by $\alpha$ and $\beta$ is also an equivalence of categories.

CategoryTheory.CostructuredArrow.postIsoMap₂ definition

(S : C) (F : B ⥤ C) (G : C ⥤ D) : post F G S ≅ map₂ (F := 𝟭 _) (𝟙 (F ⋙ G)) (𝟙 _)

Full source

/-- `CostructuredArrow.post` is a special case of `CostructuredArrow.map₂` up to natural
isomorphism. -/
def postIsoMap₂ (S : C) (F : B ⥤ C) (G : C ⥤ D) :
    postpost F G S ≅ map₂ (F := 𝟭 _) (𝟙 (F ⋙ G)) (𝟙 _) :=
  NatIso.ofComponents fun _ => isoMkisoMk <| Iso.refl _

Natural isomorphism between postcomposition and map₂ functors for costructured arrows

Informal description

For any object $S$ in category $C$, functors $F : B \to C$ and $G : C \to D$, there is a natural isomorphism between the postcomposition functor $\text{post}(F, G, S)$ and the functor $\text{map}_2$ applied to the identity natural transformation on $F \circ G$ and the identity morphism on $G(S)$. This isomorphism is constructed componentwise using the identity isomorphism in $C$.

CategoryTheory.CostructuredArrow.IsUniversal abbrev

(f : CostructuredArrow S T)

Full source

/-- A costructured arrow is called universal if it is terminal. -/
abbrev IsUniversal (f : CostructuredArrow S T) := IsTerminal f

Universal Property of Costructured Arrows

Informal description

A morphism $f \colon S(Y) \to T$ in the category of $S$-costructured arrows is called *universal* if it is a terminal object in this category. That is, for any other object $g \colon S(Y') \to T$ in the category, there exists a unique morphism $Y' \to Y$ making the obvious triangle commute.

CategoryTheory.CostructuredArrow.IsUniversal.uniq theorem

(h : IsUniversal f) (η : g ⟶ f) : η = h.from g

Full source

theorem uniq (h : IsUniversal f) (η : g ⟶ f) : η = h.from g :=
  h.hom_ext η (h.from g)

Uniqueness of Morphisms to a Universal Costructured Arrow

Informal description

Let $S : C \to D$ be a functor and $T$ an object in $D$. For any universal $S$-costructured arrow $f : S(Y) \to T$ (i.e., $f$ is terminal in the category of $S$-costructured arrows over $T$), and any morphism $\eta : g \to f$ in this category, we have $\eta = \text{from}_h(g)$, where $\text{from}_h(g)$ is the unique morphism from $g$ to $f$ guaranteed by the terminality of $f$.

CategoryTheory.CostructuredArrow.IsUniversal.lift definition

(h : IsUniversal f) (g : CostructuredArrow S T) : g.left ⟶ f.left

Full source

/-- The family of morphisms into a universal arrow. -/
def lift (h : IsUniversal f) (g : CostructuredArrow S T) : g.left ⟶ f.left :=
  (h.from g).left

Lift morphism for universal costructured arrows

Informal description

Given a universal morphism $ f \colon S(Y) \to T $ in the category of $ S $-costructured arrows, and another object $ g \colon S(Y') \to T $ in this category, the morphism $ \text{lift}_h(g) \colon Y' \to Y $ is the unique morphism making the triangle commute, i.e., satisfying $ S(\text{lift}_h(g)) \circ f = g $.

CategoryTheory.CostructuredArrow.IsUniversal.fac theorem

(h : IsUniversal f) (g : CostructuredArrow S T) : S.map (h.lift g) ≫ f.hom = g.hom

Full source

/-- Any costructured arrow factors through a universal arrow. -/
@[reassoc (attr := simp)]
theorem fac (h : IsUniversal f) (g : CostructuredArrow S T) :
    S.map (h.lift g) ≫ f.hom = g.hom :=
  Category.comp_id g.hom ▸ (h.from g).w

Factorization Property of Universal Costructured Arrows

Informal description

Let $S : C \to D$ be a functor and $T$ an object in $D$. Given a universal $S$-costructured arrow $f : S(Y) \to T$ (i.e., $f$ is terminal in the category of $S$-costructured arrows over $T$) and another object $g : S(Y') \to T$ in this category, the composition of $S$ applied to the lift morphism $\text{lift}_h(g) : Y' \to Y$ with $f$ equals $g$, i.e., $S(\text{lift}_h(g)) \circ f = g$.

CategoryTheory.CostructuredArrow.IsUniversal.hom_desc theorem

(h : IsUniversal f) {c : C} (η : c ⟶ f.left) : η = h.lift (mk <| S.map η ≫ f.hom)

Full source

theorem hom_desc (h : IsUniversal f) {c : C} (η : c ⟶ f.left) :
    η = h.lift (mk <| S.map η ≫ f.hom) :=
  let g := mk <| S.map η ≫ f.hom
  congrArg CommaMorphism.left (h.hom_ext (homMk η rfl : g ⟶ f) (h.from g))

Universal Property of Costructured Arrows: Morphism Description

Informal description

Given a universal morphism $f \colon S(Y) \to T$ in the category of $S$-costructured arrows, and any morphism $\eta \colon c \to Y$ in $C$, the morphism $\eta$ is equal to the unique lift of the costructured arrow constructed from the composition $S(\eta) \circ f$.

CategoryTheory.CostructuredArrow.IsUniversal.hom_ext theorem

(h : IsUniversal f) {c : C} {η η' : c ⟶ f.left} (w : S.map η ≫ f.hom = S.map η' ≫ f.hom) : η = η'

Full source

/-- Two morphisms into a universal `S`-costructured arrow are equal if their image under `S` are
equal after postcomposing the universal arrow. -/
theorem hom_ext (h : IsUniversal f) {c : C} {η η' : c ⟶ f.left}
    (w : S.map η ≫ f.hom = S.map η' ≫ f.hom) : η = η' := by
  rw [h.hom_desc η, h.hom_desc η', w]

Uniqueness of Morphisms into Universal Costructured Arrows

Informal description

Let $S : C \to D$ be a functor and $f : S(Y) \to T$ a universal $S$-costructured arrow. For any object $c$ in $C$ and morphisms $\eta, \eta' : c \to Y$, if the compositions $S(\eta) \circ f$ and $S(\eta') \circ f$ are equal in $D$, then $\eta = \eta'$.

CategoryTheory.CostructuredArrow.IsUniversal.existsUnique theorem

(h : IsUniversal f) (g : CostructuredArrow S T) : ∃! η : g.left ⟶ f.left, S.map η ≫ f.hom = g.hom

Full source

theorem existsUnique (h : IsUniversal f) (g : CostructuredArrow S T) :
    ∃! η : g.left ⟶ f.left, S.map η ≫ f.hom = g.hom :=
  ⟨h.lift g, h.fac g, fun f w ↦ h.hom_ext <| by simp [w]⟩

Unique Existence of Morphism into Universal Costructured Arrow

Informal description

Let $S : C \to D$ be a functor and $f : S(Y) \to T$ a universal $S$-costructured arrow. For any other $S$-costructured arrow $g : S(Y') \to T$, there exists a unique morphism $\eta : Y' \to Y$ in $C$ such that the composition $S(\eta) \circ f$ equals $g$.

CategoryTheory.Functor.toStructuredArrow definition

 (G : E ⥤ C) (X : D) (F : C ⥤ D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z) : E ⥤ StructuredArrow X F

Full source

/-- Given `X : D` and `F : C ⥤ D`, to upgrade a functor `G : E ⥤ C` to a functor
    `E ⥤ StructuredArrow X F`, it suffices to provide maps `X ⟶ F.obj (G.obj Y)` for all `Y` making
    the obvious triangles involving all `F.map (G.map g)` commute.

    This is of course the same as providing a cone over `F ⋙ G` with cone point `X`, see
    `Functor.toStructuredArrowIsoToStructuredArrow`. -/
@[simps]
def toStructuredArrow (G : E ⥤ C) (X : D) (F : C ⥤ D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
    (h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z) : E ⥤ StructuredArrow X F where
  obj Y := StructuredArrow.mk (f Y)
  map g := StructuredArrow.homMk (G.map g) (h g)

Functor to category of structured arrows

Informal description

Given a functor $G \colon E \to C$, an object $X \colon D$, and a functor $F \colon C \to D$, along with a family of morphisms $f_Y \colon X \to F(G(Y))$ for each $Y \colon E$ that satisfy the commutativity condition $f_Y \circ F(G(g)) = f_Z$ for any morphism $g \colon Y \to Z$ in $E$, this constructs a functor from $E$ to the category of $F$-structured arrows with domain $X$. The objects are mapped via $f_Y$, and the morphisms are mapped using $G(g)$ while ensuring the commutativity condition holds.

CategoryTheory.Functor.toStructuredArrowCompProj definition

 (G : E ⥤ C) (X : D) (F : C ⥤ D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z) :
  G.toStructuredArrow X F f h ⋙ StructuredArrow.proj _ _ ≅ G

Full source

/-- Upgrading a functor `E ⥤ C` to a functor `E ⥤ StructuredArrow X F` and composing with the
    forgetful functor `StructuredArrow X F ⥤ C` recovers the original functor. -/
def toStructuredArrowCompProj (G : E ⥤ C) (X : D) (F : C ⥤ D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
    (h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z) :
    G.toStructuredArrow X F f h ⋙ StructuredArrow.proj _ _G.toStructuredArrow X F f h ⋙ StructuredArrow.proj _ _ ≅ G :=
  Iso.refl _

Composition of structured arrow functor with projection is isomorphic to original functor

Informal description

Given a functor $G \colon E \to C$, an object $X \colon D$, and a functor $F \colon C \to D$, along with a family of morphisms $f_Y \colon X \to F(G(Y))$ for each $Y \colon E$ that satisfy the commutativity condition $f_Y \circ F(G(g)) = f_Z$ for any morphism $g \colon Y \to Z$ in $E$, the composition of the functor to structured arrows with the projection functor is naturally isomorphic to the original functor $G$.

CategoryTheory.Functor.toStructuredArrow_comp_proj theorem

 (G : E ⥤ C) (X : D) (F : C ⥤ D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z) :
  G.toStructuredArrow X F f h ⋙ StructuredArrow.proj _ _ = G

Full source

@[simp]
lemma toStructuredArrow_comp_proj (G : E ⥤ C) (X : D) (F : C ⥤ D)
    (f : (Y : E) → X ⟶ F.obj (G.obj Y)) (h : ∀ {Y Z : E} (g : Y ⟶ Z), f Y ≫ F.map (G.map g) = f Z) :
    G.toStructuredArrow X F f h ⋙ StructuredArrow.proj _ _ = G :=
  rfl

Equality of Functor Compositions in Structured Arrow Category

Informal description

Given a functor $G \colon E \to C$, an object $X \colon D$, and a functor $F \colon C \to D$, along with a family of morphisms $f_Y \colon X \to F(G(Y))$ for each $Y \colon E$ that satisfy the commutativity condition $f_Y \circ F(G(g)) = f_Z$ for any morphism $g \colon Y \to Z$ in $E$, the composition of the induced functor to the category of $F$-structured arrows with domain $X$ and the projection functor to $C$ is equal to $G$. In other words, the following diagram commutes: \[ \begin{tikzcd} E \arrow[r, "G"] \arrow[rr, bend right, "G.toStructuredArrow\, X\, F\, f\, h \,\circ\, \text{StructuredArrow.proj}\, \_\, \_"] & C \arrow[r, "F"] & D \end{tikzcd} \]

CategoryTheory.Functor.toCostructuredArrow definition

 (G : E ⥤ C) (F : C ⥤ D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) : E ⥤ CostructuredArrow F X

Full source

/-- Given `F : C ⥤ D` and `X : D`, to upgrade a functor `G : E ⥤ C` to a functor
    `E ⥤ CostructuredArrow F X`, it suffices to provide maps `F.obj (G.obj Y) ⟶ X` for all `Y`
    making the obvious triangles involving all `F.map (G.map g)` commute.

    This is of course the same as providing a cocone over `F ⋙ G` with cocone point `X`, see
    `Functor.toCostructuredArrowIsoToCostructuredArrow`. -/
@[simps]
def toCostructuredArrow (G : E ⥤ C) (F : C ⥤ D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
    (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) : E ⥤ CostructuredArrow F X where
  obj Y := CostructuredArrow.mk (f Y)
  map g := CostructuredArrow.homMk (G.map g) (h g)

Functor to category of costructured arrows

Informal description

Given functors $G : E \to C$ and $F : C \to D$, an object $X : D$, and for each $Y \in E$ a morphism $f_Y : F(G(Y)) \to X$ such that for any morphism $g : Y \to Z$ in $E$ the diagram commutes (i.e., $F(G(g)) \circ f_Z = f_Y$), this constructs a functor from $E$ to the category of $F$-costructured arrows over $X$. The functor sends each object $Y$ to the costructured arrow $(G(Y), f_Y)$ and each morphism $g$ to the induced morphism between costructured arrows.

CategoryTheory.Functor.toCostructuredArrowCompProj definition

 (G : E ⥤ C) (F : C ⥤ D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) :
  G.toCostructuredArrow F X f h ⋙ CostructuredArrow.proj _ _ ≅ G

Full source

/-- Upgrading a functor `E ⥤ C` to a functor `E ⥤ CostructuredArrow F X` and composing with the
    forgetful functor `CostructuredArrow F X ⥤ C` recovers the original functor. -/
def toCostructuredArrowCompProj (G : E ⥤ C) (F : C ⥤ D) (X : D)
    (f : (Y : E) → F.obj (G.obj Y) ⟶ X) (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) :
    G.toCostructuredArrow F X f h ⋙ CostructuredArrow.proj _ _G.toCostructuredArrow F X f h ⋙ CostructuredArrow.proj _ _ ≅ G :=
  Iso.refl _

Natural isomorphism between composed functor and original functor in costructured arrows

Informal description

Given functors $G \colon E \to C$ and $F \colon C \to D$, an object $X \colon D$, and for each $Y \in E$ a morphism $f_Y \colon F(G(Y)) \to X$ such that for any morphism $g \colon Y \to Z$ in $E$ the diagram commutes (i.e., $F(G(g)) \circ f_Z = f_Y$), the composition of the induced functor to the category of $F$-costructured arrows over $X$ with the projection functor is naturally isomorphic to $G$. In other words, the diagram: \[ E \xrightarrow{G} C \xrightarrow{F} D \] induces a functor $E \to \mathrm{CostructuredArrow}(F, X)$ whose composition with the projection $\mathrm{CostructuredArrow}(F, X) \to C$ recovers $G$ up to natural isomorphism.

CategoryTheory.Functor.toCostructuredArrow_comp_proj theorem

 (G : E ⥤ C) (F : C ⥤ D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) :
  G.toCostructuredArrow F X f h ⋙ CostructuredArrow.proj _ _ = G

Full source

@[simp]
lemma toCostructuredArrow_comp_proj (G : E ⥤ C) (F : C ⥤ D) (X : D)
    (f : (Y : E) → F.obj (G.obj Y) ⟶ X) (h : ∀ {Y Z : E} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) :
    G.toCostructuredArrow F X f h ⋙ CostructuredArrow.proj _ _ = G :=
rfl

Composition of Induced Functor with Projection Equals Original Functor

Informal description

Given functors $G \colon E \to C$ and $F \colon C \to D$, an object $X \in D$, and for each $Y \in E$ a morphism $f_Y \colon F(G(Y)) \to X$ such that for any morphism $g \colon Y \to Z$ in $E$ the diagram commutes (i.e., $F(G(g)) \circ f_Z = f_Y$), the composition of the induced functor $G.\mathrm{toCostructuredArrow}\,F\,X\,f\,h$ with the projection functor $\mathrm{CostructuredArrow.proj}\,F\,X$ is equal to $G$.

CategoryTheory.StructuredArrow.toCostructuredArrow definition

(F : C ⥤ D) (d : D) : (StructuredArrow d F)ᵒᵖ ⥤ CostructuredArrow F.op (op d)

Full source

/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of structured arrows `d ⟶ F.obj c` to the category of costructured arrows
`F.op.obj c ⟶ (op d)`.
-/
@[simps]
def toCostructuredArrow (F : C ⥤ D) (d : D) :
    (StructuredArrow d F)ᵒᵖ(StructuredArrow d F)ᵒᵖ ⥤ CostructuredArrow F.op (op d) where
  obj X := @CostructuredArrow.mk _ _ _ _ _ (op X.unop.right) F.op X.unop.hom.op
  map f := CostructuredArrow.homMk f.unop.right.op (by simp [← op_comp])

Functor from opposite structured arrows to costructured arrows

Informal description

Given a functor $F \colon C \to D$ and an object $d \colon D$, the functor maps the opposite category of $F$-structured arrows with domain $d$ to the category of $F^{\mathrm{op}}$-costructured arrows over $\mathrm{op}\,d$. Specifically: - On objects: For an object $X$ in $(\mathrm{StructuredArrow}\,d\,F)^{\mathrm{op}}$ (which is a morphism $d \to F(Y)$ in $D$ for some $Y \colon C$), the functor constructs a costructured arrow $\mathrm{CostructuredArrow.mk}\,(F^{\mathrm{op}}(\mathrm{op}\,Y), \mathrm{op}\,(d \to F(Y)))$. - On morphisms: For a morphism $f$ in $(\mathrm{StructuredArrow}\,d\,F)^{\mathrm{op}}$, the functor constructs a morphism in $\mathrm{CostructuredArrow}\,F^{\mathrm{op}}\,(\mathrm{op}\,d)$ using the opposite of the underlying morphism in $C$.

CategoryTheory.StructuredArrow.toCostructuredArrow' definition

(F : C ⥤ D) (d : D) : (StructuredArrow (op d) F.op)ᵒᵖ ⥤ CostructuredArrow F d

Full source

/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of structured arrows `op d ⟶ F.op.obj c` to the category of costructured arrows
`F.obj c ⟶ d`.
-/
@[simps]
def toCostructuredArrow' (F : C ⥤ D) (d : D) :
    (StructuredArrow (op d) F.op)ᵒᵖ(StructuredArrow (op d) F.op)ᵒᵖ ⥤ CostructuredArrow F d where
  obj X := @CostructuredArrow.mk _ _ _ _ _ (unop X.unop.right) F X.unop.hom.unop
  map f :=
    CostructuredArrow.homMk f.unop.right.unop
      (by
        dsimp
        rw [← Quiver.Hom.unop_op (F.map (Quiver.Hom.unop f.unop.right)), ← unop_comp, ← F.op_map, ←
          f.unop.w]
        simp)

Functor from opposite structured arrows to costructured arrows

Informal description

Given a functor $F \colon C \to D$ and an object $d \colon D$, the functor maps an object $(X \colon \text{StructuredArrow}\,(\text{op}\,d)\,F^{\text{op}})^{\text{op}}$ to the costructured arrow $\text{CostructuredArrow.mk}\,(X^{\text{unop}}.\text{hom}^{\text{unop}})$ in the category $\text{CostructuredArrow}\,F\,d$. On morphisms, it sends $f$ to $\text{CostructuredArrow.homMk}\,(f^{\text{unop}}.\text{right}^{\text{unop}})$, ensuring the appropriate diagram commutes.

CategoryTheory.CostructuredArrow.toStructuredArrow definition

(F : C ⥤ D) (d : D) : (CostructuredArrow F d)ᵒᵖ ⥤ StructuredArrow (op d) F.op

Full source

/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of costructured arrows `F.obj c ⟶ d` to the category of structured arrows
`op d ⟶ F.op.obj c`.
-/
@[simps]
def toStructuredArrow (F : C ⥤ D) (d : D) :
    (CostructuredArrow F d)ᵒᵖ(CostructuredArrow F d)ᵒᵖ ⥤ StructuredArrow (op d) F.op where
  obj X := @StructuredArrow.mk _ _ _ _ _ (op X.unop.left) F.op X.unop.hom.op
  map f := StructuredArrow.homMk f.unop.left.op (by simp [← op_comp])

Functor from costructured arrows to structured arrows via opposite categories

Informal description

Given a functor $F \colon C \to D$ and an object $d \in D$, the functor maps an object $(f \colon F(Y) \to d) \in (\mathrm{CostructuredArrow}\, F\, d)^{\mathrm{op}}$ to the structured arrow $(f^{\mathrm{op}} \colon \mathrm{op}\, d \to F^{\mathrm{op}}(Y)) \in \mathrm{StructuredArrow}\, (\mathrm{op}\, d)\, F^{\mathrm{op}}$, and similarly for morphisms.

CategoryTheory.CostructuredArrow.toStructuredArrow' definition

(F : C ⥤ D) (d : D) : (CostructuredArrow F.op (op d))ᵒᵖ ⥤ StructuredArrow d F

Full source

/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of costructured arrows `F.op.obj c ⟶ op d` to the category of structured arrows
`d ⟶ F.obj c`.
-/
@[simps]
def toStructuredArrow' (F : C ⥤ D) (d : D) :
    (CostructuredArrow F.op (op d))ᵒᵖ(CostructuredArrow F.op (op d))ᵒᵖ ⥤ StructuredArrow d F where
  obj X := @StructuredArrow.mk _ _ _ _ _ (unop X.unop.left) F X.unop.hom.unop
  map f :=
    StructuredArrow.homMk f.unop.left.unop
      (by
        dsimp
        rw [← Quiver.Hom.unop_op (F.map f.unop.left.unop), ← unop_comp, ← F.op_map, f.unop.w,
          Functor.const_obj_map]
        simp)

Functor from opposite costructured arrows to structured arrows

Informal description

Given a functor $F \colon C \to D$ and an object $d \colon D$, the functor maps an object $(X \colon \text{CostructuredArrow}\, F^{\text{op}}\, (\text{op}\, d))^{\text{op}}$ to a structured arrow $\text{StructuredArrow.mk}\, (\text{unop}\, X.\text{left})\, F\, (\text{unop}\, X.\text{hom})$. On morphisms, it sends $f$ to $\text{StructuredArrow.homMk}\, (\text{unop}\, f.\text{left})$ with the appropriate commuting condition.

CategoryTheory.structuredArrowOpEquivalence definition

(F : C ⥤ D) (d : D) : (StructuredArrow d F)ᵒᵖ ≌ CostructuredArrow F.op (op d)

Full source

/-- For a functor `F : C ⥤ D` and an object `d : D`, the category of structured arrows `d ⟶ F.obj c`
is contravariantly equivalent to the category of costructured arrows `F.op.obj c ⟶ op d`.
-/
def structuredArrowOpEquivalence (F : C ⥤ D) (d : D) :
    (StructuredArrow d F)ᵒᵖ(StructuredArrow d F)ᵒᵖ ≌ CostructuredArrow F.op (op d) where
  functor := StructuredArrow.toCostructuredArrow F d
  inverse := (CostructuredArrow.toStructuredArrow' F d).rightOp
  unitIso := NatIso.ofComponents
      (fun X => (StructuredArrow.isoMk (Iso.refl _)).op)
      fun {X Y} f => Quiver.Hom.unop_inj <| by
        apply CommaMorphism.ext <;>
          dsimp [StructuredArrow.isoMk, Comma.isoMk,StructuredArrow.homMk]; simp
  counitIso := NatIso.ofComponents
      (fun X => CostructuredArrow.isoMk (Iso.refl _))
      fun {X Y} f => by
        apply CommaMorphism.ext <;>
          dsimp [CostructuredArrow.isoMk, Comma.isoMk, CostructuredArrow.homMk]; simp

Equivalence between opposite structured arrows and costructured arrows

Informal description

For a functor $F \colon C \to D$ and an object $d \in D$, there is an equivalence of categories between the opposite category of $F$-structured arrows with domain $d$ and the category of $F^{\mathrm{op}}$-costructured arrows with target $\mathrm{op}\,d$. Specifically: - The functor from $(\mathrm{StructuredArrow}\,d\,F)^{\mathrm{op}}$ to $\mathrm{CostructuredArrow}\,F^{\mathrm{op}}\,(\mathrm{op}\,d)$ maps a structured arrow $(f \colon d \to F(Y))^{\mathrm{op}}$ to the costructured arrow $F^{\mathrm{op}}(\mathrm{op}\,Y) \to \mathrm{op}\,d$ obtained by applying the opposite functor. - The inverse functor is constructed similarly using the right opposite operation. - The unit and counit isomorphisms are given by identity isomorphisms in the respective categories.

CategoryTheory.costructuredArrowOpEquivalence definition

(F : C ⥤ D) (d : D) : (CostructuredArrow F d)ᵒᵖ ≌ StructuredArrow (op d) F.op

Full source

/-- For a functor `F : C ⥤ D` and an object `d : D`, the category of costructured arrows
`F.obj c ⟶ d` is contravariantly equivalent to the category of structured arrows
`op d ⟶ F.op.obj c`.
-/
def costructuredArrowOpEquivalence (F : C ⥤ D) (d : D) :
    (CostructuredArrow F d)ᵒᵖ(CostructuredArrow F d)ᵒᵖ ≌ StructuredArrow (op d) F.op where
  functor := CostructuredArrow.toStructuredArrow F d
  inverse := (StructuredArrow.toCostructuredArrow' F d).rightOp
  unitIso := NatIso.ofComponents
      (fun X => (CostructuredArrow.isoMk (Iso.refl _)).op)
      fun {X Y} f => Quiver.Hom.unop_inj <| by
        apply CommaMorphism.ext <;>
          dsimp [CostructuredArrow.isoMk, CostructuredArrow.homMk, Comma.isoMk]; simp
  counitIso := NatIso.ofComponents
      (fun X => StructuredArrow.isoMk (Iso.refl _))
      fun {X Y} f => by
        apply CommaMorphism.ext <;>
          dsimp [StructuredArrow.isoMk, StructuredArrow.homMk, Comma.isoMk]; simp

Equivalence between opposite costructured arrows and structured arrows via opposite functor

Informal description

For a functor $F \colon C \to D$ and an object $d \in D$, the opposite category of costructured arrows $(F(Y) \to d)$ is equivalent to the category of structured arrows $(op\, d \to F^{op}(Y))$ via the opposite functor $F^{op} \colon C^{op} \to D^{op}$. The equivalence is established by: 1. A functor mapping $(F(Y) \to d)^{op}$ to $(op\, d \to F^{op}(Y))$, 2. An inverse functor constructed via right opposite, 3. Natural isomorphisms ensuring the equivalence, built from identity isomorphisms on the objects.

CategoryTheory.StructuredArrow.preEquivalenceFunctor definition

(f : StructuredArrow e G) : StructuredArrow f (pre e F G) ⥤ StructuredArrow f.right F

Full source

/-- The functor establishing the equivalence `StructuredArrow.preEquivalence`. -/
@[simps!]
def StructuredArrow.preEquivalenceFunctor (f : StructuredArrow e G) :
    StructuredArrowStructuredArrow f (pre e F G) ⥤ StructuredArrow f.right F where
  obj g := mk g.hom.right
  map φ := homMk φ.right.right <| by
    have := w φ
    simp only [Functor.const_obj_obj] at this ⊢
    rw [← this, comp_right]
    simp

Functor establishing equivalence between structured arrow categories

Informal description

Given a structured arrow $f \colon e \to G(Y)$ and functors $F \colon B \to C$ and $G \colon C \to D$, the functor maps an object $g$ in the category of $(F \comp G)$-structured arrows with domain $e$ to the object $\mathrm{mk}\,g.\mathrm{hom}.\mathrm{right}$ in the category of $F$-structured arrows with domain $Y$. For a morphism $\varphi$ between such objects, it constructs a morphism using $\varphi.\mathrm{right}.\mathrm{right}$ and ensures the necessary diagram commutes.

CategoryTheory.StructuredArrow.preEquivalenceInverse definition

(f : StructuredArrow e G) : StructuredArrow f.right F ⥤ StructuredArrow f (pre e F G)

Full source

/-- The inverse functor establishing the equivalence `StructuredArrow.preEquivalence`. -/
@[simps!]
def StructuredArrow.preEquivalenceInverse (f : StructuredArrow e G) :
    StructuredArrowStructuredArrow f.right F ⥤ StructuredArrow f (pre e F G) where
  obj g := mk
            (Y := mk (Y := g.right)
              (f.hom ≫ (G.map g.hom : G.obj f.right ⟶ (F ⋙ G).obj g.right)))
            (homMk g.hom)
  map φ := homMk <| homMk φ.right <| by
    simp only [Functor.const_obj_obj, Functor.comp_obj, mk_right, mk_left, mk_hom_eq_self,
      Functor.comp_map, Category.assoc, ← w φ, Functor.map_comp]

Inverse functor for precomposition equivalence of structured arrows

Informal description

Given a functor $F \colon B \to C$, a functor $G \colon C \to D$, and a $G$-structured arrow $f \colon e \to G(Y)$ with domain $e \colon D$, the inverse functor $\text{preEquivalenceInverse}$ maps from the category of $F$-structured arrows with domain $Y$ to the category of $(F \comp G)$-structured arrows with domain $e$. Specifically, for any object $g$ in the category of $F$-structured arrows with domain $Y$, the functor constructs a $(F \comp G)$-structured arrow with domain $e$ by composing $f$ with $G(g)$, where $g$ is a morphism $Y \to F(Z)$ for some $Z \colon B$.

CategoryTheory.StructuredArrow.preEquivalence definition

(f : StructuredArrow e G) : StructuredArrow f (pre e F G) ≌ StructuredArrow f.right F

Full source

/-- A structured arrow category on a `StructuredArrow.pre e F G` functor is equivalent to the
structured arrow category on F -/
@[simps]
def StructuredArrow.preEquivalence (f : StructuredArrow e G) :
    StructuredArrowStructuredArrow f (pre e F G) ≌ StructuredArrow f.right F where
  functor := preEquivalenceFunctor F f
  inverse := preEquivalenceInverse F f
  unitIso := NatIso.ofComponents (fun _ => isoMk (isoMk (Iso.refl _)))
  counitIso := NatIso.ofComponents (fun _ => isoMk (Iso.refl _))

Equivalence between precomposed structured arrow categories

Informal description

Given a functor $F \colon B \to C$, a functor $G \colon C \to D$, and a $G$-structured arrow $f \colon e \to G(Y)$ with domain $e \colon D$, there is an equivalence of categories between: 1. The category of $(F \comp G)$-structured arrows with domain $e$ and morphisms over $f$, and 2. The category of $F$-structured arrows with domain $Y$. The equivalence is established by functors that: - Map $(F \comp G)$-structured arrows to $F$-structured arrows via projection to the right component, - Map $F$-structured arrows back to $(F \comp G)$-structured arrows by composition with $f$, with natural isomorphisms given by identity morphisms at each object.

CategoryTheory.StructuredArrow.map₂IsoPreEquivalenceInverseCompProj definition

 {T : C ⥤ D} {S : D ⥤ E} {T' : C ⥤ E} (d : D) (e : E) (u : e ⟶ S.obj d) (α : T ⋙ S ⟶ T') :
  map₂ (F := 𝟭 _) u α ≅ (preEquivalence T (mk u)).inverse ⋙ proj (mk u) (pre _ T S) ⋙ map₂ (F := 𝟭 _) (G := 𝟭 _) (𝟙 _) α

Full source

/-- The functor `StructuredArrow d T ⥤ StructuredArrow e (T ⋙ S)` that `u : e ⟶ S.obj d`
induces via `StructuredArrow.map₂` can be expressed up to isomorphism by
`StructuredArrow.preEquivalence` and `StructuredArrow.proj`. -/
def StructuredArrow.map₂IsoPreEquivalenceInverseCompProj {T : C ⥤ D} {S : D ⥤ E} {T' : C ⥤ E}
    (d : D) (e : E) (u : e ⟶ S.obj d) (α : T ⋙ ST ⋙ S ⟶ T') :
    map₂map₂ (F := 𝟭 _) u α ≅ (preEquivalence T (mk u)).inverse ⋙ proj (mk u) (pre _ T S) ⋙
      map₂ (F := 𝟭 _) (G := 𝟭 _) (𝟙 _) α :=
  NatIso.ofComponents fun _ => isoMk (Iso.refl _)

Natural isomorphism between structured arrow functors via precomposition equivalence

Informal description

Given functors $T \colon C \to D$, $S \colon D \to E$, and $T' \colon C \to E$, along with a morphism $u \colon e \to S(d)$ in $E$ and a natural transformation $\alpha \colon T \circ S \to T'$, there is a natural isomorphism between: 1. The functor $\text{map}_2$ applied to $u$ and $\alpha$ (with identity functors as parameters), and 2. The composition of: - The inverse of the precomposition equivalence for $T$ at the structured arrow $\text{mk}(u)$, - The projection functor from structured arrows over $\text{mk}(u)$ with precomposition by $T$ and $S$, - The functor $\text{map}_2$ applied to the identity morphism and $\alpha$ (again with identity functors as parameters). This isomorphism is constructed componentwise using identity isomorphisms.

CategoryTheory.CostructuredArrow.preEquivalence.functor definition

(f : CostructuredArrow G e) : CostructuredArrow (pre F G e) f ⥤ CostructuredArrow F f.left

Full source

/-- The functor establishing the equivalence `CostructuredArrow.preEquivalence`. -/
@[simps!]
def CostructuredArrow.preEquivalence.functor (f : CostructuredArrow G e) :
    CostructuredArrowCostructuredArrow (pre F G e) f ⥤ CostructuredArrow F f.left where
  obj g := mk g.hom.left
  map φ := homMk φ.left.left <| by
    have := w φ
    simp only [Functor.const_obj_obj] at this ⊢
    rw [← this, comp_left]
    simp

Functor from $(F \circ G)$-costructured arrows to $F$-costructured arrows over $f.\text{left}$

Informal description

Given a functor $G : C \to D$, an object $e : D$, and an object $f$ in the category of $G$-costructured arrows over $e$, the functor maps an object $g$ in the category of $(F \circ G)$-costructured arrows over $f$ to an object in the category of $F$-costructured arrows over $f.\text{left}$, where $F : B \to C$ is another functor. The mapping is defined by sending $g$ to the object constructed from the left component of the morphism $g.\text{hom}$.

CategoryTheory.CostructuredArrow.preEquivalence.inverse definition

(f : CostructuredArrow G e) : CostructuredArrow F f.left ⥤ CostructuredArrow (pre F G e) f

Full source

/-- The inverse functor establishing the equivalence `CostructuredArrow.preEquivalence`. -/
@[simps!]
def CostructuredArrow.preEquivalence.inverse (f : CostructuredArrow G e) :
    CostructuredArrowCostructuredArrow F f.left ⥤ CostructuredArrow (pre F G e) f where
  obj g := mk (Y := mk (Y := g.left) (G.map g.hom ≫ f.hom)) (homMk g.hom)
  map φ := homMk <| homMk φ.left <| by
    simp only [Functor.const_obj_obj, Functor.comp_obj, mk_left, Functor.comp_map, mk_hom_eq_self,
      ← w φ, Functor.map_comp, Category.assoc]

Inverse functor of the precomposition equivalence for costructured arrows

Informal description

Given a functor $F : B \to C$, a functor $G : C \to D$, an object $e : D$, and an object $f$ in the category of $G$-costructured arrows over $e$, the inverse functor of the equivalence `CostructuredArrow.preEquivalence` maps an object $(Y, g : F(Y) \to f.\text{left})$ in the category of $F$-costructured arrows over $f.\text{left}$ to the object $(Y, G(g) \circ f.\text{hom})$ in the category of $(F \circ G)$-costructured arrows over $e$. Here, $f.\text{left}$ denotes the source object of the morphism $f.\text{hom} : G(f.\text{left}) \to e$ in $D$, and $f.\text{hom}$ is the morphism itself. The functor also maps morphisms in a compatible way, ensuring the appropriate diagrams commute.

CategoryTheory.CostructuredArrow.preEquivalence definition

(f : CostructuredArrow G e) : CostructuredArrow (pre F G e) f ≌ CostructuredArrow F f.left

Full source

/-- A costructured arrow category on a `CostructuredArrow.pre F G e` functor is equivalent to the
costructured arrow category on F -/
def CostructuredArrow.preEquivalence (f : CostructuredArrow G e) :
    CostructuredArrowCostructuredArrow (pre F G e) f ≌ CostructuredArrow F f.left where
  functor := preEquivalence.functor F f
  inverse := preEquivalence.inverse F f
  unitIso := NatIso.ofComponents (fun _ => isoMk (isoMk (Iso.refl _)))
  counitIso := NatIso.ofComponents (fun _ => isoMk (Iso.refl _))

Equivalence between $(F \circ G)$-costructured arrows and $F$-costructured arrows over $f.\text{left}$

Informal description

Given a functor $F : B \to C$, a functor $G : C \to D$, an object $e : D$, and an object $f$ in the category of $G$-costructured arrows over $e$, there is an equivalence of categories between the category of $(F \circ G)$-costructured arrows over $f$ and the category of $F$-costructured arrows over $f.\text{left}$. Here, $f.\text{left}$ denotes the source object of the morphism $f.\text{hom} : G(f.\text{left}) \to e$ in $D$. The equivalence is constructed via: - A functor that maps $(Y, g : (F \circ G)(Y) \to e)$ to $(Y, g)$ in the $F$-costructured arrow category over $f.\text{left}$. - An inverse functor that maps $(Y, h : F(Y) \to f.\text{left})$ to $(Y, G(h) \circ f.\text{hom})$. - Natural isomorphisms witnessing the equivalence, built from identity isomorphisms.

CategoryTheory.CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj definition

 (T : C ⥤ D) (S : D ⥤ E) (d : D) (e : E) (u : S.obj d ⟶ e) :
  map₂ (F := 𝟭 _) (U := T ⋙ S) (𝟙 (T ⋙ S)) u ≅ (preEquivalence T (mk u)).inverse ⋙ proj (pre T S _) (mk u)

Full source

/-- The functor `CostructuredArrow T d ⥤ CostructuredArrow (T ⋙ S) e` that `u : S.obj d ⟶ e`
induces via `CostructuredArrow.map₂` can be expressed up to isomorphism by
`CostructuredArrow.preEquivalence` and `CostructuredArrow.proj`. -/
def CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj (T : C ⥤ D) (S : D ⥤ E) (d : D) (e : E)
    (u : S.obj d ⟶ e) :
    map₂map₂ (F := 𝟭 _) (U := T ⋙ S) (𝟙 (T ⋙ S)) u ≅
      (preEquivalence T (mk u)).inverse ⋙ proj (pre T S _) (mk u) :=
  NatIso.ofComponents fun _ => isoMk (Iso.refl _)

Natural isomorphism between map₂ and precomposition equivalence for costructured arrows

Informal description

Given functors $T : C \to D$ and $S : D \to E$, objects $d \in D$ and $e \in E$, and a morphism $u : S(d) \to e$, there is a natural isomorphism between: 1. The functor obtained by applying $\text{map}_2$ to the identity natural transformation on $T \circ S$ and the morphism $u$, and 2. The composition of the inverse functor of the precomposition equivalence for $T$ at $\text{mk}(u)$ with the projection functor from $(T \circ S)$-costructured arrows over $\text{mk}(u)$. This isomorphism is constructed componentwise using the identity isomorphism.

CategoryTheory.StructuredArrow.w_prod_fst theorem

{X Y : StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y) : X.hom.1 ≫ T.map f.right.1 = Y.hom.1

Full source

@[reassoc (attr := simp)]
theorem StructuredArrow.w_prod_fst {X Y : StructuredArrow (S, S') (T.prod T')}
    (f : X ⟶ Y) : X.hom.1 ≫ T.map f.right.1 = Y.hom.1 :=
  congr_arg _root_.Prod.fst (StructuredArrow.w f)

Commutativity of First Component in Product of Structured Arrows

Informal description

For any objects $X$ and $Y$ in the category of $(T \times T')$-structured arrows with domain $(S, S')$, and any morphism $f \colon X \to Y$, the first component of the structured arrow commutes in the sense that $X.\text{hom}_1 \circ T(f.\text{right}_1) = Y.\text{hom}_1$, where $\text{hom}_1$ and $\text{right}_1$ denote the first projections of the respective morphisms.

CategoryTheory.StructuredArrow.w_prod_snd theorem

{X Y : StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y) : X.hom.2 ≫ T'.map f.right.2 = Y.hom.2

Full source

@[reassoc (attr := simp)]
theorem StructuredArrow.w_prod_snd {X Y : StructuredArrow (S, S') (T.prod T')}
    (f : X ⟶ Y) : X.hom.2 ≫ T'.map f.right.2 = Y.hom.2 :=
  congr_arg _root_.Prod.snd (StructuredArrow.w f)

Commutativity of Second Component in Product Structured Arrows

Informal description

For any two objects $X$ and $Y$ in the category of $(T \times T')$-structured arrows with domain $(S, S')$, and any morphism $f \colon X \to Y$, the second component of the structured arrow commutes, i.e., $X.\text{hom}_2 \circ T'(f.\text{right}_2) = Y.\text{hom}_2$.

CategoryTheory.StructuredArrow.prodFunctor definition

: StructuredArrow (S, S') (T.prod T') ⥤ StructuredArrow S T × StructuredArrow S' T'

Full source

/-- Implementation; see `StructuredArrow.prodEquivalence`. -/
@[simps]
def StructuredArrow.prodFunctor :
    StructuredArrowStructuredArrow (S, S') (T.prod T') ⥤ StructuredArrow S T × StructuredArrow S' T' where
  obj f := ⟨.mk f.hom.1, .mk f.hom.2⟩
  map η := ⟨StructuredArrow.homMk η.right.1 (by simp),
            StructuredArrow.homMk η.right.2 (by simp)⟩

Product functor for structured arrows

Informal description

The functor that maps an object $(f_1, f_2)$ in the category of $(T \times T')$-structured arrows with domain $(S, S')$ to the pair of objects $(f_1, f_2)$ in the product category of $T$-structured arrows with domain $S$ and $T'$-structured arrows with domain $S'$. On morphisms, it maps a morphism $\eta$ to the pair of morphisms $(\eta_1, \eta_2)$, where $\eta_1$ and $\eta_2$ are the components of $\eta$ in the respective structured arrow categories.

CategoryTheory.StructuredArrow.prodInverse definition

: StructuredArrow S T × StructuredArrow S' T' ⥤ StructuredArrow (S, S') (T.prod T')

Full source

/-- Implementation; see `StructuredArrow.prodEquivalence`. -/
@[simps]
def StructuredArrow.prodInverse :
    StructuredArrowStructuredArrow S T × StructuredArrow S' T'StructuredArrow S T × StructuredArrow S' T' ⥤ StructuredArrow (S, S') (T.prod T') where
  obj f := .mk (Y := (f.1.right, f.2.right)) ⟨f.1.hom, f.2.hom⟩
  map η := StructuredArrow.homMk ⟨η.1.right, η.2.right⟩ (by simp)

Inverse functor for product of structured arrows

Informal description

The functor $\text{prodInverse}$ maps a pair of $T$-structured arrows $(f_1 \colon S \to T(Y_1), f_2 \colon S' \to T'(Y_2))$ to a single structured arrow $(f_1, f_2) \colon (S, S') \to (T \times T')(Y_1, Y_2)$ in the product category. On morphisms, it maps a pair of morphisms $(\eta_1 \colon Y_1 \to Y_1', \eta_2 \colon Y_2 \to Y_2')$ to the morphism $(\eta_1, \eta_2) \colon (Y_1, Y_2) \to (Y_1', Y_2')$ in the product category, ensuring the obvious diagram commutes.

CategoryTheory.StructuredArrow.prodEquivalence definition

: StructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T'

Full source

/-- The natural equivalence
`StructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T'`. -/
@[simps]
def StructuredArrow.prodEquivalence :
    StructuredArrowStructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T' where
  functor := StructuredArrow.prodFunctor S S' T T'
  inverse := StructuredArrow.prodInverse S S' T T'
  unitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)

Equivalence between product of structured arrows and structured arrows of products

Informal description

The natural equivalence between the category of $(T \times T')$-structured arrows with domain $(S, S')$ and the product category of $T$-structured arrows with domain $S$ and $T'$-structured arrows with domain $S'$. This equivalence is given by: - The functor $\text{prodFunctor}$ which decomposes a structured arrow $(f_1, f_2) \colon (S, S') \to (T \times T')(Y_1, Y_2)$ into a pair of structured arrows $(f_1 \colon S \to T(Y_1), f_2 \colon S' \to T'(Y_2))$. - The inverse functor $\text{prodInverse}$ which combines a pair of structured arrows into a single structured arrow in the product category. - The unit and counit isomorphisms are both identity isomorphisms, ensuring the equivalence is naturally isomorphic to the identity functors.

CategoryTheory.CostructuredArrow.w_prod_fst theorem

{A B : CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) : S.map f.left.1 ≫ B.hom.1 = A.hom.1

Full source

@[reassoc (attr := simp)]
theorem CostructuredArrow.w_prod_fst {A B : CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) :
    S.map f.left.1 ≫ B.hom.1 = A.hom.1 :=
  congr_arg _root_.Prod.fst (CostructuredArrow.w f)

Commutativity of First Component in Product of Costructured Arrows

Informal description

For any morphism $f \colon A \to B$ in the category of $(S \times S')$-costructured arrows with target $(T, T')$, the first component of the defining morphisms satisfies the commutativity condition: $S(f_{\text{left},1}) \circ B_{\text{hom},1} = A_{\text{hom},1}$, where $f_{\text{left},1}$ is the first component of the underlying morphism in $C \times C'$, and $A_{\text{hom},1}$, $B_{\text{hom},1}$ are the first components of the defining morphisms of $A$ and $B$.

CategoryTheory.CostructuredArrow.w_prod_snd theorem

{A B : CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) : S'.map f.left.2 ≫ B.hom.2 = A.hom.2

Full source

@[reassoc (attr := simp)]
theorem CostructuredArrow.w_prod_snd {A B : CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) :
    S'.map f.left.2 ≫ B.hom.2 = A.hom.2 :=
  congr_arg _root_.Prod.snd (CostructuredArrow.w f)

Commutativity of Second Component in Product Costructured Arrows

Informal description

For any morphism $f \colon A \to B$ in the category of $(S \times S')$-costructured arrows with target $(T, T')$, the second component of the diagram commutes: $S'(f_{\text{left},2}) \circ B_{\text{hom},2} = A_{\text{hom},2}$, where $f_{\text{left},2}$ is the second component of the underlying morphism in $C \times C'$ and $A_{\text{hom},2}$, $B_{\text{hom},2}$ are the second components of the defining morphisms of the objects $A$ and $B$.

CategoryTheory.CostructuredArrow.prodFunctor definition

: CostructuredArrow (S.prod S') (T, T') ⥤ CostructuredArrow S T × CostructuredArrow S' T'

Full source

/-- Implementation; see `CostructuredArrow.prodEquivalence`. -/
@[simps]
def CostructuredArrow.prodFunctor :
    CostructuredArrowCostructuredArrow (S.prod S') (T, T') ⥤ CostructuredArrow S T × CostructuredArrow S' T' where
  obj f := ⟨.mk f.hom.1, .mk f.hom.2⟩
  map η := ⟨CostructuredArrow.homMk η.left.1 (by simp),
            CostructuredArrow.homMk η.left.2 (by simp)⟩

Product functor for costructured arrows

Informal description

The functor that maps an object in the category of $(S \times S')$-costructured arrows over $(T, T')$ to the product of objects in the categories of $S$-costructured arrows over $T$ and $S'$-costructured arrows over $T'$. Specifically, for an object $f$ in $\mathrm{CostructuredArrow}(S \times S', (T, T'))$, the functor sends $f$ to the pair $(\mathrm{mk}(f.\hom_1), \mathrm{mk}(f.\hom_2))$, where $\mathrm{mk}$ constructs the corresponding costructured arrow. For a morphism $\eta$, the functor sends it to the pair of morphisms $(\mathrm{homMk}(\eta.\mathrm{left}_1), \mathrm{homMk}(\eta.\mathrm{left}_2))$, where $\mathrm{homMk}$ constructs the corresponding morphism in the costructured arrow category.

CategoryTheory.CostructuredArrow.prodInverse definition

: CostructuredArrow S T × CostructuredArrow S' T' ⥤ CostructuredArrow (S.prod S') (T, T')

Full source

/-- Implementation; see `CostructuredArrow.prodEquivalence`. -/
@[simps]
def CostructuredArrow.prodInverse :
    CostructuredArrowCostructuredArrow S T × CostructuredArrow S' T'CostructuredArrow S T × CostructuredArrow S' T' ⥤ CostructuredArrow (S.prod S') (T, T') where
  obj f := .mk (Y := (f.1.left, f.2.left)) ⟨f.1.hom, f.2.hom⟩
  map η := CostructuredArrow.homMk ⟨η.1.left, η.2.left⟩ (by simp)

Inverse functor for product of costructured arrows

Informal description

The functor that maps a pair of $S$-costructured arrows over $T$ and $S'$-costructured arrows over $T'$ to an $(S \times S')$-costructured arrow over $(T, T')$. Specifically, given objects $(f_1 : S(Y_1) \to T, f_2 : S'(Y_2) \to T')$ in the product category $\mathrm{CostructuredArrow}\,S\,T \times \mathrm{CostructuredArrow}\,S'\,T'$, it constructs an object in $\mathrm{CostructuredArrow}\,(S \times S')\,(T, T')$ consisting of the pair $(Y_1, Y_2)$ and the morphism $(f_1, f_2) : (S(Y_1), S'(Y_2)) \to (T, T')$.

CategoryTheory.CostructuredArrow.prodEquivalence definition

: CostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T'

Full source

/-- The natural equivalence
`CostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T'`. -/
@[simps]
def CostructuredArrow.prodEquivalence :
    CostructuredArrowCostructuredArrow (S.prod S') (T, T') ≌ CostructuredArrow S T × CostructuredArrow S' T' where
  functor := CostructuredArrow.prodFunctor S S' T T'
  inverse := CostructuredArrow.prodInverse S S' T T'
  unitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)

Equivalence between product of costructured arrow categories

Informal description

The natural equivalence between the category of $(S \times S')$-costructured arrows over $(T, T')$ and the product of categories of $S$-costructured arrows over $T$ and $S'$-costructured arrows over $T'$. More precisely, this equivalence is constructed via: 1. A functor that decomposes an $(S \times S')$-costructured arrow into a pair of $S$- and $S'$-costructured arrows. 2. An inverse functor that combines a pair of $S$- and $S'$-costructured arrows back into an $(S \times S')$-costructured arrow. 3. Natural isomorphisms witnessing the equivalence, both given by identity isomorphisms at each component.