feat(algebraic_topology/simplex_category): epi and monos in the simpl…

…ex category (#8101)

Characterize epimorphisms and monomorphisms in `simplex_category` in terms of the function they represent. Add lemmas about their behavior on length of objects. 



Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

src/algebraic_topology/simplex_category.lean

@@ -402,4 +402,100 @@ full_subcategory_inclusion _
 
 end truncated
 
+section concrete
+
+instance : concrete_category.{0} simplex_category.{u} :=
+{ forget :=
+  { obj := λ i, fin (i.len + 1),
+    map := λ i j f, f.to_preorder_hom },
+  forget_faithful := {} }
+
+end concrete
+
+section epi_mono
+
+/-- A morphism in `simplex_category` is a monomorphism precisely when it is an injective function
+-/
+theorem mono_iff_injective {n m : simplex_category} {f : n ⟶ m} :
+  mono f ↔ function.injective f.to_preorder_hom :=
+begin
+  split,
+  { introsI m x y h,
+    have H : const n x ≫ f = const n y ≫ f,
+    { dsimp, rw h },
+    change (n.const x).to_preorder_hom 0 = (n.const y).to_preorder_hom 0,
+    rw cancel_mono f at H,
+    rw H },
+  { exact concrete_category.mono_of_injective f }
+end
+
+/-- A morphism in `simplex_category` is an epimorphism if and only if it is a surjective function
+-/
+lemma epi_iff_surjective {n m : simplex_category} {f: n ⟶ m} :
+  epi f ↔ function.surjective f.to_preorder_hom :=
+begin
+  split,
+  { introsI hyp_f_epi x,
+    by_contradiction h_ab,
+    rw not_exists at h_ab,
+    -- The proof is by contradiction: assume f is not surjective,
+    -- then introduce two non-equal auxiliary functions equalizing f, and get a contradiction.
+    -- First we define the two auxiliary functions.
+    set chi_1 : m ⟶ [1] := hom.mk ⟨λ u, if u ≤ x then 0 else 1, begin
+      intros a b h,
+      dsimp only [],
+      split_ifs with h1 h2 h3,
+      any_goals { exact le_refl _ },
+      { exact bot_le },
+      { exact false.elim (h1 (le_trans h h3)) }
+    end ⟩,
+    set chi_2 : m ⟶ [1] := hom.mk ⟨λ u, if u < x then 0 else 1, begin
+      intros a b h,
+      dsimp only [],
+      split_ifs with h1 h2 h3,
+      any_goals { exact le_refl _ },
+      { exact bot_le },
+      { exact false.elim (h1 (lt_of_le_of_lt h h3)) }
+    end ⟩,
+    -- The two auxiliary functions equalize f
+    have f_comp_chi_i : f ≫ chi_1 = f ≫ chi_2,
+    { dsimp,
+      ext,
+      simp [le_iff_lt_or_eq, h_ab x_1] },
+    -- We now just have to show the two auxiliary functions are not equal.
+    rw category_theory.cancel_epi f at f_comp_chi_i, rename f_comp_chi_i eq_chi_i,
+    apply_fun (λ e, e.to_preorder_hom x) at eq_chi_i,
+    suffices : (0 : fin 2) = 1, by exact bot_ne_top this,
+    simpa using eq_chi_i },
+  { exact concrete_category.epi_of_surjective f }
+end
+
+/-- A monomorphism in `simplex_category` must increase lengths-/
+lemma len_le_of_mono {x y : simplex_category} {f : x ⟶ y} :
+  mono f → (x.len ≤ y.len) :=
+begin
+  intro hyp_f_mono,
+  have f_inj : function.injective f.to_preorder_hom.to_fun,
+  { exact mono_iff_injective.elim_left (hyp_f_mono) },
+  simpa using fintype.card_le_of_injective f.to_preorder_hom.to_fun f_inj,
+end
+
+lemma le_of_mono {n m : ℕ} {f : [n] ⟶ [m]} : (category_theory.mono f) → (n ≤ m) :=
+len_le_of_mono
+
+/-- An epimorphism in `simplex_category` must decrease lengths-/
+lemma len_le_of_epi {x y : simplex_category} {f : x ⟶ y} :
+  epi f → y.len ≤ x.len :=
+begin
+  intro hyp_f_epi,
+  have f_surj : function.surjective f.to_preorder_hom.to_fun,
+  { exact epi_iff_surjective.elim_left (hyp_f_epi) },
+  simpa using fintype.card_le_of_surjective f.to_preorder_hom.to_fun f_surj,
+end
+
+lemma le_of_epi {n m : ℕ} {f : [n] ⟶ [m]} : epi f → (m ≤ n) :=
+len_le_of_epi
+
+end epi_mono
+
 end simplex_category