Documentation

Mathlib.CategoryTheory.MorphismProperty.Representable

Relatively representable morphisms #

In this file we define and develop basic results about relatively representable morphisms.

Classically, a morphism f : X ⟶ Y of presheaves is said to be representable if for any morphism g : yoneda.obj X ⟶ G, there exists a pullback square of the following form

  yoneda.obj Y --yoneda.map snd--> yoneda.obj X
      |                                |
     fst                               g
      |                                |
      v                                v
      F ------------ f --------------> G

In this file, we define a notion of relative representability which works with respect to any functor, and not just yoneda. The fact that a morphism f : F ⟶ G between presheaves is representable in the classical case will then be given by yoneda.relativelyRepresentable f.

Main definitions #

Throughout this file, F : C ⥤ D is a functor between categories C and D.

We define relativelyRepresentable as a MorphismProperty. A morphism f : X ⟶ Y in D is said to be relatively representable with respect to F, if for any g : F.obj a ⟶ Y, there exists a pullback square of the following form

  F.obj b --F.map snd--> F.obj a
      |                     |
     fst                    g
      |                     |
      v                     v
      X ------- f --------> Y

API #

Given hf : relativelyRepresentable f, with f : X ⟶ Y and g : F.obj a ⟶ Y, we provide:

hf.pullback g which is the object in C such that F.obj (hf.pullback g) is a pullback of f and g.
hf.snd g is the morphism hf.pullback g ⟶ F.obj a
hf.fst g is the morphism F.obj (hf.pullback g) ⟶ X
If F is full, and f is of type F.obj c ⟶ G, we also have hf.fst' g : hf.pullback g ⟶ X which is the preimage under F of hf.fst g.
hom_ext, hom_ext', lift, lift' are variants of the universal property of F.obj (hf.pullback g), where as much as possible has been formulated internally to C. For these theorems we also need that F is full and/or faithful.
symmetry and symmetryIso are variants of the fact that pullbacks are symmetric for representable morphisms, formulated internally to C. We assume that F is fully faithful here.

Main results #

relativelyRepresentable.isMultiplicative: The class of relatively representable morphisms is multiplicative.
relativelyRepresentable.stableUnderBaseChange: Being relatively representable is stable under base change.
relativelyRepresentable.of_isIso: Isomorphisms are relatively representable.

def CategoryTheory.Functor.relativelyRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

CategoryTheory.MorphismProperty D

A morphism f : X ⟶ Y in D is said to be relatively representable if for any g : F.obj a ⟶ Y, there exists a pullback square of the following form

F.obj b --F.map snd--> F.obj a
    |                     |
   fst                    g
    |                     |
    v                     v
    X ------- f --------> Y

Equations

F.relativelyRepresentable f = ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), CategoryTheory.IsPullback fst (F.map snd) f g

Instances For

noncomputable def CategoryTheory.Functor.relativelyRepresentable.pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y) :

C

Let f : X ⟶ Y be a relatively representable morphism in D. Then, for any g : F.obj a ⟶ Y, hf.pullback g denotes the (choice of) a corresponding object in C such that there is a pullback square of the following form

hf.pullback g --F.map snd--> F.obj a
    |                          |
   fst                         g
    |                          |
    v                          v
    X ---------- f ----------> Y

Equations

hf.pullback g = ⋯.choose

Instances For

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.relativelyRepresentable.snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y) :

hf.pullback g ⟶ a

Given a representable morphism f : X ⟶ Y, then for any g : F.obj a ⟶ Y, hf.snd g denotes the morphism in C giving rise to the following diagram

hf.pullback g --F.map (hf.snd g)--> F.obj a
    |                                 |
   fst                                g
    |                                 |
    v                                 v
    X -------------- f -------------> Y

Equations

hf.snd g = ⋯.choose

Instances For

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.relativelyRepresentable.fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y) :

F.obj (hf.pullback g) ⟶ X

Given a relatively representable morphism f : X ⟶ Y, then for any g : F.obj a ⟶ Y, hf.fst g denotes the first projection in the following diagram, given by the defining property of f being relatively representable

hf.pullback g --F.map (hf.snd g)--> F.obj a
    |                                 |
hf.fst g                              g
    |                                 |
    v                                 v
    X -------------- f -------------> Y

Equations

hf.fst g = ⋯.choose

Instances For

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.relativelyRepresentable.fst' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} (g : F.obj a ⟶ Y) [F.Full] :

hf'.pullback g ⟶ b

When F is full, given a representable morphism f' : F.obj b ⟶ Y, then hf'.fst' g denotes the preimage of hf'.fst g under F.

Equations

hf'.fst' g = F.preimage (hf'.fst g)

Instances For

theorem CategoryTheory.Functor.relativelyRepresentable.map_fst' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} (g : F.obj a ⟶ Y) [F.Full] :

F.map (hf'.fst' g) = hf'.fst g

theorem CategoryTheory.Functor.relativelyRepresentable.isPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y) :

