From 048e3ff1269d88f0264010adabd0b32c52303da7 Mon Sep 17 00:00:00 2001
From: Saul Glasman <saulglasman0@gmail.com>
Date: Tue, 27 Oct 2020 16:11:56 -0400
Subject: [PATCH 1/4] Op...

---
 src/category_theory/model/category.lean | 20 ++++++++++++++++++++
 src/category_theory/model/wfs.lean      | 18 +++++++++++++++++-
 src/category_theory/morphism_class.lean |  3 +++
 src/category_theory/retract.lean        |  2 +-
 4 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/src/category_theory/model/category.lean b/src/category_theory/model/category.lean
index 1d288c9..cc5215b 100644
--- a/src/category_theory/model/category.lean
+++ b/src/category_theory/model/category.lean
@@ -19,6 +19,26 @@ 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 ⟨ Fβ, h.weq.weq_cancel_left WCα.2 hf ⟩,
+end
+
 omit 𝓜
 class model_category (M : Type u) extends category.{v} M :=
 (complete : has_limits M)
diff --git a/src/category_theory/model/wfs.lean b/src/category_theory/model/wfs.lean
index fb21d37..2fcf141 100644
--- a/src/category_theory/model/wfs.lean
+++ b/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,6 +31,21 @@ 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 llp.op (R : morphism_class M) : morphism_class.op M (llp R) = rlp (morphism_class.op M R) :=
+begin
+  unfold morphism_class.op,
+  ext,
+  split,
+  intros g p q d e f g h,
+end 
+
+lemma is_wfs.op { L R : morphism_class M } ( w: is_wfs L R ) : @is_wfs Mᵒᵖ infer_instance (morphism_class.op M R) (morphism_class.op M L) := 
+{
+  llp := by { unfold morphism_class.op, tidy; rw w.rlp at *,},
+  rlp := by { sorry },
+  fact := by { sorry }
+}
+
 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
@@ -47,7 +63,7 @@ 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
+end    
 
 lemma llp_rlp_self (L : morphism_class M) : L ⊆ llp (rlp L) :=
 λ a b f hf x y g hg, hg hf
diff --git a/src/category_theory/morphism_class.lean b/src/category_theory/morphism_class.lean
index 24af4c0..ed04f1c 100644
--- a/src/category_theory/morphism_class.lean
+++ b/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)
diff --git a/src/category_theory/retract.lean b/src/category_theory/retract.lean
index 0fba5fe..c8299e8 100644
--- a/src/category_theory/retract.lean
+++ b/src/category_theory/retract.lean
@@ -11,7 +11,7 @@ universes v v' u u'
 variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
---- `retract f f'` is a diagram exhibiting f' as a retract of f.
+-- `retract f f'` is a diagram exhibiting f' as a retract of f.
 structure retract {a b a' b' : C} (f : a ⟶ b) (f' : a' ⟶ b') : Type v :=
 (ia : a' ⟶ a) (ra : a ⟶ a')
 (ib : b' ⟶ b) (rb : b ⟶ b')

From 6d9dd44a0cc818e04d0d70905f947e76ec2dc109 Mon Sep 17 00:00:00 2001
From: Saul Glasman <saulglasman0@gmail.com>
Date: Fri, 6 Nov 2020 16:12:21 -0500
Subject: [PATCH 2/4] Proof

---
 src/category_theory/model/category.lean | 54 +++++++++++++++++++++++--
 src/category_theory/model/wfs.lean      | 28 ++++++-------
 2 files changed, 64 insertions(+), 18 deletions(-)

diff --git a/src/category_theory/model/category.lean b/src/category_theory/model/category.lean
index cc5215b..5a4be64 100644
--- a/src/category_theory/model/category.lean
+++ b/src/category_theory/model/category.lean
@@ -36,7 +36,50 @@ lemma is_model_category.weq_of_weq_retract_fib { W C F : morphism_class M } ( h
    },
    rw ← h.acf.llp at WCα,
    rw ← f_fact at hf,
-   --exact is_wfs.retract ⟨ Fβ, h.weq.weq_cancel_left WCα.2 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,
+   refine h.weq.weq_comp a' c b' α β WCα.2 _,
+   refine is_model_category.weq_of_weq_retract_fib h rεβ _ Fβ,
+   refine h.weq.weq_cancel_left WCδ.2 _,
+   rw Is_pushout.induced_commutes₁ po _ _ _,
+   assumption,
 end
 
 omit 𝓜
@@ -46,7 +89,12 @@ class model_category (M : Type u) extends category.{v} M :=
 (W C F : morphism_class M)
 (h : is_model_category W C F)
 
-variables {M}
+-- variables { C: Type u } [mc: model_category C] {a b : C} { f: a ⟶ b }
+-- lemma model_category.weq_of_weq_retract { C: Type u } [mc: model_category C]
+--  {a b a' b' : C} {f : a ⟶ b} {f' : a' ⟶ b'} (r : retract f f') ( hf : W f ) : W f' := 
+-- begin
+  
+-- end
 include 𝓜
 
 /-- We can skip checking the condition C ∩ W ⊆ AC. Compare Hirschhorn, Theorem 11.3.1. -/
@@ -83,7 +131,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}
diff --git a/src/category_theory/model/wfs.lean b/src/category_theory/model/wfs.lean
index 2fcf141..f35aaf7 100644
--- a/src/category_theory/model/wfs.lean
+++ b/src/category_theory/model/wfs.lean
@@ -31,20 +31,6 @@ 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 llp.op (R : morphism_class M) : morphism_class.op M (llp R) = rlp (morphism_class.op M R) :=
-begin
-  unfold morphism_class.op,
-  ext,
-  split,
-  intros g p q d e f g h,
-end 
-
-lemma is_wfs.op { L R : morphism_class M } ( w: is_wfs L R ) : @is_wfs Mᵒᵖ infer_instance (morphism_class.op M R) (morphism_class.op M L) := 
-{
-  llp := by { unfold morphism_class.op, tidy; rw w.rlp at *,},
-  rlp := by { sorry },
-  fact := by { sorry }
-}
 
 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 :=
