refactor(category_theory/lifting_properties): refactor lifting proper…

…ties using comm_sq (#15765)




Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: kkytola <kalle.kytola@aalto.fi>
Co-authored-by: Tyler Raven Billingsley <trbillin@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: damiano <adomani@gmail.com>
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: negiizhao <egresf@gmail.com>
Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: tb65536 <tb65536@uw.edu>
Co-authored-by: Kexing Ying <kexing.ying19@imperial.ac.uk>
Co-authored-by: Rémy Degenne <Remydegenne@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/category_theory/arrow.lean

@@ -168,74 +168,6 @@ lemma square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : arrow T) (sq : arrow.m
   i.inv ≫ sq.left ≫ p.hom = sq.right :=
 by simp only [iso.inv_hom_id_assoc, arrow.w, arrow.mk_hom]
 
-/-- A lift of a commutative square is a diagonal morphism making the two triangles commute. -/
-@[ext] structure lift_struct {f g : arrow T} (sq : f ⟶ g) :=
-(lift : f.right ⟶ g.left)
-(fac_left' : f.hom ≫ lift = sq.left . obviously)
-(fac_right' : lift ≫ g.hom = sq.right . obviously)
-
-restate_axiom lift_struct.fac_left'
-restate_axiom lift_struct.fac_right'
-
-instance lift_struct_inhabited {X : T} : inhabited (lift_struct (𝟙 (arrow.mk (𝟙 X)))) :=
-⟨⟨𝟙 _, category.id_comp _, category.comp_id _⟩⟩
-
-/-- `has_lift sq` says that there is some `lift_struct sq`, i.e., that it is possible to find a
-    diagonal morphism making the two triangles commute. -/
-class has_lift {f g : arrow T} (sq : f ⟶ g) : Prop :=
-mk' :: (exists_lift : nonempty (lift_struct sq))
-
-lemma has_lift.mk {f g : arrow T} {sq : f ⟶ g} (s : lift_struct sq) : has_lift sq :=
-⟨nonempty.intro s⟩
-
-attribute [simp, reassoc] lift_struct.fac_left lift_struct.fac_right
-
-/-- Given `has_lift sq`, obtain a lift. -/
-noncomputable def has_lift.struct {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : lift_struct sq :=
-classical.choice has_lift.exists_lift
-
-/-- If there is a lift of a commutative square `sq`, we can access it by saying `lift sq`. -/
-noncomputable abbreviation lift {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : f.right ⟶ g.left :=
-(has_lift.struct sq).lift
-
-lemma lift.fac_left {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : f.hom ≫ lift sq = sq.left :=
-by simp
-
-lemma lift.fac_right {f g : arrow T} (sq : f ⟶ g) [has_lift sq] : lift sq ≫ g.hom = sq.right :=
-by simp
-
-@[simp, reassoc]
-lemma lift.fac_right_of_to_mk {X Y : T} {f : arrow T} {g : X ⟶ Y} (sq : f ⟶ mk g) [has_lift sq] :
-  lift sq ≫ g = sq.right :=
-by simp only [←mk_hom g, lift.fac_right]
-
-@[simp, reassoc]
-lemma lift.fac_left_of_from_mk {X Y : T} {f : X ⟶ Y} {g : arrow T} (sq : mk f ⟶ g) [has_lift sq] :
-  f ≫ lift sq = sq.left :=
-by simp only [←mk_hom f, lift.fac_left]
-
-@[simp, reassoc]
-lemma lift_mk'_left {X Y P Q : T} {f : X ⟶ Y} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
-  (h : u ≫ g = f ≫ v) [has_lift $ arrow.hom_mk' h] : f ≫ lift (arrow.hom_mk' h) = u :=
-by simp only [←arrow.mk_hom f, lift.fac_left, arrow.hom_mk'_left]
-
-@[simp, reassoc]
-lemma lift_mk'_right {X Y P Q : T} {f : X ⟶ Y} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
-  (h : u ≫ g = f ≫ v) [has_lift $ arrow.hom_mk' h] : lift (arrow.hom_mk' h) ≫ g = v :=
-by simp only [←arrow.mk_hom g, lift.fac_right, arrow.hom_mk'_right]
-
-section
-
-instance subsingleton_lift_struct_of_epi {f g : arrow T} (sq : f ⟶ g) [epi f.hom] :
-  subsingleton (lift_struct sq) :=
-subsingleton.intro $ λ a b, lift_struct.ext a b $ (cancel_epi f.hom).1 $ by simp
-
-instance subsingleton_lift_struct_of_mono {f g : arrow T} (sq : f ⟶ g) [mono g.hom] :
-  subsingleton (lift_struct sq) :=
-subsingleton.intro $ λ a b, lift_struct.ext a b $ (cancel_mono g.hom).1 $ by simp
-
-end
-
 variables {C : Type u} [category.{v} C]
 /-- A helper construction: given a square between `i` and `f ≫ g`, produce a square between
 `i` and `g`, whose top leg uses `f`:

src/category_theory/comm_sq.lean

@@ -1,11 +1,10 @@
 /-
 Copyright (c) 2022 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Joël Riou
 -/
 import category_theory.arrow
 
-
 /-!
 # Commutative squares
 
@@ -75,4 +74,111 @@ end functor
 
 alias functor.map_comm_sq ← comm_sq.map
 
+namespace comm_sq
+
+variables {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
+
+/-- The datum of a lift in a commutative square, i.e. a up-right-diagonal
+morphism which makes both triangles commute. -/
+@[ext, nolint has_nonempty_instance]
+structure lift_struct (sq : comm_sq f i p g) :=
+(l : B ⟶ X) (fac_left' : i ≫ l = f) (fac_right' : l ≫ p = g)
+
+namespace lift_struct
+
+restate_axiom fac_left'
+restate_axiom fac_right'
+
+/-- A `lift_struct` for a commutative square gives a `lift_struct` for the
+corresponding square in the opposite category. -/
+@[simps]
+def op {sq : comm_sq f i p g} (l : lift_struct sq) : lift_struct sq.op :=
+{ l := l.l.op,
+  fac_left' := by rw [← op_comp, l.fac_right],
+  fac_right' := by rw [← op_comp, l.fac_left], }
+
+/-- A `lift_struct` for a commutative square in the opposite category
+gives a `lift_struct` for the corresponding square in the original category. -/
+@[simps]
+def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : comm_sq f i p g}
+  (l : lift_struct sq) : lift_struct sq.unop :=
+{ l := l.l.unop,
+  fac_left' := by rw [← unop_comp, l.fac_right],
+  fac_right' := by rw [← unop_comp, l.fac_left], }
+
+/-- Equivalences of `lift_struct` for a square and the corresponding square
+in the opposite category. -/
+@[simps]
+def op_equiv (sq : comm_sq f i p g) : lift_struct sq ≃ lift_struct sq.op :=
+{ to_fun := op,
+  inv_fun := unop,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+/-- Equivalences of `lift_struct` for a square in the oppositive category and
+the corresponding square in the original category. -/
+def unop_equiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
+  (sq : comm_sq f i p g) : lift_struct sq ≃ lift_struct sq.unop :=
+{ to_fun := unop,
+  inv_fun := op,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+end lift_struct
+
+instance subsingleton_lift_struct_of_epi (sq : comm_sq f i p g) [epi i] :
+  subsingleton (lift_struct sq) :=
+⟨λ l₁ l₂, by { ext, simp only [← cancel_epi i, lift_struct.fac_left], }⟩
+
+instance subsingleton_lift_struct_of_mono (sq : comm_sq f i p g) [mono p] :
+  subsingleton (lift_struct sq) :=
+⟨λ l₁ l₂, by { ext, simp only [← cancel_mono p, lift_struct.fac_right], }⟩
+
+variable (sq : comm_sq f i p g)
+
+/-- The assertion that a square has a `lift_struct`. -/
+class has_lift : Prop := (exists_lift : nonempty sq.lift_struct)
+
+namespace has_lift
+
+variable {sq}
+
+lemma mk' (l : sq.lift_struct) : has_lift sq := ⟨nonempty.intro l⟩
+
+variable (sq)
+
+lemma iff : has_lift sq ↔ nonempty sq.lift_struct :=
+by { split, exacts [λ h, h.exists_lift, λ h, mk h], }
+
+lemma iff_op : has_lift sq ↔ has_lift sq.op :=
+begin
+  rw [iff, iff],
+  exact nonempty.congr (lift_struct.op_equiv sq).to_fun (lift_struct.op_equiv sq).inv_fun,
+end
+
+lemma iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
+  (sq : comm_sq f i p g) : has_lift sq ↔ has_lift sq.unop :=
+begin
+  rw [iff, iff],
+  exact nonempty.congr (lift_struct.unop_equiv sq).to_fun (lift_struct.unop_equiv sq).inv_fun,
+end
+
+end has_lift
+
+/-- A choice of a diagonal morphism that is part of a `lift_struct` when
+the square has a lift. -/
+noncomputable
+def lift [hsq : has_lift sq] : B ⟶ X :=
+hsq.exists_lift.some.l
+
+@[simp, reassoc]
+lemma fac_left [hsq : has_lift sq] : i ≫ sq.lift = f :=
+hsq.exists_lift.some.fac_left
+
+@[simp, reassoc]
+lemma fac_right [hsq : has_lift sq] : sq.lift ≫ p = g :=
+hsq.exists_lift.some.fac_right
+
+end comm_sq
+
 end category_theory