|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Markus Himmel. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Markus Himmel |
| 5 | +-/ |
| 6 | +import category_theory.epi_mono |
| 7 | + |
| 8 | +/-! |
| 9 | +# Preservation and reflection of monomorphisms and epimorphisms |
| 10 | +
|
| 11 | +We provide typeclasses that state that a functor preserves or reflects monomorphisms or |
| 12 | +epimorphisms. |
| 13 | +-/ |
| 14 | + |
| 15 | +open category_theory |
| 16 | + |
| 17 | +universes v₁ v₂ v₃ u₁ u₂ u₃ |
| 18 | + |
| 19 | +namespace category_theory.functor |
| 20 | +variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D] |
| 21 | + {E : Type u₃} [category.{v₃} E] |
| 22 | + |
| 23 | +/-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms. -/ |
| 24 | +class preserves_monomorphisms (F : C ⥤ D) : Prop := |
| 25 | +(preserves : ∀ {X Y : C} (f : X ⟶ Y) [mono f], mono (F.map f)) |
| 26 | + |
| 27 | +instance map_mono (F : C ⥤ D) [preserves_monomorphisms F] {X Y : C} (f : X ⟶ Y) [mono f] : |
| 28 | + mono (F.map f) := |
| 29 | +preserves_monomorphisms.preserves f |
| 30 | + |
| 31 | +/-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms. -/ |
| 32 | +class preserves_epimorphisms (F : C ⥤ D) : Prop := |
| 33 | +(preserves : ∀ {X Y : C} (f : X ⟶ Y) [epi f], epi (F.map f)) |
| 34 | + |
| 35 | +instance map_epi (F : C ⥤ D) [preserves_epimorphisms F] {X Y : C} (f : X ⟶ Y) [epi f] : |
| 36 | + epi (F.map f) := |
| 37 | +preserves_epimorphisms.preserves f |
| 38 | + |
| 39 | +/-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves |
| 40 | + monomorphisms. -/ |
| 41 | +class reflects_monomorphisms (F : C ⥤ D) : Prop := |
| 42 | +(reflects : ∀ {X Y : C} (f : X ⟶ Y), mono (F.map f) → mono f) |
| 43 | + |
| 44 | +lemma mono_of_mono_map (F : C ⥤ D) [reflects_monomorphisms F] {X Y : C} {f : X ⟶ Y} |
| 45 | + (h : mono (F.map f)) : mono f := |
| 46 | +reflects_monomorphisms.reflects f h |
| 47 | + |
| 48 | +/-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves |
| 49 | + epimorphisms. -/ |
| 50 | +class reflects_epimorphisms (F : C ⥤ D) : Prop := |
| 51 | +(reflects : ∀ {X Y : C} (f : X ⟶ Y), epi (F.map f) → epi f) |
| 52 | + |
| 53 | +lemma epi_of_epi_map (F : C ⥤ D) [reflects_epimorphisms F] {X Y : C} {f : X ⟶ Y} |
| 54 | + (h : epi (F.map f)) : epi f := |
| 55 | +reflects_epimorphisms.reflects f h |
| 56 | + |
| 57 | +instance preserves_monomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [preserves_monomorphisms F] |
| 58 | + [preserves_monomorphisms G] : preserves_monomorphisms (F ⋙ G) := |
| 59 | +{ preserves := λ X Y f h, by { rw comp_map, exactI infer_instance } } |
| 60 | + |
| 61 | +instance preserves_epimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [preserves_epimorphisms F] |
| 62 | + [preserves_epimorphisms G] : preserves_epimorphisms (F ⋙ G) := |
| 63 | +{ preserves := λ X Y f h, by { rw comp_map, exactI infer_instance } } |
| 64 | + |
| 65 | +instance reflects_monomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [reflects_monomorphisms F] |
| 66 | + [reflects_monomorphisms G] : reflects_monomorphisms (F ⋙ G) := |
| 67 | +{ reflects := λ X Y f h, (F.mono_of_mono_map (G.mono_of_mono_map h)) } |
| 68 | + |
| 69 | +instance reflects_epimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [reflects_epimorphisms F] |
| 70 | + [reflects_epimorphisms G] : reflects_epimorphisms (F ⋙ G) := |
| 71 | +{ reflects := λ X Y f h, (F.epi_of_epi_map (G.epi_of_epi_map h)) } |
| 72 | + |
| 73 | +lemma preserves_monomorphisms.of_iso {F G : C ⥤ D} [preserves_monomorphisms F] (α : F ≅ G) : |
| 74 | + preserves_monomorphisms G := |
| 75 | +{ preserves := λ X Y f h, |
| 76 | + begin |
| 77 | + haveI : mono (F.map f ≫ (α.app Y).hom) := by exactI mono_comp _ _, |
| 78 | + convert (mono_comp _ _ : mono ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom)), |
| 79 | + rw [iso.eq_inv_comp, iso.app_hom, iso.app_hom, nat_trans.naturality] |
| 80 | + end } |
| 81 | + |
| 82 | +lemma preserves_monomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : |
| 83 | + preserves_monomorphisms F ↔ preserves_monomorphisms G := |
| 84 | +⟨λ h, by exactI preserves_monomorphisms.of_iso α, |
| 85 | + λ h, by exactI preserves_monomorphisms.of_iso α.symm⟩ |
| 86 | + |
| 87 | +lemma preserves_epimorphisms.of_iso {F G : C ⥤ D} [preserves_epimorphisms F] (α : F ≅ G) : |
| 88 | + preserves_epimorphisms G := |
| 89 | +{ preserves := λ X Y f h, |
| 90 | + begin |
| 91 | + haveI : epi (F.map f ≫ (α.app Y).hom) := by exactI epi_comp _ _, |
| 92 | + convert (epi_comp _ _ : epi ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom)), |
| 93 | + rw [iso.eq_inv_comp, iso.app_hom, iso.app_hom, nat_trans.naturality] |
| 94 | + end } |
| 95 | + |
| 96 | +lemma preserves_epimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : |
| 97 | + preserves_epimorphisms F ↔ preserves_epimorphisms G := |
| 98 | +⟨λ h, by exactI preserves_epimorphisms.of_iso α, |
| 99 | + λ h, by exactI preserves_epimorphisms.of_iso α.symm⟩ |
| 100 | + |
| 101 | +lemma reflects_monomorphisms.of_iso {F G : C ⥤ D} [reflects_monomorphisms F] (α : F ≅ G) : |
| 102 | + reflects_monomorphisms G := |
| 103 | +{ reflects := λ X Y f h, |
| 104 | + begin |
| 105 | + apply F.mono_of_mono_map, |
| 106 | + haveI : mono (G.map f ≫ (α.app Y).inv) := by exactI mono_comp _ _, |
| 107 | + convert (mono_comp _ _ : mono ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv)), |
| 108 | + rw [← category.assoc, iso.eq_comp_inv, iso.app_hom, iso.app_hom, nat_trans.naturality] |
| 109 | + end } |
| 110 | + |
| 111 | +lemma reflects_monomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : |
| 112 | + reflects_monomorphisms F ↔ reflects_monomorphisms G := |
| 113 | +⟨λ h, by exactI reflects_monomorphisms.of_iso α, |
| 114 | + λ h, by exactI reflects_monomorphisms.of_iso α.symm⟩ |
| 115 | + |
| 116 | +lemma reflects_epimorphisms.of_iso {F G : C ⥤ D} [reflects_epimorphisms F] (α : F ≅ G) : |
| 117 | + reflects_epimorphisms G := |
| 118 | +{ reflects := λ X Y f h, |
| 119 | + begin |
| 120 | + apply F.epi_of_epi_map, |
| 121 | + haveI : epi (G.map f ≫ (α.app Y).inv) := by exactI epi_comp _ _, |
| 122 | + convert (epi_comp _ _ : epi ((α.app X).hom ≫ G.map f ≫ (α.app Y).inv)), |
| 123 | + rw [← category.assoc, iso.eq_comp_inv, iso.app_hom, iso.app_hom, nat_trans.naturality] |
| 124 | + end } |
| 125 | + |
| 126 | +lemma reflects_epimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) : |
| 127 | + reflects_epimorphisms F ↔ reflects_epimorphisms G := |
| 128 | +⟨λ h, by exactI reflects_epimorphisms.of_iso α, λ h, by exactI reflects_epimorphisms.of_iso α.symm⟩ |
| 129 | + |
| 130 | +lemma preserves_epimorphsisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : |
| 131 | + preserves_epimorphisms F := |
| 132 | +{ preserves := λ X Y f hf, |
| 133 | + ⟨begin |
| 134 | + introsI Z g h H, |
| 135 | + replace H := congr_arg (adj.hom_equiv X Z) H, |
| 136 | + rwa [adj.hom_equiv_naturality_left, adj.hom_equiv_naturality_left, cancel_epi, |
| 137 | + equiv.apply_eq_iff_eq] at H |
| 138 | + end⟩ } |
| 139 | + |
| 140 | +@[priority 100] |
| 141 | +instance preserves_epimorphisms_of_is_left_adjoint (F : C ⥤ D) [is_left_adjoint F] : |
| 142 | + preserves_epimorphisms F := |
| 143 | +preserves_epimorphsisms_of_adjunction (adjunction.of_left_adjoint F) |
| 144 | + |
| 145 | +lemma preserves_monomorphisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : |
| 146 | + preserves_monomorphisms G := |
| 147 | +{ preserves := λ X Y f hf, |
| 148 | + ⟨begin |
| 149 | + introsI Z g h H, |
| 150 | + replace H := congr_arg (adj.hom_equiv Z Y).symm H, |
| 151 | + rwa [adj.hom_equiv_naturality_right_symm, adj.hom_equiv_naturality_right_symm, |
| 152 | + cancel_mono, equiv.apply_eq_iff_eq] at H |
| 153 | + end⟩ } |
| 154 | + |
| 155 | +@[priority 100] |
| 156 | +instance preserves_monomorphisms_of_is_right_adjoint (F : C ⥤ D) [is_right_adjoint F] : |
| 157 | + preserves_monomorphisms F := |
| 158 | +preserves_monomorphisms_of_adjunction (adjunction.of_right_adjoint F) |
| 159 | + |
| 160 | +@[priority 100] |
| 161 | +instance reflects_monomorphisms_of_faithful (F : C ⥤ D) [faithful F] : reflects_monomorphisms F := |
| 162 | +{ reflects := λ X Y f hf, ⟨λ Z g h hgh, by exactI F.map_injective ((cancel_mono (F.map f)).1 |
| 163 | + (by rw [← F.map_comp, hgh, F.map_comp]))⟩ } |
| 164 | + |
| 165 | +@[priority 100] |
| 166 | +instance reflects_epimorphisms_of_faithful (F : C ⥤ D) [faithful F] : reflects_epimorphisms F := |
| 167 | +{ reflects := λ X Y f hf, ⟨λ Z g h hgh, by exactI F.map_injective ((cancel_epi (F.map f)).1 |
| 168 | + (by rw [← F.map_comp, hgh, F.map_comp]))⟩ } |
| 169 | + |
| 170 | +end category_theory.functor |
0 commit comments