CategoryTheory.IsPullback (hf.fst g) (F.map (hf.snd g)) f g

theorem CategoryTheory.Functor.relativelyRepresentable.w_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y) {Z : D} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf.fst g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (F.map (hf.snd g)) (CategoryTheory.CategoryStruct.comp g h)

theorem CategoryTheory.Functor.relativelyRepresentable.w {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y) :

CategoryTheory.CategoryStruct.comp (hf.fst g) f = CategoryTheory.CategoryStruct.comp (F.map (hf.snd g)) g

theorem CategoryTheory.Functor.relativelyRepresentable.isPullback' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} (g : F.obj a ⟶ Y) [F.Full] :

CategoryTheory.IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g

Variant of the pullback square when F is full, and given f' : F.obj b ⟶ Y.

theorem CategoryTheory.Functor.relativelyRepresentable.w'_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} {Z : C} {f : X ⟶ Z✝} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z✝) [F.Full] [F.Faithful] {Z : C} (h : Z✝ ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf.fst' (F.map g)) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (hf.snd (F.map g)) (CategoryTheory.CategoryStruct.comp g h)

theorem CategoryTheory.Functor.relativelyRepresentable.w' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} {Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf.fst' (F.map g)) f = CategoryTheory.CategoryStruct.comp (hf.snd (F.map g)) g

theorem CategoryTheory.Functor.relativelyRepresentable.isPullback_of_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} {Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z) [F.Full] [F.Faithful] :

CategoryTheory.IsPullback (hf.fst' (F.map g)) (hf.snd (F.map g)) f g

theorem CategoryTheory.Functor.relativelyRepresentable.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} {hf : F.relativelyRepresentable f} {a : C} {g : F.obj a✝ ⟶ Y} [F.Faithful] {c : C} {a : c ⟶ hf.pullback g} {b : c ⟶ hf.pullback g} :

a = b ↔ CategoryTheory.CategoryStruct.comp (F.map a) (hf.fst g) = CategoryTheory.CategoryStruct.comp (F.map b) (hf.fst g) ∧ CategoryTheory.CategoryStruct.comp a (hf.snd g) = CategoryTheory.CategoryStruct.comp b (hf.snd g)

theorem CategoryTheory.Functor.relativelyRepresentable.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a✝ ⟶ Y} [F.Faithful] {c : C} {a : c ⟶ hf.pullback g} {b : c ⟶ hf.pullback g} (h₁ : CategoryTheory.CategoryStruct.comp (F.map a) (hf.fst g) = CategoryTheory.CategoryStruct.comp (F.map b) (hf.fst g)) (h₂ : CategoryTheory.CategoryStruct.comp a (hf.snd g) = CategoryTheory.CategoryStruct.comp b (hf.snd g)) :

a = b

Two morphisms a b : c ⟶ hf.pullback g are equal if

Their compositions (in C) with hf.snd g : hf.pullback ⟶ X are equal.
The compositions of F.map a and F.map b with hf.fst g are equal.

theorem CategoryTheory.Functor.relativelyRepresentable.hom_ext'_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b✝ ⟶ Y} {hf' : F.relativelyRepresentable f'} {a : C} {g : F.obj a✝ ⟶ Y} [F.Full] [F.Faithful] {c : C} {a : c ⟶ hf'.pullback g} {b : c ⟶ hf'.pullback g} :

a = b ↔ CategoryTheory.CategoryStruct.comp a (hf'.fst' g) = CategoryTheory.CategoryStruct.comp b (hf'.fst' g) ∧ CategoryTheory.CategoryStruct.comp a (hf'.snd g) = CategoryTheory.CategoryStruct.comp b (hf'.snd g)

theorem CategoryTheory.Functor.relativelyRepresentable.hom_ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b✝ ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a✝ ⟶ Y} [F.Full] [F.Faithful] {c : C} {a : c ⟶ hf'.pullback g} {b : c ⟶ hf'.pullback g} (h₁ : CategoryTheory.CategoryStruct.comp a (hf'.fst' g) = CategoryTheory.CategoryStruct.comp b (hf'.fst' g)) (h₂ : CategoryTheory.CategoryStruct.comp a (hf'.snd g) = CategoryTheory.CategoryStruct.comp b (hf'.snd g)) :

a = b

In the case of a representable morphism f' : F.obj Y ⟶ G, whose codomain lies in the image of F, we get that two morphism a b : Z ⟶ hf.pullback g are equal if

Their compositions (in C) with hf'.snd g : hf.pullback ⟶ X are equal.
Their compositions (in C) with hf'.fst' g : hf.pullback ⟶ Y are equal.

