Monomorphisms over a fixed object #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
As preparation for defining subobject X, we set up the theory for
mono_over X := {f : over X // mono f.hom}.
Here mono_over X is a thin category (a pair of objects has at most one morphism between them),
so we can think of it as a preorder. However as it is not skeletal, it is not yet a partial order.
subobject X will be defined as the skeletalization of mono_over X.
We provide
def pullback [has_pullbacks C] (f : X ⟶ Y) : mono_over Y ⥤ mono_over Xdef map (f : X ⟶ Y) [mono f] : mono_over X ⥤ mono_over Ydef «exists» [has_images C] (f : X ⟶ Y) : mono_over X ⥤ mono_over Yand prove their basic properties and relationships.
Notes #
This development originally appeared in Bhavik Mehta's "Topos theory for Lean" repository, and was ported to mathlib by Scott Morrison.
The category of monomorphisms into X as a full subcategory of the over category.
This isn't skeletal, so it's not a partial order.
Later we define subobject X as the quotient of this by isomorphisms.
Equations
@[protected, instance]
def
category_theory.mono_over.mk'
{C : Type u₁}
[category_theory.category C]
{X A : C}
(f : A ⟶ X)
[hf : category_theory.mono f] :
Construct a mono_over X.
Equations
- category_theory.mono_over.mk' f = {obj := category_theory.over.mk f, property := hf}
@[simp]
theorem
category_theory.mono_over.mk'_obj
{C : Type u₁}
[category_theory.category C]
{X A : C}
(f : A ⟶ X)
[hf : category_theory.mono f] :
The inclusion from monomorphisms over X to morphisms over X.
Equations
@[protected, instance]
Equations
- category_theory.mono_over.has_coe = {coe := λ (Y : category_theory.mono_over X), Y.obj.left}
@[simp]
theorem
category_theory.mono_over.forget_obj_left
{C : Type u₁}
[category_theory.category C]
{X : C}
{f : category_theory.mono_over X} :
((category_theory.mono_over.forget X).obj f).left = ↑f
@[simp]
theorem
category_theory.mono_over.mk'_coe'
{C : Type u₁}
[category_theory.category C]
{X A : C}
(f : A ⟶ X)
[hf : category_theory.mono f] :
@[reducible]
def
category_theory.mono_over.arrow
{C : Type u₁}
[category_theory.category C]
{X : C}
(f : category_theory.mono_over X) :
Convenience notation for the underlying arrow of a monomorphism over X.
@[simp]
theorem
category_theory.mono_over.mk'_arrow
{C : Type u₁}
[category_theory.category C]
{X A : C}
(f : A ⟶ X)
[hf : category_theory.mono f] :
@[simp]
theorem
category_theory.mono_over.forget_obj_hom
{C : Type u₁}
[category_theory.category C]
{X : C}
{f : category_theory.mono_over X} :
((category_theory.mono_over.forget X).obj f).hom = f.arrow
@[protected, instance]
def
category_theory.mono_over.forget.category_theory.full
{C : Type u₁}
[category_theory.category C]
{X : C} :
@[protected, instance]
@[protected, instance]
def
category_theory.mono_over.mono
{C : Type u₁}
[category_theory.category C]
{X : C}
(f : category_theory.mono_over X) :
@[protected, instance]
The category of monomorphisms over X is a thin category, which makes defining its skeleton easy.
theorem
category_theory.mono_over.w
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
(k : f ⟶ g) :
theorem
category_theory.mono_over.w_assoc
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
(k : f ⟶ g)
{X' : C}
(f' : X ⟶ X') :
@[reducible]
def
category_theory.mono_over.hom_mk
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
(h : f.obj.left ⟶ g.obj.left)
(w : h ≫ g.arrow = f.arrow) :
f ⟶ g
Convenience constructor for a morphism in monomorphisms over X.
@[simp]
theorem
category_theory.mono_over.iso_mk_hom
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
(h : f.obj.left ≅ g.obj.left)
(w : h.hom ≫ g.arrow = f.arrow) :
def
category_theory.mono_over.iso_mk
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
(h : f.obj.left ≅ g.obj.left)
(w : h.hom ≫ g.arrow = f.arrow) :
f ≅ g
Convenience constructor for an isomorphism in monomorphisms over X.
Equations
- category_theory.mono_over.iso_mk h w = {hom := category_theory.mono_over.hom_mk h.hom w, inv := category_theory.mono_over.hom_mk h.inv _, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.mono_over.iso_mk_inv
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
(h : f.obj.left ≅ g.obj.left)
(w : h.hom ≫ g.arrow = f.arrow) :
@[simp]
def
category_theory.mono_over.mk'_arrow_iso
{C : Type u₁}
[category_theory.category C]
{X : C}
(f : category_theory.mono_over X) :
If f : mono_over X, then mk' f.arrow is of course just f, but not definitionally, so we
package it as an isomorphism.
def
category_theory.mono_over.lift
{C : Type u₁}
[category_theory.category C]
{X : C}
{D : Type u₂}
[category_theory.category D]
{Y : D}
(F : category_theory.over Y ⥤ category_theory.over X)
(h : ∀ (f : category_theory.mono_over Y), category_theory.mono (F.obj ((category_theory.mono_over.forget Y).obj f)).hom) :
Lift a functor between over categories to a functor between mono_over categories,
given suitable evidence that morphisms are taken to monomorphisms.
Equations
- category_theory.mono_over.lift F h = {obj := λ (f : category_theory.mono_over Y), {obj := F.obj ((category_theory.mono_over.forget Y).obj f), property := _}, map := λ (_x _x_1 : category_theory.mono_over Y) (k : _x ⟶ _x_1), (category_theory.mono_over.forget X).preimage ((category_theory.mono_over.forget Y ⋙ F).map k), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.mono_over.lift_map
{C : Type u₁}
[category_theory.category C]
{X : C}
{D : Type u₂}
[category_theory.category D]
{Y : D}
(F : category_theory.over Y ⥤ category_theory.over X)
(h : ∀ (f : category_theory.mono_over Y), category_theory.mono (F.obj ((category_theory.mono_over.forget Y).obj f)).hom)
(_x _x_1 : category_theory.mono_over Y)
(k : _x ⟶ _x_1) :
(category_theory.mono_over.lift F h).map k = (category_theory.mono_over.forget X).preimage ((category_theory.mono_over.forget Y ⋙ F).map k)
@[simp]
theorem
category_theory.mono_over.lift_obj_obj
{C : Type u₁}
[category_theory.category C]
{X : C}
{D : Type u₂}
[category_theory.category D]
{Y : D}
(F : category_theory.over Y ⥤ category_theory.over X)
(h : ∀ (f : category_theory.mono_over Y), category_theory.mono (F.obj ((category_theory.mono_over.forget Y).obj f)).hom)
(f : category_theory.mono_over Y) :
((category_theory.mono_over.lift F h).obj f).obj = F.obj ((category_theory.mono_over.forget Y).obj f)
def
category_theory.mono_over.lift_iso
{C : Type u₁}
[category_theory.category C]
{X : C}
{D : Type u₂}
[category_theory.category D]
{Y : D}
{F₁ F₂ : category_theory.over Y ⥤ category_theory.over X}
(h₁ : ∀ (f : category_theory.mono_over Y), category_theory.mono (F₁.obj ((category_theory.mono_over.forget Y).obj f)).hom)
(h₂ : ∀ (f : category_theory.mono_over Y), category_theory.mono (F₂.obj ((category_theory.mono_over.forget Y).obj f)).hom)
(i : F₁ ≅ F₂) :
Isomorphic functors over Y ⥤ over X lift to isomorphic functors mono_over Y ⥤ mono_over X.
def
category_theory.mono_over.lift_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{X Z : C}
{Y : D}
(F : category_theory.over X ⥤ category_theory.over Y)
(G : category_theory.over Y ⥤ category_theory.over Z)
(h₁ : ∀ (f : category_theory.mono_over X), category_theory.mono (F.obj ((category_theory.mono_over.forget X).obj f)).hom)
(h₂ : ∀ (f : category_theory.mono_over Y), category_theory.mono (G.obj ((category_theory.mono_over.forget Y).obj f)).hom) :
mono_over.lift commutes with composition of functors.
def
category_theory.mono_over.lift_id
{C : Type u₁}
[category_theory.category C]
{X : C} :
category_theory.mono_over.lift (𝟭 (category_theory.over X)) category_theory.mono_over.lift_id._proof_1 ≅ 𝟭 (category_theory.mono_over X)
mono_over.lift preserves the identity functor.
Equations
- category_theory.mono_over.lift_id = category_theory.fully_faithful_cancel_right (category_theory.mono_over.forget X) (category_theory.iso.refl (category_theory.mono_over.lift (𝟭 (category_theory.over X)) category_theory.mono_over.lift_id._proof_2 ⋙ category_theory.mono_over.forget X))
@[simp]
theorem
category_theory.mono_over.lift_comm
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(F : category_theory.over Y ⥤ category_theory.over X)
(h : ∀ (f : category_theory.mono_over Y), category_theory.mono (F.obj ((category_theory.mono_over.forget Y).obj f)).hom) :
@[simp]
theorem
category_theory.mono_over.lift_obj_arrow
{C : Type u₁}
[category_theory.category C]
{X : C}
{D : Type u₂}
[category_theory.category D]
{Y : D}
(F : category_theory.over Y ⥤ category_theory.over X)
(h : ∀ (f : category_theory.mono_over Y), category_theory.mono (F.obj ((category_theory.mono_over.forget Y).obj f)).hom)
(f : category_theory.mono_over Y) :
((category_theory.mono_over.lift F h).obj f).arrow = (F.obj ((category_theory.mono_over.forget Y).obj f)).hom
def
category_theory.mono_over.slice
{C : Type u₁}
[category_theory.category C]
{A : C}
{f : category_theory.over A}
(h₁ : ∀ (f_1 : category_theory.mono_over f), category_theory.mono (f.iterated_slice_equiv.functor.obj ((category_theory.mono_over.forget f).obj f_1)).hom)
(h₂ : ∀ (f_1 : category_theory.mono_over f.left), category_theory.mono (f.iterated_slice_equiv.inverse.obj ((category_theory.mono_over.forget f.left).obj f_1)).hom) :
Monomorphisms over an object f : over A in an over category
are equivalent to monomorphisms over the source of f.
Equations
- category_theory.mono_over.slice h₁ h₂ = {functor := category_theory.mono_over.lift f.iterated_slice_equiv.functor h₁, inverse := category_theory.mono_over.lift f.iterated_slice_equiv.inverse h₂, unit_iso := category_theory.mono_over.lift_id.symm ≪≫ category_theory.mono_over.lift_iso category_theory.mono_over.slice._proof_3 _ f.iterated_slice_equiv.unit_iso ≪≫ (category_theory.mono_over.lift_comp f.iterated_slice_equiv.functor f.iterated_slice_equiv.inverse h₁ h₂).symm, counit_iso := category_theory.mono_over.lift_comp f.iterated_slice_equiv.inverse f.iterated_slice_equiv.functor h₂ h₁ ≪≫ category_theory.mono_over.lift_iso _ category_theory.mono_over.slice._proof_8 f.iterated_slice_equiv.counit_iso ≪≫ category_theory.mono_over.lift_id, functor_unit_iso_comp' := _}
noncomputable
def
category_theory.mono_over.pullback
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y) :
When C has pullbacks, a morphism f : X ⟶ Y induces a functor mono_over Y ⥤ mono_over X,
by pulling back a monomorphism along f.
noncomputable
def
category_theory.mono_over.pullback_comp
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y)
(g : Y ⟶ Z) :
pullback commutes with composition (up to a natural isomorphism)
noncomputable
def
category_theory.mono_over.pullback_id
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_pullbacks C] :
pullback preserves the identity (up to a natural isomorphism)
Equations
- category_theory.mono_over.pullback_id = category_theory.mono_over.lift_iso category_theory.mono_over.pullback_id._proof_1 category_theory.mono_over.lift_id._proof_1 category_theory.over.pullback_id ≪≫ category_theory.mono_over.lift_id
@[simp]
theorem
category_theory.mono_over.pullback_obj_left
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y)
(g : category_theory.mono_over Y) :
@[simp]
theorem
category_theory.mono_over.pullback_obj_arrow
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y)
(g : category_theory.mono_over Y) :
def
category_theory.mono_over.map
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
We can map monomorphisms over X to monomorphisms over Y
by post-composition with a monomorphism f : X ⟶ Y.
Equations
Instances for category_theory.mono_over.map
def
category_theory.mono_over.map_comp
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.mono f]
[category_theory.mono g] :
mono_over.map commutes with composition (up to a natural isomorphism).
mono_over.map preserves the identity (up to a natural isomorphism).
Equations
- category_theory.mono_over.map_id = category_theory.mono_over.lift_iso category_theory.mono_over.map_id._proof_1 category_theory.mono_over.lift_id._proof_1 category_theory.over.map_id ≪≫ category_theory.mono_over.lift_id
@[simp]
theorem
category_theory.mono_over.map_obj_left
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
(g : category_theory.mono_over X) :
@[simp]
theorem
category_theory.mono_over.map_obj_arrow
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
(g : category_theory.mono_over X) :
@[protected, instance]
def
category_theory.mono_over.full_map
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
Equations
- category_theory.mono_over.full_map f = {preimage := λ (g h : category_theory.mono_over X) (e : (category_theory.mono_over.map f).obj g ⟶ (category_theory.mono_over.map f).obj h), category_theory.mono_over.hom_mk e.left _, witness' := _}
@[protected, instance]
def
category_theory.mono_over.faithful_map
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
@[simp]
theorem
category_theory.mono_over.map_iso_functor
{C : Type u₁}
[category_theory.category C]
{A B : C}
(e : A ≅ B) :
def
category_theory.mono_over.map_iso
{C : Type u₁}
[category_theory.category C]
{A B : C}
(e : A ≅ B) :
Isomorphic objects have equivalent mono_over categories.
Equations
- category_theory.mono_over.map_iso e = {functor := category_theory.mono_over.map e.hom _, inverse := category_theory.mono_over.map e.inv _, unit_iso := ((category_theory.mono_over.map_comp e.hom e.inv).symm ≪≫ category_theory.eq_to_iso _ ≪≫ category_theory.mono_over.map_id).symm, counit_iso := (category_theory.mono_over.map_comp e.inv e.hom).symm ≪≫ category_theory.eq_to_iso _ ≪≫ category_theory.mono_over.map_id, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.mono_over.map_iso_unit_iso
{C : Type u₁}
[category_theory.category C]
{A B : C}
(e : A ≅ B) :
@[simp]
theorem
category_theory.mono_over.map_iso_inverse
{C : Type u₁}
[category_theory.category C]
{A B : C}
(e : A ≅ B) :
@[simp]
theorem
category_theory.mono_over.map_iso_counit_iso
{C : Type u₁}
[category_theory.category C]
{A B : C}
(e : A ≅ B) :
@[simp]
theorem
category_theory.mono_over.congr_functor
{C : Type u₁}
[category_theory.category C]
(X : C)
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
@[simp]
theorem
category_theory.mono_over.congr_inverse
{C : Type u₁}
[category_theory.category C]
(X : C)
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
@[simp]
theorem
category_theory.mono_over.congr_unit_iso
{C : Type u₁}
[category_theory.category C]
(X : C)
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
@[simp]
theorem
category_theory.mono_over.congr_counit_iso
{C : Type u₁}
[category_theory.category C]
(X : C)
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
(category_theory.mono_over.congr X e).counit_iso = category_theory.nat_iso.of_components (λ (Y : category_theory.mono_over (e.functor.obj X)), category_theory.mono_over.iso_mk (e.counit_iso.app ↑Y) _) _
def
category_theory.mono_over.congr
{C : Type u₁}
[category_theory.category C]
(X : C)
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
An equivalence of categories e between C and D induces an equivalence between
mono_over X and mono_over (e.functor.obj X) whenever X is an object of C.
Equations
- category_theory.mono_over.congr X e = {functor := category_theory.mono_over.lift (category_theory.over.post e.functor) _, inverse := category_theory.mono_over.lift (category_theory.over.post e.inverse) _ ⋙ (category_theory.mono_over.map_iso (e.unit_iso.symm.app X)).functor, unit_iso := category_theory.nat_iso.of_components (λ (Y : category_theory.mono_over X), category_theory.mono_over.iso_mk (e.unit_iso.app ↑Y) _) _, counit_iso := category_theory.nat_iso.of_components (λ (Y : category_theory.mono_over (e.functor.obj X)), category_theory.mono_over.iso_mk (e.counit_iso.app ↑Y) _) _, functor_unit_iso_comp' := _}
noncomputable
def
category_theory.mono_over.map_pullback_adj
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y)
[category_theory.mono f] :
map f is left adjoint to pullback f when f is a monomorphism
Equations
- category_theory.mono_over.map_pullback_adj f = category_theory.adjunction.restrict_fully_faithful (category_theory.mono_over.forget X) (category_theory.mono_over.forget Y) (category_theory.over.map_pullback_adj f) (category_theory.iso.refl (category_theory.mono_over.forget X ⋙ category_theory.over.map f)) (category_theory.iso.refl (category_theory.mono_over.forget Y ⋙ category_theory.over.pullback f))
noncomputable
def
category_theory.mono_over.pullback_map_self
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_pullbacks C]
(f : X ⟶ Y)
[category_theory.mono f] :
mono_over.map f followed by mono_over.pullback f is the identity.
noncomputable
def
category_theory.mono_over.image_mono_over
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
The mono_over Y for the image inclusion for a morphism f : X ⟶ Y.
@[simp]
theorem
category_theory.mono_over.image_mono_over_arrow
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
@[simp]
theorem
category_theory.mono_over.image_obj
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C]
(f : category_theory.over X) :
noncomputable
def
category_theory.mono_over.image
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C] :
Taking the image of a morphism gives a functor over X ⥤ mono_over X.
Equations
- category_theory.mono_over.image = {obj := λ (f : category_theory.over X), category_theory.mono_over.image_mono_over f.hom, map := λ (f g : category_theory.over X) (k : f ⟶ g), (category_theory.mono_over.forget X).preimage (category_theory.over.hom_mk (category_theory.limits.image.lift {I := category_theory.limits.image g.hom _, m := category_theory.limits.image.ι g.hom _, m_mono := _, e := k.left ≫ category_theory.limits.factor_thru_image g.hom, fac' := _}) _), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.mono_over.image_map
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C]
(f g : category_theory.over X)
(k : f ⟶ g) :
category_theory.mono_over.image.map k = (category_theory.mono_over.forget X).preimage (category_theory.over.hom_mk (category_theory.limits.image.lift {I := category_theory.limits.image g.hom _, m := category_theory.limits.image.ι g.hom _, m_mono := _, e := k.left ≫ category_theory.limits.factor_thru_image g.hom, fac' := _}) _)
noncomputable
def
category_theory.mono_over.image_forget_adj
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C] :
mono_over.image : over X ⥤ mono_over X is left adjoint to
mono_over.forget : mono_over X ⥤ over X
Equations
- category_theory.mono_over.image_forget_adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (f : category_theory.over X) (g : category_theory.mono_over X), {to_fun := λ (k : category_theory.mono_over.image.obj f ⟶ g), category_theory.over.hom_mk (category_theory.limits.factor_thru_image f.hom ≫ k.left) _, inv_fun := λ (k : f ⟶ (category_theory.mono_over.forget X).obj g), category_theory.over.hom_mk (category_theory.limits.image.lift {I := g.obj.left, m := g.arrow, m_mono := _, e := k.left, fac' := _}) _, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
@[protected, instance]
noncomputable
def
category_theory.mono_over.forget.category_theory.is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C] :
Equations
@[protected, instance]
noncomputable
def
category_theory.mono_over.reflective
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C] :
noncomputable
def
category_theory.mono_over.forget_image
{C : Type u₁}
[category_theory.category C]
{X : C}
[category_theory.limits.has_images C] :
Forgetting that a monomorphism over X is a monomorphism, then taking its image,
is the identity functor.
noncomputable
def
category_theory.mono_over.exists
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_images C]
(f : X ⟶ Y) :
In the case where f is not a monomorphism but C has images,
we can still take the "forward map" under it, which agrees with mono_over.map f.
Equations
Instances for category_theory.mono_over.exists
@[protected, instance]
def
category_theory.mono_over.faithful_exists
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_images C]
(f : X ⟶ Y) :
noncomputable
def
category_theory.mono_over.exists_iso_map
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_images C]
(f : X ⟶ Y)
[category_theory.mono f] :
When f : X ⟶ Y is a monomorphism, exists f agrees with map f.
noncomputable
def
category_theory.mono_over.exists_pullback_adj
{C : Type u₁}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_images C]
(f : X ⟶ Y)
[category_theory.limits.has_pullbacks C] :
exists is adjoint to pullback when images exist
Equations
- category_theory.mono_over.exists_pullback_adj f = category_theory.adjunction.restrict_fully_faithful (category_theory.mono_over.forget X) (𝟭 (category_theory.mono_over Y)) ((category_theory.over.map_pullback_adj f).comp category_theory.mono_over.image_forget_adj) (category_theory.iso.refl (category_theory.mono_over.forget X ⋙ category_theory.over.map f ⋙ category_theory.mono_over.image)) (category_theory.iso.refl (𝟭 (category_theory.mono_over Y) ⋙ category_theory.mono_over.forget Y ⋙ category_theory.over.pullback f))