Simplicial stuff

simplicial_stuff.lean

import order.category.NonemptyFinLinOrd
import category_theory.skeletal
import category_theory.types
import data.finset.sort
import data.fintype.basic
import data.set.basic
import order.rel_iso
import data.fin_enum
import set_theory.cardinal
import init
import algebraic_topology.simplex_category
import tactic.linarith

universe variables u
open category_theory
open_locale simplicial
namespace simplex_category

namespace epi_mono


lemma mono_iff_function_is_injective {u v : simplex_category} {f: u ⟶ v} : (category_theory.mono f) ↔ (function.injective ⇑(f.to_preorder_hom)):= begin
  split,
  {intros m x y h,
  set n := u.len with def_n,
  set m := v.len with def_m, 
  set cx : [0] ⟶ u := const u x with h_cx,
  set cy : [0] ⟶ u := const u y with h_cy,
  have H : (cx ≫ f = cy ≫ f) := by {
    dsimp,
    rw h,
  },
  resetI,
  rw (cancel_mono f) at H,
    have from_constant_function : (∀ (z : fin(u.len + 1)), (z = (const u z).to_preorder_hom.to_fun 0)) := by {
      intro z,
      simp,
      refl,
    },
    rw [from_constant_function x, from_constant_function y,←h_cx,←h_cy,H],
  },
  {
    intro H,
    split,
    intros Z g h hyp_eq,
    dsimp,
    ext,
    apply_fun hom.to_preorder_hom at hyp_eq,
    dsimp at hyp_eq,
    apply_fun preorder_hom.to_fun at hyp_eq,
    replace hyp_eq := (congr_fun hyp_eq x),
    rw [hom.to_preorder_hom_mk, hom.to_preorder_hom_mk] at hyp_eq,
    rw [preorder_hom.to_fun_eq_coe, preorder_hom.to_fun_eq_coe] at hyp_eq,
    rw [preorder_hom.comp_coe, preorder_hom.comp_coe] at hyp_eq,
    dsimp at hyp_eq,
    have last_hyp := H hyp_eq,
    rw last_hyp,
    }
end

lemma epi_iff_function_is_surjective {u v : simplex_category} {f: u ⟶ v} : (category_theory.epi f) ↔ (function.surjective ⇑f.to_preorder_hom) := begin
  split,
  {intro hyp_f_epi,
  intro x,
  set n := u.len with def_n,
  set m := v.len with def_m,
  by_contradiction h_ab,
  rw not_exists at h_ab,
  set chi_1 : v ⟶ [1] := hom.mk ⟨λ u, if u ≤ x then 0 else 1, by {
    intros a b a_leq_b,
    by_cases a ≤ x,
    {
     simp [h],
     obviously,
    },
    {
      simp [h],
      have b_ge_x : ¬(b ≤ x) := by {
        by_contra b_leq_x,
        have a_leq_x : a ≤ x := by {
          transitivity b,
          exact a_leq_b,
          exact b_leq_x,
        },
        exact h a_leq_x,
      },
      simp [b_ge_x],
    }
  }⟩ with def_chi_1,
  set chi_2 : v ⟶ [1] := hom.mk ⟨λ u, if u < x then 0 else 1, by {
    intros a b a_leq_b,
    by_cases (a = b),
    {
      rw h,
    },
    rename h a_neq_b,
    have a_lt_b : a < b := by {
      cases nat.eq_or_lt_of_le a_leq_b,{
        exfalso,
        exact a_neq_b (subtype.eq h),
      },
      {
        exact h,
      }
    },
    by_cases a < x,
    {
     simp [h],
     obviously,
    },
    {
      simp [h],
      have b_geq_x : ¬(b < x) := by {
        by_contra b_leq_x,
        have a_lt_x : a < x := by {
          transitivity b,
          exact a_lt_b,
          exact b_leq_x,
        },
        exact h a_lt_x,
      },
      simp [b_geq_x],
    }
  }⟩ with def_chi_2,
  have f_compo_chi_i : f ≫ chi_1 = f ≫ chi_2 := by {
    dsimp,
    ext,
    rw [hom.to_preorder_hom_mk, hom.to_preorder_hom_mk, preorder_hom.comp_coe],
    rw [hom.to_preorder_hom_mk, hom.to_preorder_hom_mk, preorder_hom.comp_coe],
    rw [function.comp_app, function.comp_app],
    have f_x_1_ne_x : ¬((f.to_preorder_hom) x_1 = x) := by {
        exact h_ab x_1,
      },
    by_cases ((f.to_preorder_hom) x_1) ≤ x,
    { 
     
      have f_x_1_lt_x : ((f.to_preorder_hom) x_1) < x := by {
        cases nat.eq_or_lt_of_le h,
        exfalso,
        replace h_1 := subtype.eq h_1,
        exact f_x_1_ne_x h_1,
        exact h_1,
      },
      simp [f_x_1_lt_x, h],
    },
    {
      have n_f_x_1_lt_x : ¬(((f.to_preorder_hom) x_1) < x) := by {
        erw not_iff_not_of_iff nat.lt_iff_le_not_le,
        rw not_and,
        intro h3, exfalso,
        refine h h3,
      },
      simp [n_f_x_1_lt_x, h],
    }
  },
   resetI,
   rw category_theory.cancel_epi f at f_compo_chi_i, rename f_compo_chi_i eq_chi_i,
   apply_fun hom.to_preorder_hom at eq_chi_i,
   apply_fun preorder_hom.to_fun at eq_chi_i,
   replace eq_chi_i := congr_fun eq_chi_i x,
   dsimp at eq_chi_i,
   have chi_1_x : (hom.to_preorder_hom chi_1) x = 0 := by {
     simp,
   },
   have chi_2_x : (hom.to_preorder_hom chi_2) x = 1 := by {
     simp,
   },
   rw [chi_1_x, chi_2_x] at eq_chi_i,
   refine nat.zero_ne_one (fin.veq_of_eq eq_chi_i),
  },
  {
    intro hyp_surj,
    refine ⟨ by{
      intros l g h h_eq_comp,
      dsimp at *,
      ext,
      set y := Exists.some (hyp_surj x) with d_y,
      have y_eq_f_x : x = f.to_preorder_hom y := by {
        rw d_y,
        exact (Exists.some_spec (hyp_surj x)).symm,
      },
      apply_fun hom.to_preorder_hom at h_eq_comp,
      apply_fun preorder_hom.to_fun at h_eq_comp,
      replace h_eq_comp := congr_fun h_eq_comp y,
      dsimp at h_eq_comp,
      rw [hom.to_preorder_hom_mk, preorder_hom.comp_coe, function.comp_app] at h_eq_comp,
      rw [hom.to_preorder_hom_mk, preorder_hom.comp_coe, function.comp_app] at h_eq_comp,
      rw ←y_eq_f_x at h_eq_comp,
      refine fin.veq_of_eq h_eq_comp,
    }
    ⟩,
  }
