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.

  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:

Main results #

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
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) :
            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) :
            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) :
            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] :
            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} :
            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} :
            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
            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) :
              @[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) :
              @[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) :
                @[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) :
                @[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) :
                  @[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) :
                  @[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) :
                  @[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
                    • =

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

                    Equations
                    • =