Library UniMath.ModelCategories.WFS

Weak Factorization Systems
Weak Factorization Systems (WFSs) form the foundation of model category theory. They describe interacting morphism classes, connected by a dual lifting property. We define the notion of WFS, as well as some basic properties that they have.
We found that some properties that we would like a WFS to have (closedness under arbitrary coproducts or transfinite compotisition) relies on the Axiom of Choice.
Important sources:
  • More Concise Algebraic Topology (MCAT)
  • My thesis: https://studenttheses.uu.nl/handle/20.500.12932/45658
  • nlab: https://ncatlab.org/nlab/show/weak+factorization+system
Contents:
  • Definition of lifting property
  • Definition of WFS
  • Properties of WFS (Left Saturatedness)

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Pushouts.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.Limits.Opp.

Require Import UniMath.CategoryTheory.Chains.Chains.

Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.
Require Import UniMath.ModelCategories.Retract.
Require Import UniMath.ModelCategories.MorphismClass.
Require Import UniMath.ModelCategories.Lifting.

Local Open Scope cat.
Local Open Scope morcls.
Local Open Scope retract.

Section wfs.

Any map can be factored through maps in L and R
Definition wfs_fact_ax {C : category} (L R : morphism_class C) :=
  ∏ x y (f : x --> y),
    ∃ ef (l : x --> ef) (r : ef --> y),
      (L _ _) l × (R _ _) r × l · r = f.

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL27
Definition is_wfs {C : category} (L R : morphism_class C) :=
  (L = llp R) × (R = rlp L) × (wfs_fact_ax L R).

Definition make_is_wfs {C : category} {L R : morphism_class C}
    (llp : L = llp R) (rlp : R = rlp L) (fact : wfs_fact_ax L R) : is_wfs L R :=
  make_dirprod llp (make_dirprod rlp fact).

Definition wfs (C : category) :=
  ∑ (L R : morphism_class C), is_wfs L R.

Definition make_wfs {C : category} (L R : morphism_class C) (w : is_wfs L R) : wfs C :=
  tpair _ L (tpair _ R w).

Definition wfs_L {C : category} (w : wfs C) := (pr1 w).
Definition wfs_R {C : category} (w : wfs C) := pr1 (pr2 w).
Definition is_wfs_llp {C : category} {L R : morphism_class C} (w : is_wfs L R) := pr1 w.
Definition is_wfs_rlp {C : category} {L R : morphism_class C} (w : is_wfs L R) := pr1 (pr2 w).
Definition is_wfs_fact {C : category} {L R : morphism_class C} (w : is_wfs L R) := pr2 (pr2 w).
Definition wfs_is_wfs {C : category} (w : wfs C) := pr2 (pr2 w).
Definition wfs_llp {C : category} (w : wfs C) := is_wfs_llp (wfs_is_wfs w).
Definition wfs_rlp {C : category} (w : wfs C) := is_wfs_rlp (wfs_is_wfs w).
Definition wfs_fact {C : category} (w : wfs C) := is_wfs_fact (wfs_is_wfs w).

Lemma isaprop_is_wfs {C : category} (L R : morphism_class C) :
    isaprop (is_wfs L R).
Show proof.
  apply isapropdirprod.
  - unfold isaprop.
    exact (isasetmorphism_class _ _).
  - apply isapropdirprod.
    * exact (isasetmorphism_class _ _).
    * do 3 (apply impred_isaprop; intro).
      apply propproperty.

Context {C : category}.

Can't do dot notation like in lean (is_wfs.lp) any two maps in a wfs have the lifting property with respect to each other https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL33
Lemma wfs'lp (w : wfs C)
    {x y a b} {f : x --> y} {g : a --> b}
    (hf : (wfs_L w _ _) f) (hg : (wfs_R w _ _) g) :
  lp f g.
Show proof.
  unfold wfs_L in hf.
  rewrite (wfs_llp w) in hf.
  exact (hf _ _ _ hg).