end




lemma mono_le_length {x y : simplex_category} {f : x ⟶ y} : (category_theory.mono f) → (x.len ≤ y.len) := begin 
  set n := x.len with def_n,
  set m := y.len with def_m,
  intro hyp_f_mono,
  have f_inj : function.injective f.to_preorder_hom.to_fun := mono_iff_function_is_injective.elim_left (hyp_f_mono),
  have card_leq := fintype.card_le_of_injective f.to_preorder_hom.to_fun f_inj,
  simp at card_leq,
  exact card_leq,
end

lemma mono_le_card {n m : ℕ} {f : [n] ⟶ [m]} : (category_theory.mono f) → (n ≤ m) := by {refine @mono_le_length [n] [m] f}

lemma epi_ge_length {x y : simplex_category} {f : x ⟶ y} : (category_theory.epi f) → (x.len ≥ y.len) := begin
  intro hyp_f_epi, 
  have f_surj : function.surjective f.to_preorder_hom.to_fun := epi_iff_function_is_surjective.elim_left (hyp_f_epi),
  have card_geq := fintype.card_le_of_surjective f.to_preorder_hom.to_fun f_surj,
  simp at card_geq,
  exact card_geq,
end

lemma epi_ge_card {n m : ℕ} {f : [n] ⟶ [m]} : (category_theory.epi f) → (n ≥ m) := by {refine @epi_ge_length [n] [m] f}
end epi_mono 


namespace image
  -- variables {x y: simplex_category.{u}}
  def range_nb {x y : simplex_category} (f : x ⟶ y) : ℕ := fintype.card (set.range f.to_preorder_hom.to_fun) - 1
   --variable f : x ⟶ y
  -- #check  (mono_equiv_of_fin (set.range (f.to_preorder_hom.to_fun)) (by obviously)).to_fun
  def f_to_range_f_inv {x y : simplex_category} (f : x ⟶ y) : fin ((range_nb f) + 1) ≃o (set.range (f.to_preorder_hom.to_fun)) := (mono_equiv_of_fin (set.range (f.to_preorder_hom.to_fun)) (by {
     rw range_nb,
     rw nat.sub_add_cancel,
     rw nat.add_one_le_iff,
     rw fintype.card_pos_iff,
     simp,
     exact set.range.nonempty f.to_preorder_hom.to_fun,
   }
 ))
 lemma same_range_implies_same_range_nb {x y z: simplex_category} {f : x ⟶ y} {g : z ⟶ y} (h : (set.range ⇑(f.to_preorder_hom)) = (set.range ⇑(g.to_preorder_hom))) : (range_nb f = range_nb g) :=
  begin 
    rw range_nb,
    rw range_nb,
    rw [preorder_hom.to_fun_eq_coe, preorder_hom.to_fun_eq_coe],
    have eq_coe : ↥(set.range ⇑(hom.to_preorder_hom f)) = ↥(set.range ⇑(hom.to_preorder_hom g)) := by {obviously},
    rw fintype.card_congr (@equiv.cast (set.range ⇑(f.to_preorder_hom)) (set.range ⇑(g.to_preorder_hom)) eq_coe),
  end 

