From f7baecbb54bd0f24f228576f97b1752fc3c9b318 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 11 Jul 2022 09:33:55 +0000 Subject: [PATCH] feat(category_theory/functor): preserving/reflecting monos/epis (#14829) --- src/algebra/category/Group/abelian.lean | 4 +- src/algebra/category/Group/adjunctions.lean | 6 +- src/algebraic_geometry/open_immersion.lean | 10 +- .../adjunction/evaluation.lean | 10 +- .../concrete_category/basic.lean | 6 +- src/category_theory/epi_mono.lean | 42 ----- src/category_theory/functor/epi_mono.lean | 170 ++++++++++++++++++ src/category_theory/glue_data.lean | 2 +- .../limits/constructions/epi_mono.lean | 36 +++- src/category_theory/over.lean | 6 +- src/topology/category/CompHaus/default.lean | 4 +- src/topology/category/Profinite/default.lean | 4 +- src/topology/category/Top/adjunctions.lean | 1 + src/topology/category/Top/epi_mono.lean | 8 +- 14 files changed, 228 insertions(+), 81 deletions(-) create mode 100644 src/category_theory/functor/epi_mono.lean diff --git a/src/algebra/category/Group/abelian.lean b/src/algebra/category/Group/abelian.lean index e9dd71e2ee605..a11ad5a1a383a 100644 --- a/src/algebra/category/Group/abelian.lean +++ b/src/algebra/category/Group/abelian.lean @@ -28,12 +28,12 @@ variables {X Y : AddCommGroup.{u}} (f : X ⟶ Y) /-- In the category of abelian groups, every monomorphism is normal. -/ def normal_mono (hf : mono f) : normal_mono f := equivalence_reflects_normal_mono (forget₂ (Module.{u} ℤ) AddCommGroup.{u}).inv $ - Module.normal_mono _ $ right_adjoint_preserves_mono (functor.adjunction _) hf + Module.normal_mono _ infer_instance /-- In the category of abelian groups, every epimorphism is normal. -/ def normal_epi (hf : epi f) : normal_epi f := equivalence_reflects_normal_epi (forget₂ (Module.{u} ℤ) AddCommGroup.{u}).inv $ - Module.normal_epi _ $ left_adjoint_preserves_epi (functor.adjunction _) hf + Module.normal_epi _ infer_instance end diff --git a/src/algebra/category/Group/adjunctions.lean b/src/algebra/category/Group/adjunctions.lean index 2167941a3068a..5b99034bb7177 100644 --- a/src/algebra/category/Group/adjunctions.lean +++ b/src/algebra/category/Group/adjunctions.lean @@ -65,6 +65,8 @@ adjunction.mk_of_hom_equiv hom_equiv_naturality_left_symm' := by { intros, ext, refl} } +instance : is_right_adjoint (forget AddCommGroup.{u}) := ⟨_, adj⟩ + /-- As an example, we now give a high-powered proof that the monomorphisms in `AddCommGroup` are just the injective functions. @@ -72,9 +74,7 @@ the monomorphisms in `AddCommGroup` are just the injective functions. (This proof works in all universes.) -/ example {G H : AddCommGroup.{u}} (f : G ⟶ H) [mono f] : function.injective f := -(mono_iff_injective f).1 (right_adjoint_preserves_mono adj (by apply_instance : mono f)) - -instance : is_right_adjoint (forget AddCommGroup.{u}) := ⟨_, adj⟩ +(mono_iff_injective f).1 (show mono ((forget AddCommGroup.{u}).map f), by apply_instance) end AddCommGroup diff --git a/src/algebraic_geometry/open_immersion.lean b/src/algebraic_geometry/open_immersion.lean index 1740844d6842a..fef2ecddf4123 100644 --- a/src/algebraic_geometry/open_immersion.lean +++ b/src/algebraic_geometry/open_immersion.lean @@ -630,8 +630,8 @@ include H local notation `forget` := SheafedSpace.forget_to_PresheafedSpace open category_theory.limits.walking_cospan -instance : mono f := faithful_reflects_mono forget - (show @mono (PresheafedSpace C) _ _ _ f, by apply_instance) +instance : mono f := +forget .mono_of_mono_map (show @mono (PresheafedSpace C) _ _ _ f, by apply_instance) instance forget_map_is_open_immersion : PresheafedSpace.is_open_immersion (forget .map f) := ⟨H.base_open, H.c_iso⟩ @@ -862,8 +862,7 @@ instance comp (g : Z ⟶ Y) [LocallyRingedSpace.is_open_immersion g] : LocallyRingedSpace.is_open_immersion (f ≫ g) := PresheafedSpace.is_open_immersion.comp f.1 g.1 instance mono : mono f := -faithful_reflects_mono (LocallyRingedSpace.forget_to_SheafedSpace) - (show mono f.1, by apply_instance) +LocallyRingedSpace.forget_to_SheafedSpace.mono_of_mono_map (show mono f.1, by apply_instance) instance : SheafedSpace.is_open_immersion (LocallyRingedSpace.forget_to_SheafedSpace.map f) := H @@ -1405,8 +1404,7 @@ include H local notation `forget` := Scheme.forget_to_LocallyRingedSpace instance mono : mono f := -faithful_reflects_mono (induced_functor _) - (show @mono LocallyRingedSpace _ _ _ f, by apply_instance) +(induced_functor _).mono_of_mono_map (show @mono LocallyRingedSpace _ _ _ f, by apply_instance) instance forget_map_is_open_immersion : LocallyRingedSpace.is_open_immersion (forget .map f) := ⟨H.base_open, H.c_iso⟩ diff --git a/src/category_theory/adjunction/evaluation.lean b/src/category_theory/adjunction/evaluation.lean index 237f5a79edc58..1bcf4ca7e93ef 100644 --- a/src/category_theory/adjunction/evaluation.lean +++ b/src/category_theory/adjunction/evaluation.lean @@ -5,7 +5,7 @@ Authors: Adam Topaz -/ import category_theory.limits.shapes.products -import category_theory.epi_mono +import category_theory.functor.epi_mono /-! @@ -79,8 +79,8 @@ lemma nat_trans.mono_iff_app_mono {F G : C ⥤ D} (η : F ⟶ G) : mono η ↔ (∀ c, mono (η.app c)) := begin split, - { intros h c, - exact right_adjoint_preserves_mono (evaluation_adjunction_right D c) h }, + { introsI h c, + exact (infer_instance : mono (((evaluation _ _).obj c).map η)) }, { introsI _, apply nat_trans.mono_app_of_mono } end @@ -144,8 +144,8 @@ lemma nat_trans.epi_iff_app_epi {F G : C ⥤ D} (η : F ⟶ G) : epi η ↔ (∀ c, epi (η.app c)) := begin split, - { intros h c, - exact left_adjoint_preserves_epi (evaluation_adjunction_left D c) h }, + { introsI h c, + exact (infer_instance : epi (((evaluation _ _).obj c).map η)) }, { introsI, apply nat_trans.epi_app_of_epi } end diff --git a/src/category_theory/concrete_category/basic.lean b/src/category_theory/concrete_category/basic.lean index 1b2366e6aa80c..bf12a8c81f664 100644 --- a/src/category_theory/concrete_category/basic.lean +++ b/src/category_theory/concrete_category/basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudryashov -/ import category_theory.types -import category_theory.epi_mono +import category_theory.functor.epi_mono /-! # Concrete categories @@ -127,12 +127,12 @@ congr_arg (f : X → Y) h /-- In any concrete category, injective morphisms are monomorphisms. -/ lemma concrete_category.mono_of_injective {X Y : C} (f : X ⟶ Y) (i : function.injective f) : mono f := -faithful_reflects_mono (forget C) ((mono_iff_injective f).2 i) +(forget C).mono_of_mono_map ((mono_iff_injective f).2 i) /-- In any concrete category, surjective morphisms are epimorphisms. -/ lemma concrete_category.epi_of_surjective {X Y : C} (f : X ⟶ Y) (s : function.surjective f) : epi f := -faithful_reflects_epi (forget C) ((epi_iff_surjective f).2 s) +(forget C).epi_of_epi_map ((epi_iff_surjective f).2 s) @[simp] lemma concrete_category.has_coe_to_fun_Type {X Y : Type u} (f : X ⟶ Y) : coe_fn f = f := diff --git a/src/category_theory/epi_mono.lean b/src/category_theory/epi_mono.lean index 21c763c5e3f33..002a0a4857b37 100644 --- a/src/category_theory/epi_mono.lean +++ b/src/category_theory/epi_mono.lean @@ -32,48 +32,6 @@ instance op_mono_of_epi {A B : C} (f : A ⟶ B) [epi f] : mono f.op := instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op := ⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩ -section -variables {D : Type u₂} [category.{v₂} D] - -lemma left_adjoint_preserves_epi {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) - {X Y : C} {f : X ⟶ Y} (hf : epi f) : epi (F.map f) := -begin - constructor, - intros Z g h H, - replace H := congr_arg (adj.hom_equiv X Z) H, - rwa [adj.hom_equiv_naturality_left, adj.hom_equiv_naturality_left, - cancel_epi, equiv.apply_eq_iff_eq] at H -end - -lemma right_adjoint_preserves_mono {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) - {X Y : D} {f : X ⟶ Y} (hf : mono f) : mono (G.map f) := -begin - constructor, - intros Z g h H, - replace H := congr_arg (adj.hom_equiv Z Y).symm H, - rwa [adj.hom_equiv_naturality_right_symm, adj.hom_equiv_naturality_right_symm, - cancel_mono, equiv.apply_eq_iff_eq] at H -end - -instance is_equivalence.epi_map {F : C ⥤ D} [is_left_adjoint F] {X Y : C} {f : X ⟶ Y} - [h : epi f] : epi (F.map f) := -left_adjoint_preserves_epi (adjunction.of_left_adjoint F) h - -instance is_equivalence.mono_map {F : C ⥤ D} [is_right_adjoint F] {X Y : C} {f : X ⟶ Y} - [h : mono f] : mono (F.map f) := -right_adjoint_preserves_mono (adjunction.of_right_adjoint F) h - -lemma faithful_reflects_epi (F : C ⥤ D) [faithful F] {X Y : C} {f : X ⟶ Y} - (hf : epi (F.map f)) : epi f := -⟨λ Z g h H, F.map_injective $ - by rw [←cancel_epi (F.map f), ←F.map_comp, ←F.map_comp, H]⟩ - -lemma faithful_reflects_mono (F : C ⥤ D) [faithful F] {X Y : C} {f : X ⟶ Y} - (hf : mono (F.map f)) : mono f := -⟨λ Z g h H, F.map_injective $ - by rw [←cancel_mono (F.map f), ←F.map_comp, ←F.map_comp, H]⟩ -end - /-- A split monomorphism is a morphism `f : X ⟶ Y` admitting a retraction `retraction f : Y ⟶ X` such that `f ≫ retraction f = 𝟙 X`. diff --git a/src/category_theory/functor/epi_mono.lean b/src/category_theory/functor/epi_mono.lean new file mode 100644 index 0000000000000..2ed2ad6f30291 --- /dev/null +++ b/src/category_theory/functor/epi_mono.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2022 Markus Himmel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus Himmel +-/ +import category_theory.epi_mono + +/-! +# Preservation and reflection of monomorphisms and epimorphisms + +We provide typeclasses that state that a functor preserves or reflects monomorphisms or +epimorphisms. +-/ + +open category_theory + +universes v₁ v₂ v₃ u₁ u₂ u₃ + +namespace category_theory.functor +variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D] + {E : Type u₃} [category.{v₃} E] + +/-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms. -/ +class preserves_monomorphisms (F : C ⥤ D) : Prop := +(preserves : ∀ {X Y : C} (f : X ⟶ Y) [mono f], mono (F.map f)) + +instance map_mono (F : C ⥤ D) [preserves_monomorphisms F] {X Y : C} (f : X ⟶ Y) [mono f] : + mono (F.map f) := +preserves_monomorphisms.preserves f + +/-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms. -/ +class preserves_epimorphisms (F : C ⥤ D) : Prop := +(preserves : ∀ {X Y : C} (f : X ⟶ Y) [epi f], epi (F.map f)) + +instance map_epi (F : C ⥤ D) [preserves_epimorphisms F] {X Y : C} (f : X ⟶ Y) [epi f] : + epi (F.map f) := +preserves_epimorphisms.preserves f + +/-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves + monomorphisms. -/ +class reflects_monomorphisms (F : C ⥤ D) : Prop := +(reflects : ∀ {X Y : C} (f : X ⟶ Y), mono (F.map f) → mono f) + +lemma mono_of_mono_map (F : C ⥤ D) [reflects_monomorphisms F] {X Y : C} {f : X ⟶ Y} + (h : mono (F.map f)) : mono f := +reflects_monomorphisms.reflects f h + +/-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves + epimorphisms. -/ +class reflects_epimorphisms (F : C ⥤ D) : Prop := +(reflects : ∀ {X Y : C} (f : X ⟶ Y), epi (F.map f) → epi f) + +lemma epi_of_epi_map (F : C ⥤ D) [reflects_epimorphisms F] {X Y : C} {f : X ⟶ Y} + (h : epi (F.map f)) : epi f := +reflects_epimorphisms.reflects f h + +instance preserves_monomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [preserves_monomorphisms F] + [preserves_monomorphisms G] : preserves_monomorphisms (F ⋙ G) := +{ preserves := λ X Y f h, by { rw comp_map, exactI infer_instance } } + +instance preserves_epimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [preserves_epimorphisms F] + [preserves_epimorphisms G] : preserves_epimorphisms (F ⋙ G) := +{ preserves := λ X Y f h, by { rw comp_map, exactI infer_instance } } + +instance reflects_monomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [reflects_monomorphisms F] + [reflects_monomorphisms G] : reflects_monomorphisms (F ⋙ G) := +{ reflects := λ X Y f h, (F.mono_of_mono_map (G.mono_of_mono_map h)) } + +instance reflects_epimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [reflects_epimorphisms F] + [reflects_epimorphisms G] : reflects_epimorphisms (F ⋙ G) := +{ reflects := λ X Y f h, (F.epi_of_epi_map (G.epi_of_epi_map h)) } + +lemma preserves_monomorphisms.of_iso {F G : C ⥤ D} [preserves_monomorphisms F] (α : F ≅ G) : + preserves_monomorphisms G := +{ preserves := λ X Y f h, + begin + haveI : mono (F.map f ≫ (α.app Y).hom) := by exactI mono_comp _ _, + convert (mono_comp _ _ : mono ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom)), + rw [iso.eq_inv_comp, iso.app_hom, iso.app_hom, nat_trans.naturality] + end } + +lemma preserves_monomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : + preserves_monomorphisms F ↔ preserves_monomorphisms G := +⟨λ h, by exactI preserves_monomorphisms.of_iso α, + λ h, by exactI preserves_monomorphisms.of_iso α.symm⟩ + +lemma preserves_epimorphisms.of_iso {F G : C ⥤ D} [preserves_epimorphisms F] (α : F ≅ G) : + preserves_epimorphisms G := +{ preserves := λ X Y f h, + begin + haveI : epi (F.map f ≫ (α.app Y).hom) := by exactI epi_comp _ _, + convert (epi_comp _ _ : epi ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom)), + rw [iso.eq_inv_comp, iso.app_hom, iso.app_hom, nat_trans.naturality] + end } + +lemma preserves_epimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : + preserves_epimorphisms F ↔ preserves_epimorphisms G := +⟨λ h, by exactI preserves_epimorphisms.of_iso α, + λ h, by exactI preserves_epimorphisms.of_iso α.symm⟩ + +lemma reflects_monomorphisms.of_iso {F G : C ⥤ D} [reflects_monomorphisms F] (α : F ≅ G) : + reflects_monomorphisms G := +{ reflects := λ X Y f h, + begin + apply F.mono_of_mono_map, + haveI : mono (G.map f ≫ (α.app Y).inv) := by exactI mono_comp _ _, + convert (mono_comp _ _ : mono ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv)), + rw [← category.assoc, iso.eq_comp_inv, iso.app_hom, iso.app_hom, nat_trans.naturality] + end } + +lemma reflects_monomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : + reflects_monomorphisms F ↔ reflects_monomorphisms G := +⟨λ h, by exactI reflects_monomorphisms.of_iso α, + λ h, by exactI reflects_monomorphisms.of_iso α.symm⟩ + +lemma reflects_epimorphisms.of_iso {F G : C ⥤ D} [reflects_epimorphisms F] (α : F ≅ G) : + reflects_epimorphisms G := +{ reflects := λ X Y f h, + begin + apply F.epi_of_epi_map, + haveI : epi (G.map f ≫ (α.app Y).inv) := by exactI epi_comp _ _, + convert (epi_comp _ _ : epi ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv)), + rw [← category.assoc, iso.eq_comp_inv, iso.app_hom, iso.app_hom, nat_trans.naturality] + end } + +lemma reflects_epimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : + reflects_epimorphisms F ↔ reflects_epimorphisms G := +⟨λ h, by exactI reflects_epimorphisms.of_iso α, λ h, by exactI reflects_epimorphisms.of_iso α.symm⟩ + +lemma preserves_epimorphsisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : + preserves_epimorphisms F := +{ preserves := λ X Y f hf, + ⟨begin + introsI Z g h H, + replace H := congr_arg (adj.hom_equiv X Z) H, + rwa [adj.hom_equiv_naturality_left, adj.hom_equiv_naturality_left, cancel_epi, + equiv.apply_eq_iff_eq] at H + end⟩ } + +@[priority 100] +instance preserves_epimorphisms_of_is_left_adjoint (F : C ⥤ D) [is_left_adjoint F] : + preserves_epimorphisms F := +preserves_epimorphsisms_of_adjunction (adjunction.of_left_adjoint F) + +lemma preserves_monomorphisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : + preserves_monomorphisms G := +{ preserves := λ X Y f hf, + ⟨begin + introsI Z g h H, + replace H := congr_arg (adj.hom_equiv Z Y).symm H, + rwa [adj.hom_equiv_naturality_right_symm, adj.hom_equiv_naturality_right_symm, + cancel_mono, equiv.apply_eq_iff_eq] at H + end⟩ } + +@[priority 100] +instance preserves_monomorphisms_of_is_right_adjoint (F : C ⥤ D) [is_right_adjoint F] : + preserves_monomorphisms F := +preserves_monomorphisms_of_adjunction (adjunction.of_right_adjoint F) + +@[priority 100] +instance reflects_monomorphisms_of_faithful (F : C ⥤ D) [faithful F] : reflects_monomorphisms F := +{ reflects := λ X Y f hf, ⟨λ Z g h hgh, by exactI F.map_injective ((cancel_mono (F.map f)).1 + (by rw [← F.map_comp, hgh, F.map_comp]))⟩ } + +@[priority 100] +instance reflects_epimorphisms_of_faithful (F : C ⥤ D) [faithful F] : reflects_epimorphisms F := +{ reflects := λ X Y f hf, ⟨λ Z g h hgh, by exactI F.map_injective ((cancel_epi (F.map f)).1 + (by rw [← F.map_comp, hgh, F.map_comp]))⟩ } + +end category_theory.functor diff --git a/src/category_theory/glue_data.lean b/src/category_theory/glue_data.lean index 422f45d391d19..bd2220c9a6b92 100644 --- a/src/category_theory/glue_data.lean +++ b/src/category_theory/glue_data.lean @@ -199,7 +199,7 @@ instance (i j k : D.J) : has_pullback (F.map (D.f i j)) (F.map (D.f i k)) := U := λ i, F.obj (D.U i), V := λ i, F.obj (D.V i), f := λ i j, F.map (D.f i j), - f_mono := λ i j, category_theory.preserves_mono F (D.f i j), + f_mono := λ i j, preserves_mono_of_preserves_limit _ _, f_id := λ i, infer_instance, t := λ i j, F.map (D.t i j), t_id := λ i, by { rw D.t_id i, simp }, diff --git a/src/category_theory/limits/constructions/epi_mono.lean b/src/category_theory/limits/constructions/epi_mono.lean index 4461c6edfc975..db94b19d852fb 100644 --- a/src/category_theory/limits/constructions/epi_mono.lean +++ b/src/category_theory/limits/constructions/epi_mono.lean @@ -25,35 +25,50 @@ variables {C : Type u₁} {D : Type u₂} [category.{v₁} C] [category.{v₂} D variables (F : C ⥤ D) /-- If `F` preserves pullbacks, then it preserves monomorphisms. -/ -instance preserves_mono {X Y : C} (f : X ⟶ Y) [preserves_limit (cospan f f) F] [mono f] : - mono (F.map f) := +lemma preserves_mono_of_preserves_limit {X Y : C} (f : X ⟶ Y) [preserves_limit (cospan f f) F] + [mono f] : mono (F.map f) := begin have := is_limit_pullback_cone_map_of_is_limit F _ (pullback_cone.is_limit_mk_id_id f), simp_rw [F.map_id] at this, apply pullback_cone.mono_of_is_limit_mk_id_id _ this, end +@[priority 100] +instance preserves_monomorphisms_of_preserves_limits_of_shape + [preserves_limits_of_shape walking_cospan F] : F.preserves_monomorphisms := +{ preserves := λ X Y f hf, by exactI preserves_mono_of_preserves_limit F f } + /-- If `F` reflects pullbacks, then it reflects monomorphisms. -/ -lemma reflects_mono {X Y : C} (f : X ⟶ Y) [reflects_limit (cospan f f) F] [mono (F.map f)] : - mono f := +lemma reflects_mono_of_reflects_limit {X Y : C} (f : X ⟶ Y) [reflects_limit (cospan f f) F] + [mono (F.map f)] : mono f := begin have := pullback_cone.is_limit_mk_id_id (F.map f), simp_rw [←F.map_id] at this, apply pullback_cone.mono_of_is_limit_mk_id_id _ (is_limit_of_is_limit_pullback_cone_map F _ this), end +@[priority 100] +instance reflects_monomorphisms_of_reflects_limits_of_shape + [reflects_limits_of_shape walking_cospan F] : F.reflects_monomorphisms := +{ reflects := λ X Y f hf, by exactI reflects_mono_of_reflects_limit F f } + /-- If `F` preserves pushouts, then it preserves epimorphisms. -/ -instance preserves_epi {X Y : C} (f : X ⟶ Y) [preserves_colimit (span f f) F] [epi f] : - epi (F.map f) := +lemma preserves_epi_of_preserves_colimit {X Y : C} (f : X ⟶ Y) [preserves_colimit (span f f) F] + [epi f] : epi (F.map f) := begin have := is_colimit_pushout_cocone_map_of_is_colimit F _ (pushout_cocone.is_colimit_mk_id_id f), simp_rw [F.map_id] at this, apply pushout_cocone.epi_of_is_colimit_mk_id_id _ this, end +@[priority 100] +instance preserves_epimorphisms_of_preserves_colimits_of_shape + [preserves_colimits_of_shape walking_span F] : F.preserves_epimorphisms := +{ preserves := λ X Y f hf, by exactI preserves_epi_of_preserves_colimit F f } + /-- If `F` reflects pushouts, then it reflects epimorphisms. -/ -lemma reflects_epi {X Y : C} (f : X ⟶ Y) [reflects_colimit (span f f) F] [epi (F.map f)] : - epi f := +lemma reflects_epi_of_reflects_colimit {X Y : C} (f : X ⟶ Y) [reflects_colimit (span f f) F] + [epi (F.map f)] : epi f := begin have := pushout_cocone.is_colimit_mk_id_id (F.map f), simp_rw [← F.map_id] at this, @@ -61,4 +76,9 @@ begin (is_colimit_of_is_colimit_pushout_cocone_map F _ this) end +@[priority 100] +instance reflects_epimorphisms_of_reflects_colimits_of_shape + [reflects_colimits_of_shape walking_span F] : F.reflects_epimorphisms := +{ reflects := λ X Y f hf, by exactI reflects_epi_of_reflects_colimit F f } + end category_theory diff --git a/src/category_theory/over.lean b/src/category_theory/over.lean index 6ce654adeb05a..3438a646700aa 100644 --- a/src/category_theory/over.lean +++ b/src/category_theory/over.lean @@ -6,7 +6,7 @@ Authors: Johan Commelin, Bhavik Mehta import category_theory.structured_arrow import category_theory.punit import category_theory.functor.reflects_isomorphisms -import category_theory.epi_mono +import category_theory.functor.epi_mono /-! # Over and under categories @@ -147,7 +147,7 @@ The converse does not hold without additional assumptions on the underlying cate -/ -- TODO: Show the converse holds if `T` has binary products or pushouts. lemma epi_of_epi_left {f g : over X} (k : f ⟶ g) [hk : epi k.left] : epi k := -faithful_reflects_epi (forget X) hk +(forget X).epi_of_epi_map hk /-- If `k.left` is a monomorphism, then `k` is a monomorphism. In other words, `over.forget X` reflects @@ -157,7 +157,7 @@ The converse of `category_theory.over.mono_left_of_mono`. This lemma is not an instance, to avoid loops in type class inference. -/ lemma mono_of_mono_left {f g : over X} (k : f ⟶ g) [hk : mono k.left] : mono k := -faithful_reflects_mono (forget X) hk +(forget X).mono_of_mono_map hk /-- If `k` is a monomorphism, then `k.left` is a monomorphism. In other words, `over.forget X` preserves diff --git a/src/topology/category/CompHaus/default.lean b/src/topology/category/CompHaus/default.lean index 4c7d7325ab7e4..cecaffef17560 100644 --- a/src/topology/category/CompHaus/default.lean +++ b/src/topology/category/CompHaus/default.lean @@ -228,7 +228,7 @@ begin simp only [subtype.mk_eq_mk, hφ1 (set.mem_singleton y), pi.one_apply] at H, exact zero_ne_one H, }, { rw ← category_theory.epi_iff_surjective, - apply faithful_reflects_epi (forget CompHaus) }, + apply (forget CompHaus).epi_of_epi_map } end lemma mono_iff_injective {X Y : CompHaus.{u}} (f : X ⟶ Y) : mono f ↔ function.injective f := @@ -242,7 +242,7 @@ begin apply_fun (λ e, e punit.star) at this, exact this }, { rw ← category_theory.mono_iff_injective, - apply faithful_reflects_mono (forget CompHaus) } + apply (forget CompHaus).mono_of_mono_map } end end CompHaus diff --git a/src/topology/category/Profinite/default.lean b/src/topology/category/Profinite/default.lean index 615e55709b93d..8b99832f1c294 100644 --- a/src/topology/category/Profinite/default.lean +++ b/src/topology/category/Profinite/default.lean @@ -280,7 +280,7 @@ begin rw if_pos hyV at H, exact top_ne_bot H }, { rw ← category_theory.epi_iff_surjective, - apply faithful_reflects_epi (forget Profinite) }, + apply (forget Profinite).epi_of_epi_map } end lemma mono_iff_injective {X Y : Profinite.{u}} (f : X ⟶ Y) : mono f ↔ function.injective f := @@ -291,7 +291,7 @@ begin haveI : mono (Profinite_to_CompHaus.map f) := infer_instance, rwa ← CompHaus.mono_iff_injective }, { rw ← category_theory.mono_iff_injective, - apply faithful_reflects_mono (forget Profinite) } + apply (forget Profinite).mono_of_mono_map } end end Profinite diff --git a/src/topology/category/Top/adjunctions.lean b/src/topology/category/Top/adjunctions.lean index 62a4711da14c7..a0ce2a4cf7430 100644 --- a/src/topology/category/Top/adjunctions.lean +++ b/src/topology/category/Top/adjunctions.lean @@ -38,5 +38,6 @@ adjunction.mk_of_unit_counit counit := { app := λ X, id } } instance : is_right_adjoint (forget Top.{u}) := ⟨_, adj₁⟩ +instance : is_left_adjoint (forget Top.{u}) := ⟨_, adj₂⟩ end Top diff --git a/src/topology/category/Top/epi_mono.lean b/src/topology/category/Top/epi_mono.lean index c99937ab9c3bc..b113ee4df1355 100644 --- a/src/topology/category/Top/epi_mono.lean +++ b/src/topology/category/Top/epi_mono.lean @@ -26,8 +26,8 @@ begin suffices : epi f ↔ epi ((forget Top).map f), { rw [this, category_theory.epi_iff_surjective], refl }, split, - { apply left_adjoint_preserves_epi adj₂ }, - { apply faithful_reflects_epi } + { introI, apply_instance }, + { apply functor.epi_of_epi_map } end lemma mono_iff_injective {X Y : Top.{u}} (f : X ⟶ Y) : mono f ↔ function.injective f := @@ -35,8 +35,8 @@ begin suffices : mono f ↔ mono ((forget Top).map f), { rw [this, category_theory.mono_iff_injective], refl }, split, - { apply right_adjoint_preserves_mono adj₁ }, - { apply faithful_reflects_mono } + { introI, apply_instance }, + { apply functor.mono_of_mono_map } end end Top