feat(category_theory/strong_epi): various results about strong_epi (#…

…16182)

In order to prepare for the proof of the existence of strong epi mono factorisations in `simplex_category` (which shall be used for the Dold-Kan correspondence), various results are obtained, mostly about strong epimorphisms (and strong monomorphisms). If two arrows are isomorphic, then one is a strong epi iff the other is. An equivalence of categories preserves and reflects strong epimorphisms.

src/category_theory/arrow.lean

@@ -106,6 +106,21 @@ abbreviation iso_mk' {W X Y Z : T} (f : W ⟶ X) (g : Y ⟶ Z)
   (e₁ : W ≅ Y) (e₂ : X ≅ Z) (h : e₁.hom ≫ g = f ≫ e₂.hom) : arrow.mk f ≅ arrow.mk g :=
 arrow.iso_mk e₁ e₂ h
 
+lemma hom.congr_left {f g : arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) :
+  φ₁.left = φ₂.left := by rw h
+lemma hom.congr_right {f g : arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) :
+  φ₁.right = φ₂.right := by rw h
+
+lemma iso_w {f g : arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right :=
+begin
+  have eq := arrow.hom.congr_right e.inv_hom_id,
+  dsimp at eq,
+  erw [w_assoc, eq, category.comp_id],
+end
+
+lemma iso_w' {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : arrow.mk f ≅ arrow.mk g) :
+  g = e.inv.left ≫ f ≫ e.hom.right := iso_w e
+
 section
 
 variables {f g : arrow T} (sq : f ⟶ g)
@@ -216,4 +231,11 @@ def map_arrow (F : C ⥤ D) : arrow C ⥤ arrow D :=
 
 end functor
 
+/-- The images of `f : arrow C` by two isomorphic functors `F : C ⥤ D` are
+isomorphic arrows in `D`. -/
+def arrow.iso_of_nat_iso {C D : Type*} [category C] [category D]
+  {F G : C ⥤ D} (e : F ≅ G) (f : arrow C) :
+  F.map_arrow.obj f ≅ G.map_arrow.obj f :=
+arrow.iso_mk (e.app f.left) (e.app f.right) (by simp)
+
 end category_theory

src/category_theory/concrete_category/basic.lean

@@ -134,6 +134,10 @@ lemma concrete_category.epi_of_surjective {X Y : C} (f : X ⟶ Y) (s : function.
   epi f :=
 (forget C).epi_of_epi_map ((epi_iff_surjective f).2 s)
 
+lemma concrete_category.bijective_of_is_iso {X Y : C} (f : X ⟶ Y) [is_iso f] :
+  function.bijective ((forget C).map f) :=
+by { rw ← is_iso_iff_bijective, apply_instance, }
+
 @[simp] lemma concrete_category.has_coe_to_fun_Type {X Y : Type u} (f : X ⟶ Y) :
   coe_fn f = f :=
 rfl

src/category_theory/functor/epi_mono.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import category_theory.epi_mono
+import category_theory.limits.shapes.strong_epi
+import category_theory.lifting_properties.adjunction
 
 /-!
 # Preservation and reflection of monomorphisms and epimorphisms
@@ -199,6 +201,14 @@ def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f)
   left_inv := by tidy,
   right_inv := by tidy, }
 