end image

namespace epi_mono

-- In this section, we prove that any morphism in the simplex category admits a unique epi-mono factorization

def epi_component {x y : simplex_category} (f : x ⟶ y) : (x ⟶ [image.range_nb f]) := (hom.mk ⟨((image.f_to_range_f_inv f).symm.to_order_embedding) ∘ (set.range_factorization f.to_preorder_hom.to_fun),
      monotone.comp (((image.f_to_range_f_inv f).symm.to_order_embedding).monotone) (by {
        intros a b a_le_b,
        rw set.range_factorization,
        dsimp,
        have monotone_f : monotone f.to_preorder_hom.to_fun := f.to_preorder_hom.monotone,
        exact monotone_f a_le_b,
        })⟩)

instance epi_component_is_epi {x y : simplex_category} (f : x ⟶ y) : epi (epi_component f) := begin
  have e_surj : function.surjective (epi_component f).to_preorder_hom := by {
        apply function.surjective.comp,
        exact (image.f_to_range_f_inv f).symm.surjective,
        exact set.surjective_onto_range,
      },
      exact epi_iff_function_is_surjective.elim_right e_surj
end

def mono_component {x y : simplex_category} (f : x ⟶ y) : ([image.range_nb f] ⟶ y) := hom.mk ⟨
  (order_embedding.subtype (set.range (f.to_preorder_hom.to_fun))) ∘ (image.f_to_range_f_inv f).to_order_embedding,
    monotone.comp (order_embedding.subtype (set.range (f.to_preorder_hom.to_fun))).monotone (image.f_to_range_f_inv f).to_order_embedding.monotone 
  ⟩

instance mono_component_is_mono {x y : simplex_category} (f: x ⟶ y) : mono (mono_component f) := begin
      rw [mono_iff_function_is_injective, mono_component],
      simp [hom.to_preorder_hom_mk],
      apply function.injective.comp,
      exact subtype.coe_injective,
      exact (image.f_to_range_f_inv f).to_order_embedding.injective
end

lemma epi_mono_factorization_is_factorization {x y : simplex_category} (f : x ⟶ y) : f = (epi_component f) ≫ (mono_component f) := begin 
  dsimp,
    apply hom.ext,
    rw hom.to_preorder_hom_mk,
    apply preorder_hom.ext,
    rw [preorder_hom.comp_coe, epi_component, mono_component],
    simp,
    conv {
      to_rhs,
      erw function.comp.assoc,
      congr, skip,
    },
    ext,
    rw [function.comp_apply, function.comp_apply, function.comp_apply, order_iso.apply_symm_apply],
    refl,
end

