Retract of weak equivalences is a weak equivalence

src/category_theory/model/category.lean

@@ -19,14 +19,75 @@ structure is_model_category (W C F : morphism_class M) : Prop :=
 -- TODO: Show that it follows that W is closed under retracts. See
 -- https://ncatlab.org/nlab/show/model+category#ClosureOfMorphisms
 
+lemma is_model_category.weq_of_weq_retract_fib { W C F : morphism_class M } ( h : is_model_category W C F )
+ {a b a' b'} {f : a ⟶ b} {f' : a' ⟶ b'} (r : retract f f') (hf : W f) (hf': F f') : W f' := begin
+   rcases h.acf.fact f with ⟨ c, α, β, WCα, Fβ, f_fact ⟩,
+   rw h.acf.llp at WCα,
+   choose l hl using WCα hf' r.ra (β ≫ r.rb) (by { rw [← category.assoc, f_fact], exact r.hr }), 
+   have rβf' : retract β f' := {
+     ia := (r.ia) ≫ α,
+     ra := l,
+     ib := r.ib,
+     rb := r.rb,
+     ha := by { simp, rw hl.1, exact r.ha },
+     hb := r.hb,
+     hi := by { rw [category.assoc, f_fact], exact r.hi },
+     hr := hl.2,
+   },
+   rw ← h.acf.llp at WCα,
+   rw ← f_fact at hf,
+   exact (is_wfs.retract_right h.caf rβf' ⟨ Fβ, h.weq.weq_cancel_left WCα.2 hf ⟩).2
+end
+
+#check @Is_pushout.uniqueness
+
+lemma is_model_category.weq_of_weq_retract { W C F : morphism_class M } [ @has_pushouts M 𝓜] ( h : is_model_category W C F )
+ {a b a' b'} {f : a ⟶ b} {f' : a' ⟶ b'} (r : retract f f') (hf : W f) : W f' := begin
+   rcases h.acf.fact f' with ⟨ c, α, β, WCα, Fβ, f'_fact ⟩,
+   cases has_pushouts.pushout α r.ia with z γ δ po,
+   have WCδ : (C ∩ W) δ := by { rw h.acf.llp, rw h.acf.llp at WCα, exact llp_pushout F po WCα },
+   have uq := @Is_pushout.uniqueness M 𝓜 a' c a z α r.ia γ δ po,
+   have rεβ : retract (po.induced (β ≫ r.ib) f (by { rw [← category.assoc, f'_fact], exact r.hi.symm})) β := {
+     ia := γ,
+     ra := po.induced (𝟙 c) (r.ra ≫ α) (by { rw [category.comp_id, ← category.assoc, r.ha, category.id_comp] }),
+     ib := r.ib,
+     rb := r.rb,
+     ha := by simp,
+     hb := r.hb,
+     hi := by simp,
+     hr := by { 
+      refine uq _ _, 
+      rw [← category.assoc,
+          Is_pushout.induced_commutes₀ po _ _ _,
+          ← category.assoc, 
+          Is_pushout.induced_commutes₀ po _ _ _, 
+          category.assoc,
+          category.id_comp,
+          r.hb,
+          category.comp_id],
+      rw [← category.assoc,
+          Is_pushout.induced_commutes₁ po _ _ _,
+          ← category.assoc,
+          Is_pushout.induced_commutes₁ po _ _ _,
+          category.assoc,
+          f'_fact,
+          r.hr],
+      }
+    },
+   rw ← f'_fact,
+   apply h.weq.weq_comp a' c b' α β WCα.2,
+   refine is_model_category.weq_of_weq_retract_fib h rεβ _ Fβ,
+   apply h.weq.weq_cancel_left WCδ.2,
+   rw Is_pushout.induced_commutes₁ po _ _ _,
+   assumption,
+end
+
 omit 𝓜
 class model_category (M : Type u) extends category.{v} M :=
 (complete : has_limits M)
 (cocomplete : has_colimits M)
 (W C F : morphism_class M)
 (h : is_model_category W C F)
-
-variables {M}
 include 𝓜
 
 /-- We can skip checking the condition C ∩ W ⊆ AC. Compare Hirschhorn, Theorem 11.3.1. -/
@@ -63,7 +124,7 @@ begin
   have : retract g f,
   { refine ⟨𝟙 a, 𝟙 a, l, h, _, _, _, _⟩,
     all_goals { tidy } },
-  exact acf.retract this g_ac
+  exact acf.retract_left this g_ac
 end
 
 def model_category.mk' [has_limits M] [has_colimits M] {W C AF AC F : morphism_class M}

src/category_theory/model/wfs.lean

@@ -2,6 +2,7 @@ import category_theory.morphism_class_closure
 import category_theory.retract
 import category_theory.colimits
 import category_theory.transfinite.composition
+import category_theory.opposites
 import logic.crec
 
 universes v u
@@ -30,14 +31,15 @@ structure is_wfs (L R : morphism_class M) : Prop :=
 (fact : ∀ {x y} (f : x ⟶ y), ∃ z (g : x ⟶ z) (h : z ⟶ y),
   L g ∧ R h ∧ g ≫ h = f)
 
+
 lemma is_wfs.lp {L R : morphism_class M} (w : is_wfs L R)
   {a b x y} {f : a ⟶ b} {g : x ⟶ y} (hf : L f) (hg : R g) : lp f g :=
 begin
   rw w.llp at hf,
   exact hf hg
 end
 
-lemma is_wfs.retract {L R : morphism_class M} (w : is_wfs L R)
+lemma is_wfs.retract_left {L R : morphism_class M} (w : is_wfs L R)
   {a b a' b'} {f : a ⟶ b} {f' : a' ⟶ b'} (r : retract f f') (hf : L f) : L f' :=
 begin
   rw w.llp,
@@ -47,6 +49,18 @@ begin
   refine ⟨r.ib ≫ l, _, _⟩,
   { rw [←category.assoc, ←r.hi, category.assoc, hl₁, ←category.assoc, r.ha, category.id_comp] },
   { rw [category.assoc, hl₂, ←category.assoc, r.hb, category.id_comp] }
+end    
+
+lemma is_wfs.retract_right {L R :morphism_class M } (w : is_wfs L R)
+{a b a' b'} {f : a ⟶ b} {f' : a' ⟶ b'} (r : retract f f') (hf : R f) : R f' :=
+begin
+  rw w.rlp,
+  intros x y g hg h k s,
+  rcases w.lp hg hf (h ≫ r.ia) (k ≫ r.ib) 
+    (by rw [← category.assoc, ←s, category.assoc, category.assoc, r.hi]) with ⟨l, hl₁, hl₂⟩,
+  refine ⟨l ≫ r.ra, _, _⟩,
+  { rw [←category.assoc, hl₁, category.assoc, r.ha, category.comp_id] },
+  { rw [category.assoc, r.hr, ←category.assoc, hl₂, category.assoc, r.hb, category.comp_id] }
 end
 
 lemma llp_rlp_self (L : morphism_class M) : L ⊆ llp (rlp L) :=

src/category_theory/morphism_class.lean

@@ -1,6 +1,7 @@
 import category_theory.category
 import category_theory.isomorphism
 import category_theory.eq_to_hom
+import category_theory.opposites
 
 universes v v' u u'
 
@@ -16,6 +17,8 @@ instance : has_inter (morphism_class C) := ⟨λ I J X Y f, I f ∧ J f⟩
 
 instance : has_subset (morphism_class C) := ⟨λ I J, ∀ ⦃X Y⦄ ⦃f : X ⟶ Y⦄, I f → J f⟩
 
+def morphism_class.op (I : morphism_class C) : morphism_class Cᵒᵖ := λ Y X f, I f
+
 def morphism_class.univ : morphism_class C := λ X Y f, true
 
 def morphism_class.isos : morphism_class C := λ X Y f, nonempty (is_iso f)