@@ -53,7 +39,7 @@ begin
   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,
@@ -65,6 +51,18 @@ begin
   { 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) :=
 λ a b f hf x y g hg, hg hf
 

From b1cb3ca70c7059256cb3f0dfefd3444ae7bc4df1 Mon Sep 17 00:00:00 2001
From: Saul Glasman <saulglasman0@gmail.com>
Date: Fri, 6 Nov 2020 16:13:01 -0500
Subject: [PATCH 3/4] Tweak

---
 src/category_theory/model/category.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/category_theory/model/category.lean b/src/category_theory/model/category.lean
index 5a4be64..e446c29 100644
--- a/src/category_theory/model/category.lean
+++ b/src/category_theory/model/category.lean
@@ -75,9 +75,9 @@ lemma is_model_category.weq_of_weq_retract { W C F : morphism_class M } [ @has_p
       }
     },
    rw ← f'_fact,
-   refine h.weq.weq_comp a' c b' α β WCα.2 _,
+   apply h.weq.weq_comp a' c b' α β WCα.2,
    refine is_model_category.weq_of_weq_retract_fib h rεβ _ Fβ,
-   refine h.weq.weq_cancel_left WCδ.2 _,
+   apply h.weq.weq_cancel_left WCδ.2,
    rw Is_pushout.induced_commutes₁ po _ _ _,
    assumption,
 end

From 80477317b6d3e4f27a295625e98ce5c8b63c3b20 Mon Sep 17 00:00:00 2001
From: Saul Glasman <saulglasman0@gmail.com>
Date: Tue, 10 Nov 2020 20:02:46 -0500
Subject: [PATCH 4/4] Formatting

---
 src/category_theory/model/category.lean | 7 -------
 src/category_theory/retract.lean        | 2 +-
 2 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/category_theory/model/category.lean b/src/category_theory/model/category.lean
index e446c29..b978775 100644
--- a/src/category_theory/model/category.lean
+++ b/src/category_theory/model/category.lean
@@ -88,13 +88,6 @@ class model_category (M : Type u) extends category.{v} M :=
 (cocomplete : has_colimits M)
 (W C F : morphism_class M)
 (h : is_model_category W C F)
-
--- variables { C: Type u } [mc: model_category C] {a b : C} { f: a ⟶ b }
--- lemma model_category.weq_of_weq_retract { C: Type u } [mc: model_category C]
---  {a b a' b' : C} {f : a ⟶ b} {f' : a' ⟶ b'} (r : retract f f') ( hf : W f ) : W f' := 
--- begin
-  
--- end
 include 𝓜
 
 /-- We can skip checking the condition C ∩ W ⊆ AC. Compare Hirschhorn, Theorem 11.3.1. -/
diff --git a/src/category_theory/retract.lean b/src/category_theory/retract.lean
index c8299e8..0fba5fe 100644
--- a/src/category_theory/retract.lean
+++ b/src/category_theory/retract.lean
@@ -11,7 +11,7 @@ universes v v' u u'
 variables {C : Type u} [𝒞 : category.{v} C]
 include 𝒞
 
--- `retract f f'` is a diagram exhibiting f' as a retract of f.
+--- `retract f f'` is a diagram exhibiting f' as a retract of f.
 structure retract {a b a' b' : C} (f : a ⟶ b) (f' : a' ⟶ b') : Type v :=
 (ia : a' ⟶ a) (ra : a ⟶ a')
 (ib : b' ⟶ b) (rb : b ⟶ b')