lemma epi_mono_factorization {x y : simplex_category} {f : x ⟶ y} : ∃! (z : simplex_category) (m : z ⟶ y) (e : x ⟶ z) (m_mono : category_theory.mono m) (e_epi: category_theory.epi e), (f = e ≫ m) := begin
  split, rotate, exact [image.range_nb f],
  split,
  use (mono_component f),
  split,
  use (epi_component f),
  split,
  use epi_mono.mono_component_is_mono f,
  split,
  use (epi_mono.epi_component_is_epi f),
  split,
  exact epi_mono_factorization_is_factorization f,
  {intro e_1, simp},
  {intro m_1,simp},
  {
    intro e_2, simp,
    intros mono_m_f epi_e_2 hyp,
    have comp_eg : e_2 ≫ (mono_component f) = (epi_component f) ≫ (mono_component f) := by{
      rw ←epi_mono_factorization_is_factorization f,
      conv_rhs {rw hyp},
      simp,
    },
    apply mono_m_f.right_cancellation,
    exact comp_eg,
  },
  {
    intro m_2,
    simp,
    intro hyp,
    cases hyp with e H,
    simp at H,
    cases H, cases H_left, cases H_left_right,
    rename H_left_left mono_m_2,
    rename H_left_right_left epi_e,
    rename H_left_right_right hyp_comp_1,
    rename H_right unicity_e,
    apply hom.ext,
    apply preorder_hom.ext,
    apply fin.strict_mono_unique,
    exact strict_mono_of_monotone_of_injective ((hom.to_preorder_hom m_2).monotone) (mono_iff_function_is_injective.elim_left mono_m_2),
    have aux := strict_mono_of_monotone_of_injective ((hom.to_preorder_hom (mono_component f)).monotone) (mono_iff_function_is_injective.elim_left (epi_mono.mono_component_is_mono f)),
    exact aux, -- for some reason, a direct exact did not work. 

    -- Basically a whole block to prove that the range of m_2 is the range of f
    apply_fun hom.to_preorder_hom at hyp_comp_1,
    apply_fun preorder_hom.to_fun at hyp_comp_1,
    rw [preorder_hom.to_fun_eq_coe, preorder_hom.to_fun_eq_coe] at hyp_comp_1,
    rw hom.to_preorder_hom_mk at hyp_comp_1,
    rw preorder_hom.comp_coe at hyp_comp_1,
    apply_fun set.range at hyp_comp_1,
    conv at hyp_comp_1 {to_rhs, rw set.range_comp},
    rw function.surjective.range_eq (epi_iff_function_is_surjective.elim_left epi_e) at hyp_comp_1,
    rw set.image_univ at hyp_comp_1,
    -- Now the same to prove that the range of mono_component f is the range of f
    have hyp_comp_2 := epi_mono_factorization_is_factorization f,
    apply_fun hom.to_preorder_hom at hyp_comp_2,
    apply_fun preorder_hom.to_fun at hyp_comp_2,
    rw [preorder_hom.to_fun_eq_coe, preorder_hom.to_fun_eq_coe] at hyp_comp_2,
    dsimp at hyp_comp_2,
    rw hom.to_preorder_hom_mk at hyp_comp_2,
    rw preorder_hom.comp_coe at hyp_comp_2,
    apply_fun set.range at hyp_comp_2,
    conv at hyp_comp_2 {to_rhs, rw set.range_comp},
    rw function.surjective.range_eq (epi_iff_function_is_surjective.elim_left (epi_mono.epi_component_is_epi f)) at hyp_comp_2,
    rw set.image_univ at hyp_comp_2,
    -- Now just to piece it together
    rw ←hyp_comp_1,
    rw ←hyp_comp_2, 
  },
  {
    intros z h_z,
    cases h_z with m H,
    cases H with H_1 unicity_m,
    cases H_1 with e H_e,
    cases H_e with H_3 unicity_e,
    cases H_3 with m_mono H_4,
    cases H_4 with H_5 unicity_mono_m,
    cases H_5 with epi_e H_6,
    cases H_6 with hyp_comp unicity_epi_e,
    suffices H : z.len = image.range_nb f, rw [← mk_len z, H],
    -- On prouve encore que la range de la mono_comp de f est la range de f... 
    have hyp_comp_1 := hyp_comp,
    apply_fun hom.to_preorder_hom at hyp_comp_1,
    apply_fun preorder_hom.to_fun at hyp_comp_1,
    rw [preorder_hom.to_fun_eq_coe, preorder_hom.to_fun_eq_coe] at hyp_comp_1,
    dsimp at hyp_comp_1,
    rw hom.to_preorder_hom_mk at hyp_comp_1,
    rw preorder_hom.comp_coe at hyp_comp_1,
    apply_fun set.range at hyp_comp_1,
    conv at hyp_comp_1 {to_rhs, rw set.range_comp},
    rw function.surjective.range_eq (epi_iff_function_is_surjective.elim_left epi_e) at hyp_comp_1,
    rw set.image_univ at hyp_comp_1,
    set m_range := set.range_factorization ⇑(hom.to_preorder_hom m) with def_m_range,
    have m_range_surj : function.surjective m_range := by {
      rw def_m_range,
      exact set.surjective_onto_range,
    },
    have m_inj := mono_iff_function_is_injective.elim_left m_mono,
    have m_range_inj : function.injective m_range := by { 
      intros a b h,
      rw def_m_range at h,
      rw set.range_factorization at h,
      dsimp at h,
      rw subtype.ext_iff_val at h,
      dsimp at h,
      refine m_inj h,
    },
    have m_range_bij : function.bijective m_range :=  ⟨m_range_inj, m_range_surj⟩,
    have card_eq := ((fintype.bijective_iff_surjective_and_card m_range).elim_left m_range_bij).right,
    apply_fun (λ n: ℕ, n-1) at card_eq,
    conv at card_eq {
      to_lhs,
      simp,
    },
    have eq_image_nb : (image.range_nb f = image.range_nb m) := image.same_range_implies_same_range_nb hyp_comp_1,
    rw eq_image_nb,
    rw image.range_nb,
    rw preorder_hom.to_fun_eq_coe,
    exact card_eq,
  }
end 


end epi_mono

end simplex_category