noncomputable def CategoryTheory.Functor.relativelyRepresentable.lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y} {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [F.Full] :

c ⟶ hf.pullback g

The lift (in C) obtained from the universal property of F.obj (hf.pullback g), in the case when the cone point is in the image of F.obj.

Equations

hf.lift i h hi = F.preimage (CategoryTheory.Limits.PullbackCone.IsLimit.lift ⋯.isLimit i (F.map h) hi)

Instances For

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y} {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h✝) g) [F.Full] {Z : D} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (hf.lift i h✝ hi)) (CategoryTheory.CategoryStruct.comp (hf.fst g) h) = CategoryTheory.CategoryStruct.comp i h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y} {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [F.Full] :

CategoryTheory.CategoryStruct.comp (F.map (hf.lift i h hi)) (hf.fst g) = i

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y} {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h✝) g) [F.Full] [F.Faithful] {Z : C} (h : a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf.lift i h✝ hi) (CategoryTheory.CategoryStruct.comp (hf.snd g) h) = CategoryTheory.CategoryStruct.comp h✝ h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : D} {Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y} {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf.lift i h hi) (hf.snd g) = h

noncomputable def CategoryTheory.Functor.relativelyRepresentable.lift' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g) [F.Full] :

c ⟶ hf'.pullback g

Variant of lift in the case when the domain of f lies in the image of F.obj. Thus, in this case, one can obtain the lift directly by giving two morphisms in C.

Equations

hf'.lift' i h hi = hf'.lift (F.map i) h hi

Instances For

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift'_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h✝) g) [F.Full] [F.Faithful] {Z : C} (h : b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf'.lift' i h✝ hi) (CategoryTheory.CategoryStruct.comp (hf'.fst' g) h) = CategoryTheory.CategoryStruct.comp i h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift'_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf'.lift' i h hi) (hf'.fst' g) = i

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift'_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h✝) g) [F.Full] [F.Faithful] {Z : C} (h : a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf'.lift' i h✝ hi) (CategoryTheory.CategoryStruct.comp (hf'.snd g) h) = CategoryTheory.CategoryStruct.comp h✝ h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.lift'_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a) (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf'.lift' i h hi) (hf'.snd g) = h

noncomputable def CategoryTheory.Functor.relativelyRepresentable.symmetry {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] :

hf'.pullback g ⟶ hg.pullback f'

Given two representable morphisms f' : F.obj b ⟶ Y and g : F.obj a ⟶ Y, we obtain an isomorphism hf'.pullback g ⟶ hg.pullback f'.

Equations

hf'.symmetry hg = hg.lift' (hf'.snd g) (hf'.fst' g) ⋯

Instances For

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetry_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] {Z : C} (h : a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.fst' f') h) = CategoryTheory.CategoryStruct.comp (hf'.snd g) h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetry_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (hg.fst' f') = hf'.snd g

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetry_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] {Z : C} (h : b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.snd f') h) = CategoryTheory.CategoryStruct.comp (hf'.fst' g) h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetry_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (hg.snd f') = hf'.fst' g

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetry_symmetry_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] {Z : C} (h : hf'.pullback g ⟶ Z) :

CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.symmetry hf') h) = h

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetry_symmetry {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (hg.symmetry hf') = CategoryTheory.CategoryStruct.id (hf'.pullback g)

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetryIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

(hf'.symmetryIso hg).hom = hf'.symmetry hg

@[simp]

theorem CategoryTheory.Functor.relativelyRepresentable.symmetryIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

(hf'.symmetryIso hg).inv = hg.symmetry hf'

noncomputable def CategoryTheory.Functor.relativelyRepresentable.symmetryIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

hf'.pullback g ≅ hg.pullback f'

The isomorphism given by Presheaf.representable.symmetry.

Equations

hf'.symmetryIso hg = { hom := hf'.symmetry hg, inv := hg.symmetry hf', hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

instance CategoryTheory.Functor.relativelyRepresentable.instIsIsoSymmetryOfFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C} {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [F.Full] [F.Faithful] :

CategoryTheory.IsIso (hf'.symmetry hg)

Equations

⋯ = ⋯

theorem CategoryTheory.Functor.relativelyRepresentable.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [CategoryTheory.Limits.HasPullbacks C] {a : C} {b : C} (f : a ⟶ b) :

F.relativelyRepresentable (F.map f)

When C has pullbacks, then F.map f is representable with respect to F for any f : a ⟶ b in C.

theorem CategoryTheory.Functor.relativelyRepresentable.of_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : D} {Y : D} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

F.relativelyRepresentable f

theorem CategoryTheory.Functor.relativelyRepresentable.isomorphisms_le {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

CategoryTheory.MorphismProperty.isomorphisms D ≤ F.relativelyRepresentable

instance CategoryTheory.Functor.relativelyRepresentable.isMultiplicative {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

F.relativelyRepresentable.IsMultiplicative

Equations

⋯ = ⋯

theorem CategoryTheory.Functor.relativelyRepresentable.stableUnderBaseChange {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

F.relativelyRepresentable.StableUnderBaseChange

instance CategoryTheory.Functor.relativelyRepresentable.respectsIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

F.relativelyRepresentable.RespectsIso

Equations

⋯ = ⋯