if f' is a retract of f and f is in L for some WFS, then so is f' proposition 14.1.13 in More Concise AT https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL40
Lemma wfs_L_retract (w : wfs C)
    {x y x' y' : C} {f : x --> y} {f' : x' --> y'}
    (r : retract f f') (hf : (wfs_L w _ _) f) :
  (wfs_L w _ _) f'.
Show proof.
  destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].

  unfold wfs_L.
  rewrite (wfs_llp w).
  intros a b g hg h k s.
  use (wfs'lp w hf hg (h ∘ ra) (k ∘ rb) _).
  {
    rewrite <- assoc, s, assoc, assoc, hr.
    reflexivity.
  }
  
  intro hl.
  destruct hl as [l [hlh hlk]].

  apply hinhpr.
  exists (l ∘ ib).
  split.
  * rewrite assoc, <- hi, <- assoc, hlh, assoc, ha, id_left.
    reflexivity.
  * rewrite <- assoc, hlk, assoc, hb, id_left.
    reflexivity.

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL52 Lemma 14.1.9 in MCAT
Lemma llp_rlp_self (L : morphism_class C) : L ⊆ llp (rlp L).
Show proof.
  intros a b f hf x y g hg.
  apply (hg _ _ _).
  exact hf.

no counterpart in lean
Lemma rlp_llp_self (L : morphism_class C) : L ⊆ rlp (llp L).
Show proof.
  intros a b f hf x y g hg.
  apply (hg _ _ _).
  exact hf.

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL55 No counterpart in MCAT, (□(I□), I□) is a WFS
Lemma wfs_of_factorization (I : morphism_class C)
    (h : ∏ (x y : C) (f : x --> y), ∃ z (g : x --> z) (h : z --> y), (llp (rlp I) _ _ g) × (rlp I _ _ h) × (h ∘ g = f)) :
  is_wfs (llp (rlp I)) (rlp I).
Show proof.
  use make_is_wfs.
  - trivial.
  - apply morphism_class_subset_antisymm; intros x y g hg.
    * exact (rlp_llp_self _ _ _ _ hg).
    * intros a b f hf.
      apply (hg _ _ _).
      exact (llp_rlp_self _ _ _ _ hf).
  - exact h.

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL67 same name as Lemma 14.1.12 in MCAT, but a different phrasing In MCAT, the statement is in reference of a single morphism, not a whole class
Lemma retract_argument {L' : morphism_class C} (w : wfs C)
    (H : wfs_fact_ax L' (wfs_R w)) :
  ∏ {x y} (f : x --> y),
    (wfs_L w _ _) f
    -> ∃ {x' y'} (f' : x' --> y') (r : retract f' f), (L' _ _) f'.
Show proof.
  intros x y f hf.

  specialize (H _ _ f) as eHf.
  simpl in eHf.
  use (hinhuniv _ eHf).
  intro Hf.
  destruct Hf as [z [g [h [hg [hh hgh]]]]].

  use (wfs'lp w hf hh g (identity _)).
  {
    rewrite hgh, id_right.
    reflexivity.
  }
  intro hl.
  destruct hl as [l [hl1 hl2]].

  assert (r : retract g f).
  {
    use (make_retract (identity _) (identity _) l h).
    use make_is_retract.
    - now rewrite id_left.
    - assumption.
    - rewrite id_left. now symmetry.
    - rewrite id_left. now symmetry.
  }

  
  apply hinhpr.

  exists x, z, g, r.
  exact hg.

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL82
Lemma lp_isos_univ {x y a b : C} (f : x --> y) (g : a --> b) :
  (morphism_class_isos C _ _ f) -> lp f g.
Show proof.
  intro H.
  set (fiso := make_iso _ H).
  change (lp fiso g).

  intros h k s.
  apply hinhpr.
  exists (h ∘ (inv_from_iso fiso)).
  split.
  * rewrite assoc, iso_inv_after_iso, id_left.
    reflexivity.
  * rewrite <- assoc, s, assoc.
    rewrite iso_after_iso_inv, id_left.
    reflexivity.

Lemma lp_univ_isos {x y a b : C} (f : x --> y) (g : a --> b) :
  (morphism_class_isos C _ _ f) -> lp g f.
Show proof.
  intro H.
  set (fiso := make_iso _ H).
  change (lp g fiso).

  intros h k s.
  apply hinhpr.
  exists ((inv_from_iso fiso) ∘ k).
  split.
  * rewrite assoc, <- s, <- assoc, iso_inv_after_iso, id_right.
    reflexivity.
  * rewrite <- assoc, iso_after_iso_inv, id_right.
    reflexivity.

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL91
Lemma llp_univ : llp (morphism_class_univ C) = morphism_class_isos C.
Show proof.
  apply morphism_class_subset_antisymm; intros x y f H.
  -
    specialize ((H _ _ f) tt).
    use (H (identity _) (identity _)).
    {
      
      rewrite id_left, id_right.
      reflexivity.
    }
    
    intro hl.
    destruct hl as [l [hfl hlf]].
    unfold morphism_class_isos.

    assert (is_z_isomorphism f) as f_z_iso.
    {
      exists l.
      split; assumption.
    }
    
    apply is_iso_from_is_z_iso.
    exact f_z_iso.
  - intros a b g _.
    exact (lp_isos_univ f g H).

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL101
Lemma rlp_isos : rlp (morphism_class_isos C) = morphism_class_univ C.
Show proof.
  apply morphism_class_subset_antisymm.
  -
    intros x y g H.
    unfold morphism_class_univ.
    exact tt.
  -
    rewrite <- llp_univ.
    exact (rlp_llp_self _).

https://github.com/rwbarton/lean-model-categories/blob/e366fccd9aac01154da9dd950ccf49524f1220d1/src/category_theory/model/wfs.leanL109
Lemma wfs_isos_univ : is_wfs (morphism_class_isos C) (morphism_class_univ C).
Show proof.
  use make_is_wfs; try symmetry.
  - exact llp_univ.
  - exact rlp_isos.
  -
    intros x y f.
    apply hinhpr.
    exists x, (identity x), f.

    repeat split.
    * exact (identity_is_iso C x).
    * rewrite id_left.
      reflexivity.

Definition opp_is_wfs {L R : morphism_class C} (w : is_wfs L R) :
    is_wfs (morphism_class_opp R) (morphism_class_opp L).
Show proof.
  use make_is_wfs.
  - rewrite (is_wfs_rlp w).
    exact (opp_rlp_is_llp_opp _).
  - rewrite (is_wfs_llp w).
    exact (opp_llp_is_rlp_opp _).
  - intros x y f.
    specialize ((is_wfs_fact w) _ _ (rm_opp_mor f)) as H.
    use (hinhuniv _ H).
    clear H; intro H.
    destruct H as [z [g [h [? [? ?]]]]].
    apply hinhpr.
    exists (opp_ob z), (opp_mor h), (opp_mor g).
    repeat split; assumption.

Definition opp_wfs (w : wfs C) : wfs (op_cat C).
Show proof.
  exists (morphism_class_opp (wfs_R w)), (morphism_class_opp (wfs_L w)).
  exact (opp_is_wfs (wfs_is_wfs w)).

End wfs.

Section properties.

Lemma wfs_L_contains_isos {C : category} (w : wfs C) :
    (morphism_class_isos C) ⊆ (wfs_L w).
Show proof.
  rewrite <- llp_univ.
  unfold wfs_L.
  rewrite (wfs_llp w).

  apply llp_anti.
  intros x y f hf.
  exact tt.

Dual statement
Lemma wfs_R_contains_isos {C : category} (w : wfs C) :
    (morphism_class_isos C) ⊆ (wfs_R w).
Show proof.
  intros x y f hf.
  set (opp_containment := wfs_L_contains_isos (opp_wfs w)).
  exact (opp_containment _ _ (opp_mor f) (opp_is_iso _ hf)).

Dual statement of wfs_L_retract
Lemma wfs_R_retract {C : category} (w : wfs C)
    {a b a' b'} {f : a --> b} {f' : a' --> b'}
    (r : retract f f') (hf : (wfs_R w _ _) f) :
  (wfs_R w _ _) f'.
Show proof.
  use (wfs_L_retract (opp_wfs w) (opp_retract r)).
  exact hf.

https://ncatlab.org/nlab/show/weak+factorization+systemClosuredPropertiesOfWeakFactorizationSystem
Lemma wfs_closed_pullbacks {C : category} (w : wfs C)
    {x y z : C} {p : x --> y} {f : z --> y}
    (Pb : Pullback f p) :
  ((wfs_R w _ _) p) -> ((wfs_R w _ _) (PullbackPr1 Pb)).
Show proof.
  intro p_r.

  destruct Pb as [[zfx [f'p p2]] [H isPb]].
  simpl in *.
  cbn.

  unfold wfs_R.
  rewrite (wfs_rlp w).
  intros a b i i_l.

  intros p1 g Hp1g.


  unfold wfs_R in p_r.
  rewrite (wfs_rlp w) in p_r.

  use (p_r _ _ i i_l (p2 ∘ p1) (f ∘ g) _).
  {
    rewrite <- assoc, <- H, assoc, Hp1g, assoc.
    reflexivity.
  }

  
  intro hl.
  destruct hl as [l [hl1 hl2]].
  symmetry in hl2.

  destruct (isPb _ g l hl2) as [[gh [hgh1 hgh2]] _].

  apply hinhpr.
  exists gh.
  split.
  -
    apply (MorphismsIntoPullbackEqual isPb).
    * rewrite <-assoc, hgh1, Hp1g.
      reflexivity.
    * rewrite <- assoc, hgh2, hl1.
      reflexivity.
  -
    exact hgh1.

Dual statement
Lemma wfs_closed_pushouts {C : category} (w : wfs C)
    {x y z : C} {p : x --> y} {f : x --> z}
    (Po : Pushout f p) :
  ((wfs_L w _ _) p) -> ((wfs_L w _ _) (PushoutIn1 Po)).
Show proof.
  apply (wfs_closed_pullbacks (opp_wfs _)).

https://ncatlab.org/nlab/show/weak+factorization+systemClosuredPropertiesOfWeakFactorizationSystem map between coproducts is in L if all arrows between objects in coproduct are
Lemma wfs_closed_coproducts {C : category} {I : hSet} (w : wfs C)
    {a b : I -> C}
    {f : ∏ (i : I), a i --> b i} (hf : ∀ (i : I), (wfs_L w _ _) (f i))
    (CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b)
    (aoc : AxiomOfChoice) :
  (wfs_L w _ _) (CoproductOfArrows _ _ CCa CCb f).
Show proof.
  unfold wfs_L in *.
  rewrite (wfs_llp w) in *.
  intros x y g hg.
  intros h k s.

  set (hi := λ i, (CoproductIn _ _ CCa i) · h).
  set (ki := λ i, (CoproductIn _ _ CCb i) · k).

  assert (∏ i, ∃ li, ((f i) · li = hi i) × (li · g = ki i)) as ilift.
  {
    intro i.
    specialize (hf i _ _ g hg) as H.
    specialize (H (hi i) (ki i)).

    use H.

    unfold hi, ki.
    rewrite <- assoc, s, assoc, assoc.
    now rewrite (CoproductOfArrowsIn _ _).
  }

  
  assert (∥∏ i, ∑ li, ((f i) · li = hi i) × (li · g = ki i)∥) as ilift_aoc.
  {
    set (aocI := aoc I).
    simpl in aocI.
    apply (aocI).
    exact ilift.
  }

  
  assert (∃ (li : (∏ i, (b i --> x))), (∏ i, (f i) · (li i) = hi i × ((li i) · g = ki i))) as ilifts.
  {
    use (hinhuniv _ ilift_aoc).
    intro ilift_aoc_sig.
    apply hinhpr.

    use tpair.
    - intro i.
      set (li := ilift_aoc_sig i).
      destruct li as [l hl].
      exact l.
    - intro i.
      set (li := ilift_aoc_sig i).
      simpl.
      destruct li as [l hl].
      exact hl.
  }

  use (hinhuniv _ ilifts).
  intro ilift_sig.
  destruct ilift_sig as [li hli].

  set (hl := isCoproduct_Coproduct _ _ CCb x li).
  destruct hl as [[l hl] uniqueness].

  apply hinhpr.
  exists l.
  split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l).
  -
    rewrite (precompWithCoproductArrow).

    apply CoproductArrowUnique.

    intro i.
    rewrite CoproductInCommutes.

    destruct (hli i) as [hlicomm _].

    change (CoproductIn _ _ _ _ · h) with (hi i).
    rewrite (hl i).
    exact hlicomm.
  -
    apply CoproductArrowUnique.

    intro i.
    rewrite assoc.
    rewrite CoproductInCommutes.

    destruct (hli i) as [_ klicomm].

    change (CoproductIn _ _ _ _ · k) with (ki i).
    rewrite (hl i).
    exact klicomm.

Dual statement
Lemma wfs_closed_products {C : category} {I : hSet} (w : wfs C)
    {a b : I -> C} {f : ∏ (i : I), b i --> a i}
    (hf : ∀ (i : I), (wfs_R w _ _) (f i))
    (CCa : Product _ _ a) (CCb : Product _ _ b)
    (aoc : AxiomOfChoice) :
  (wfs_R w _ _) (ProductOfArrows _ _ CCa CCb f).
Show proof.
  apply (wfs_closed_coproducts (opp_wfs w)).
  - exact hf.
  - exact aoc.


(i) wfs<X>contains_isos (ii) wfs<X>retract (iii) wfs_closed<co>products (iv) wfs_closed<pushouts|pullbacks> (v) wfs_closed_transfinite_composition
prove that L is left saturated, and R is right saturated in a WFS or lemma 14.1.8

Lemma llp_iff_lift_with_R {C : category} (w : wfs C) {x y : C} (f : x --> y)
  (H : ∑ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f) :
    lp (pr12 H) f <-> (wfs_R w _ _) f.
Show proof.
  destruct H as [z [g [h [Lg [Rh Hgh]]]]].

  split.
  - intro hf.
    unfold wfs_R.
    rewrite (wfs_rlp w).

    intros a b g' hg'.
    intros top bottom comm_total.

    use (hf (identity _) h).
    {
      rewrite id_left.
      apply pathsinv0.

      exact (Hgh).
    }
    intro h'.
    destruct h' as [lift_lff [comm_lff1 comm_lff2]].

    assert (lp g' h) as lp_grf.
    {
      set (rf_r := Rh).
      unfold wfs_R in rf_r.
      rewrite (wfs_rlp w) in rf_r.
      exact (rf_r _ _ g' hg').
    }

    
    use (lp_grf (g ∘ top) bottom).
    {
      rewrite <- assoc.
      rewrite (Hgh).
      exact comm_total.
    }

    intro H.
    destruct H as [lift_grf [comm_grf1 comm_grf2]].

    apply hinhpr.
    exists (lift_lff ∘ lift_grf).

    split.
    * etrans. apply assoc.
      etrans. apply cancel_postcomposition.
              exact comm_grf1.
      etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              exact comm_lff1.
      apply id_right.
    * etrans. apply assoc'.
      etrans. apply cancel_precomposition.
              exact comm_lff2.
      exact comm_grf2.
  -
    intro hf.
    intros h' k Hk.

    unfold wfs_R in hf.
    rewrite wfs_rlp in hf.
    use hf.
    exact (Lg).

End properties.