Relatively representable morphisms

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

Classically, a morphism f : F ⟶ G 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.

• Functor.relativelyRepresentable: 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

• MorphismProperty.relative: Given a morphism property P in C, a morphism f : X ⟶ Y in D satisfies P.relative F if it is relatively representable and for any g : F.obj a ⟶ Y, the property P holds for any represented pullback of f by g.

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

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

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

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

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

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 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 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X 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.w_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X 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.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' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y 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.w'_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y 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.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 Y 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 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y} [F.Faithful] {c : C} {a✝ 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' {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✝ 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 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)

@[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 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_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X 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_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X 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

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

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

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

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

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

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

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 := ⋯ }

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

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)

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.HasPullbacks C] {a b : C} (f : a ⟶ b) [∀ (c : C) (g : c ⟶ b), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F] : 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 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

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

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

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

Given a morphism property P in a category C, a functor F : C ⥤ D and a morphism f : X ⟶ Y in D. Then f satisfies the morphism property P.relative with respect to F iff:

• The morphism is representable with respect to F
• For any morphism g : F.obj a ⟶ Y, the property P holds for any represented pullback of f by g.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.presheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty (CategoryTheory.Functor Cᵒᵖ (Type v₁))

Given a morphism property P in a category C, a morphism f : F ⟶ G of presheaves in the category Cᵒᵖ ⥤ Type v satisfies the morphism property P.presheaf iff:

• The morphism is representable.
• For any morphism g : F.obj a ⟶ G, the property P holds for any represented pullback of f by g. This is implemented as a special case of the more general notion of P.relative, to the case when the functor F is yoneda.

Equations

• P.presheaf = CategoryTheory.MorphismProperty.relative CategoryTheory.yoneda P

theorem CategoryTheory.MorphismProperty.relative.rep {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} {f : X ⟶ Y} (hf : CategoryTheory.MorphismProperty.relative F P f) : F.relativelyRepresentable f

A morphism satisfying P.relative is representable.

theorem CategoryTheory.MorphismProperty.relative.property {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} {f : X ⟶ Y} (hf : CategoryTheory.MorphismProperty.relative F P f) ⦃a b : C⦄ (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a) : CategoryTheory.IsPullback fst (F.map snd) f g → P snd

theorem CategoryTheory.MorphismProperty.relative.property_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} {f : X ⟶ Y} (hf : CategoryTheory.MorphismProperty.relative F P f) {a : C} (g : F.obj a ⟶ Y) : P (⋯.snd g)

theorem CategoryTheory.MorphismProperty.relative.of_exists {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full] [P.RespectsIso] {f : X ⟶ Y} (h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : CategoryTheory.IsPullback fst (F.map snd) f g), P snd) : CategoryTheory.MorphismProperty.relative F P f

Given a morphism property P which respects isomorphisms, then to show that a morphism f : X ⟶ Y satisfies P.relative it suffices to show that:

• The morphism is representable.
• For any morphism g : F.obj a ⟶ G, the property P holds for some represented pullback of f by g.

theorem CategoryTheory.MorphismProperty.relative_of_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full] [P.RespectsIso] {f : X ⟶ Y} (hf : F.relativelyRepresentable f) (h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), P (hf.snd g)) : CategoryTheory.MorphismProperty.relative F P f

theorem CategoryTheory.MorphismProperty.relative_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full] [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {a b : C} {f : a ⟶ b} [∀ (c : C) (g : c ⟶ b), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F] (hf : P f) : CategoryTheory.MorphismProperty.relative F P (F.map f)

If P : MorphismProperty C is stable under base change, F is fully faithful and preserves pullbacks, and C has all pullbacks, then for any f : a ⟶ b in C, F.map f satisfies P.relative if f satisfies P.

theorem CategoryTheory.MorphismProperty.of_relative_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {P : CategoryTheory.MorphismProperty C} {a b : C} {f : a ⟶ b} (hf : CategoryTheory.MorphismProperty.relative F P (F.map f)) : P f

theorem CategoryTheory.MorphismProperty.relative_map_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] {X Y : C} {f : X ⟶ Y} : CategoryTheory.MorphismProperty.relative F P (F.map f) ↔ P f

theorem CategoryTheory.MorphismProperty.relative_monotone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {P P' : CategoryTheory.MorphismProperty C} (h : P ≤ P') : CategoryTheory.MorphismProperty.relative F P ≤ CategoryTheory.MorphismProperty.relative F P'

If P' : MorphismProperty C is satisfied whenever P is, then also P'.relative is satisfied whenever P.relative is.

theorem CategoryTheory.MorphismProperty.relative_isStableUnderBaseChange {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C) : (CategoryTheory.MorphismProperty.relative F P).IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.relative_isStableUnderComposition {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C) [F.Faithful] [F.Full] [P.IsStableUnderComposition] : (CategoryTheory.MorphismProperty.relative F P).IsStableUnderComposition

instance CategoryTheory.MorphismProperty.relative_respectsIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C) : (CategoryTheory.MorphismProperty.relative F P).RespectsIso

instance CategoryTheory.MorphismProperty.relative_isMultiplicative {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (P : CategoryTheory.MorphismProperty C) [F.Faithful] [F.Full] [P.IsMultiplicative] [P.RespectsIso] : (CategoryTheory.MorphismProperty.relative F P).IsMultiplicative

theorem CategoryTheory.MorphismProperty.presheaf_monomorphisms_le_monomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.MorphismProperty.monomorphisms C).presheaf ≤ CategoryTheory.MorphismProperty.monomorphisms (CategoryTheory.Functor Cᵒᵖ (Type v₁))

Morphisms satisfying (monomorphism C).presheaf are in particular monomorphisms.