+@[simp]
+lemma is_split_epi_iff [full F] [faithful F] : is_split_epi (F.map f) ↔ is_split_epi f :=
+begin
+  split,
+  { intro h, exact is_split_epi.mk' ((split_epi_equiv F f).inv_fun h.exists_split_epi.some), },
+  { intro h, exact is_split_epi.mk' ((split_epi_equiv F f).to_fun h.exists_split_epi.some), },
+end
+
 /-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/
 def split_mono_equiv [full F] [faithful F] : split_mono f ≃ split_mono (F.map f) :=
 { to_fun := λ f, f.map F,
@@ -211,6 +221,14 @@ def split_mono_equiv [full F] [faithful F] : split_mono f ≃ split_mono (F.map
   left_inv := by tidy,
   right_inv := by tidy, }
 
+@[simp]
+lemma is_split_mono_iff [full F] [faithful F] : is_split_mono (F.map f) ↔ is_split_mono f :=
+begin
+  split,
+  { intro h, exact is_split_mono.mk' ((split_mono_equiv F f).inv_fun h.exists_split_mono.some), },
+  { intro h, exact is_split_mono.mk' ((split_mono_equiv F f).to_fun h.exists_split_mono.some), },
+end
+
 @[simp]
 lemma epi_map_iff_epi [hF₁ : preserves_epimorphisms F] [hF₂ : reflects_epimorphisms F] :
   epi (F.map f) ↔ epi f :=
@@ -234,3 +252,38 @@ end
 end
 
 end category_theory.functor
+
+namespace category_theory.adjunction
+
+variables {C D : Type*} [category C] [category D] {F : C ⥤ D} {F' : D ⥤ C} {A B : C}
+
+lemma strong_epi_map_of_strong_epi (adj : F ⊣ F') (f : A ⟶ B)
+  [h₁ : F'.preserves_monomorphisms] [h₂ : F.preserves_epimorphisms] [strong_epi f] :
+  strong_epi (F.map f) :=
+⟨infer_instance, λ X Y Z, by { introI, rw adj.has_lifting_property_iff, apply_instance, }⟩
+
+instance strong_epi_map_of_is_equivalence [is_equivalence F] (f : A ⟶ B) [h : strong_epi f] :
+  strong_epi (F.map f) :=
+F.as_equivalence.to_adjunction.strong_epi_map_of_strong_epi f
+
+end category_theory.adjunction
+
+namespace category_theory.functor
+
+variables {C D : Type*} [category C] [category D] {F : C ⥤ D} {A B : C} (f : A ⟶ B)
+
+@[simp]
+lemma strong_epi_map_iff_strong_epi_of_is_equivalence [is_equivalence F] :
+  strong_epi (F.map f) ↔ strong_epi f  :=
+begin
+  split,
+  { introI,
+    have e : arrow.mk f ≅ arrow.mk (F.inv.map (F.map f)) :=
+      arrow.iso_of_nat_iso F.as_equivalence.unit_iso (arrow.mk f),
+    rw strong_epi.iff_of_arrow_iso e,
+    apply_instance, },
+  { introI,
+    apply_instance, },
+end
+
+end category_theory.functor

src/category_theory/lifting_properties/basic.lean

@@ -104,6 +104,26 @@ instance of_comp_right [has_lifting_property i p] [has_lifting_property i p'] :
       fac_right' := by simp only [comm_sq.fac_right_assoc, comm_sq.fac_right], },
 end⟩
 
+lemma of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
+  (e : arrow.mk i ≅ arrow.mk i') (p : X ⟶ Y)
+  [hip : has_lifting_property i p] : has_lifting_property i' p :=
+by { rw arrow.iso_w' e, apply_instance, }
+
+lemma of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
+  (e : arrow.mk p ≅ arrow.mk p')
+  [hip : has_lifting_property i p] : has_lifting_property i p' :=
+by { rw arrow.iso_w' e, apply_instance, }
+
+lemma iff_of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
+  (e : arrow.mk i ≅ arrow.mk i') (p : X ⟶ Y) :
+  has_lifting_property i p ↔ has_lifting_property i' p :=
+by { split; introI, exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p], }
+
+lemma iff_of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
+  (e : arrow.mk p ≅ arrow.mk p') :
+  has_lifting_property i p ↔ has_lifting_property i p' :=
+by { split; introI, exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm], }
+
 end has_lifting_property
 
 end category_theory

src/category_theory/limits/shapes/strong_epi.lean

@@ -119,6 +119,32 @@ lemma strong_mono_of_strong_mono [strong_mono (f ≫ g)] : strong_mono f :=
 { mono := by apply_instance,
   rlp := λ X Y z hz, has_lifting_property.of_right_iso _ _, }
 
+lemma strong_epi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+  (e : arrow.mk f ≅ arrow.mk g) [h : strong_epi f] : strong_epi g :=
+{ epi := begin
+    rw arrow.iso_w' e,
+    haveI := epi_comp f e.hom.right,
+    apply epi_comp,
+  end,
+  llp := λ X Y z, by { introI, apply has_lifting_property.of_arrow_iso_left e z, }, }
+
+lemma strong_mono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+  (e : arrow.mk f ≅ arrow.mk g) [h : strong_mono f] : strong_mono g :=
+{ mono := begin
+    rw arrow.iso_w' e,
+    haveI := mono_comp f e.hom.right,
+    apply mono_comp,
+  end,
+  rlp := λ X Y z, by { introI, apply has_lifting_property.of_arrow_iso_right z e, }, }
+
+lemma strong_epi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+  (e : arrow.mk f ≅ arrow.mk g) : strong_epi f ↔ strong_epi g :=
+by { split; introI, exacts [strong_epi.of_arrow_iso e, strong_epi.of_arrow_iso e.symm], }
+
+lemma strong_mono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
+  (e : arrow.mk f ≅ arrow.mk g) : strong_mono f ↔ strong_mono g :=
+by { split; introI, exacts [strong_mono.of_arrow_iso e, strong_mono.of_arrow_iso e.symm], }
+
 end
 
 /-- A strong epimorphism that is a monomorphism is an isomorphism. -/