From e83ba8f5e0d85288acc5d7523d92317af271796f Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Wed, 17 Aug 2022 07:10:39 +0000 Subject: [PATCH] feat(category_theory/limits/shapes/diagonal): The diagonal object of a morphism. (#15711) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- .../limits/shapes/diagonal.lean | 369 ++++++++++++++++++ .../limits/shapes/kernel_pair.lean | 39 ++ 2 files changed, 408 insertions(+) create mode 100644 src/category_theory/limits/shapes/diagonal.lean diff --git a/src/category_theory/limits/shapes/diagonal.lean b/src/category_theory/limits/shapes/diagonal.lean new file mode 100644 index 0000000000000..c19b2378a9171 --- /dev/null +++ b/src/category_theory/limits/shapes/diagonal.lean @@ -0,0 +1,369 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import category_theory.limits.shapes.pullbacks +import category_theory.limits.shapes.kernel_pair +import category_theory.limits.shapes.comm_sq + +/-! +# The diagonal object of a morphism. + +We provide various API and isomorphisms considering the diagonal object `Δ_{Y/X} := pullback f f` +of a morphism `f : X ⟶ Y`. + +-/ + +open category_theory + +noncomputable theory + +namespace category_theory.limits + +variables {C : Type*} [category C] {X Y Z : C} + +namespace pullback + +section diagonal + +variables (f : X ⟶ Y) [has_pullback f f] + +/-- The diagonal object of a morphism `f : X ⟶ Y` is `Δ_{X/Y} := pullback f f`. -/ +abbreviation diagonal_obj : C := pullback f f + +/-- The diagonal morphism `X ⟶ Δ_{X/Y}` for a morphism `f : X ⟶ Y`. -/ +def diagonal : X ⟶ diagonal_obj f := +pullback.lift (𝟙 _) (𝟙 _) rfl + +@[simp, reassoc] lemma diagonal_fst : diagonal f ≫ pullback.fst = 𝟙 _ := +pullback.lift_fst _ _ _ + +@[simp, reassoc] lemma diagonal_snd : diagonal f ≫ pullback.snd = 𝟙 _ := +pullback.lift_snd _ _ _ + +instance : is_split_mono (diagonal f) := +⟨⟨⟨pullback.fst, diagonal_fst f⟩⟩⟩ + +instance : is_split_epi (pullback.fst : pullback f f ⟶ X) := +⟨⟨⟨diagonal f, diagonal_fst f⟩⟩⟩ + +instance : is_split_epi (pullback.snd : pullback f f ⟶ X) := +⟨⟨⟨diagonal f, diagonal_snd f⟩⟩⟩ + +instance [mono f] : is_iso (diagonal f) := +begin + rw (is_iso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm, + apply_instance +end + +/-- The two projections `Δ_{X/Y} ⟶ X` form a kernel pair for `f : X ⟶ Y`. -/ +def diagonal_is_kernel_pair : + is_kernel_pair f (pullback.fst : diagonal_obj f ⟶ _) pullback.snd := +⟨pullback.condition, pullback_is_pullback _ _⟩ + +end diagonal + +end pullback + +variable [has_pullbacks C] + +open pullback + +section + +variables {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) +variables (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) + +@[simp, reassoc] +lemma pullback_diagonal_map_snd_fst_fst : + (pullback.snd : pullback (diagonal f) (map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i + (by simp [condition]) (by simp [condition])) ⟶ _) ≫ fst ≫ i₁ ≫ fst = pullback.fst := +begin + conv_rhs { rw ← category.comp_id pullback.fst }, + rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst] +end + +@[simp, reassoc] +lemma pullback_diagonal_map_snd_snd_fst : + (pullback.snd : pullback (diagonal f) (map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i + (by simp [condition]) (by simp [condition])) ⟶ _) ≫ snd ≫ i₂ ≫ fst = pullback.fst := +begin + conv_rhs { rw ← category.comp_id pullback.fst }, + rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd] +end + +variable [has_pullback i₁ i₂] + +/-- +This iso witnesses the fact that +given `f : X ⟶ Y`, `i : U ⟶ Y`, and `i₁ : V₁ ⟶ X ×[Y] U`, `i₂ : V₂ ⟶ X ×[Y] U`, the diagram + +V₁ ×[X ×[Y] U] V₂ ⟶ V₁ ×[U] V₂ + | | + | | + ↓ ↓ + X ⟶ X ×[Y] X + +is a pullback square. +Also see `pullback_fst_map_snd_is_pullback`. +-/ +def pullback_diagonal_map_iso : + pullback (diagonal f) (map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i + (by simp [condition]) (by simp [condition])) ≅ pullback i₁ i₂ := +{ hom := pullback.lift (pullback.snd ≫ pullback.fst) (pullback.snd ≫ pullback.snd) + begin + ext; simp only [category.assoc, pullback.condition, pullback_diagonal_map_snd_fst_fst, + pullback_diagonal_map_snd_snd_fst], + end, + inv := pullback.lift (pullback.fst ≫ i₁ ≫ pullback.fst) (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) + pullback.snd (category.id_comp _).symm (category.id_comp _).symm) + begin + ext; simp only [diagonal_fst, diagonal_snd, category.comp_id, pullback.condition_assoc, + category.assoc, lift_fst, lift_fst_assoc, lift_snd, lift_snd_assoc], + end, + hom_inv_id' := by ext; simp only [category.id_comp, category.assoc, lift_fst_assoc, + pullback_diagonal_map_snd_fst_fst, lift_fst, lift_snd, category.comp_id], + inv_hom_id' := by ext; simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_iso_hom_fst : + (pullback_diagonal_map_iso f i i₁ i₂).hom ≫ pullback.fst = pullback.snd ≫ pullback.fst := +by { delta pullback_diagonal_map_iso, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_iso_hom_snd : + (pullback_diagonal_map_iso f i i₁ i₂).hom ≫ pullback.snd = pullback.snd ≫ pullback.snd := +by { delta pullback_diagonal_map_iso, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_iso_inv_fst : + (pullback_diagonal_map_iso f i i₁ i₂).inv ≫ pullback.fst = pullback.fst ≫ i₁ ≫ pullback.fst := +by { delta pullback_diagonal_map_iso, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_iso_inv_snd_fst : + (pullback_diagonal_map_iso f i i₁ i₂).inv ≫ pullback.snd ≫ pullback.fst = pullback.fst := +by { delta pullback_diagonal_map_iso, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_iso_inv_snd_snd : + (pullback_diagonal_map_iso f i i₁ i₂).inv ≫ pullback.snd ≫ pullback.snd = pullback.snd := +by { delta pullback_diagonal_map_iso, simp } + +lemma pullback_fst_map_snd_is_pullback : + is_pullback + (fst ≫ i₁ ≫ fst) + (map i₁ i₂ (i₁ ≫ snd) (i₂ ≫ snd) _ _ _ (category.id_comp _).symm (category.id_comp _).symm) + (diagonal f) + (map (i₁ ≫ snd) (i₂ ≫ snd) f f (i₁ ≫ fst) (i₂ ≫ fst) i + (by simp [condition]) (by simp [condition])) := +is_pullback.of_iso_pullback ⟨by ext; simp [condition_assoc]⟩ + (pullback_diagonal_map_iso f i i₁ i₂).symm (pullback_diagonal_map_iso_inv_fst f i i₁ i₂) + (by ext1; simp) + +end + +section + +variables {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) +variables [has_pullback i i] [has_pullback f g] [has_pullback (f ≫ i) (g ≫ i)] +variable [has_pullback (diagonal i) (pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 _) + (category.comp_id _) (category.comp_id _))] + +/-- +This iso witnesses the fact that +given `f : X ⟶ T`, `g : Y ⟶ T`, and `i : T ⟶ S`, the diagram + +X ×ₜ Y ⟶ X ×ₛ Y + | | + | | + ↓ ↓ + T ⟶ T ×ₛ T + +is a pullback square. +Also see `pullback_map_diagonal_is_pullback`. +-/ +def pullback_diagonal_map_id_iso : + pullback (diagonal i) (pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 _) + (category.comp_id _) (category.comp_id _)) ≅ pullback f g := +begin + refine (as_iso $ pullback.map _ _ _ _ (𝟙 _) (pullback.congr_hom _ _).hom (𝟙 _) _ _) ≪≫ + pullback_diagonal_map_iso i (𝟙 _) (f ≫ inv pullback.fst) (g ≫ inv pullback.fst) ≪≫ + (as_iso $ pullback.map _ _ _ _ (𝟙 _) (𝟙 _) pullback.fst _ _), + { rw [← category.comp_id pullback.snd, ← condition, category.assoc, is_iso.inv_hom_id_assoc] }, + { rw [← category.comp_id pullback.snd, ← condition, category.assoc, is_iso.inv_hom_id_assoc] }, + { rw [category.comp_id, category.id_comp] }, + { ext; simp }, + { apply_instance }, + { rw [category.assoc, category.id_comp, is_iso.inv_hom_id, category.comp_id] }, + { rw [category.assoc, category.id_comp, is_iso.inv_hom_id, category.comp_id] }, + { apply_instance }, +end + +@[simp, reassoc] +lemma pullback_diagonal_map_id_iso_hom_fst : + (pullback_diagonal_map_id_iso f g i).hom ≫ pullback.fst = pullback.snd ≫ pullback.fst := +by { delta pullback_diagonal_map_id_iso, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_id_iso_hom_snd : + (pullback_diagonal_map_id_iso f g i).hom ≫ pullback.snd = pullback.snd ≫ pullback.snd := +by { delta pullback_diagonal_map_id_iso, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_id_iso_inv_fst : + (pullback_diagonal_map_id_iso f g i).inv ≫ pullback.fst = pullback.fst ≫ f := +begin + rw [iso.inv_comp_eq, ← category.comp_id pullback.fst, ← diagonal_fst i, pullback.condition_assoc], + simp, +end + +@[simp, reassoc] +lemma pullback_diagonal_map_id_iso_inv_snd_fst : + (pullback_diagonal_map_id_iso f g i).inv ≫ pullback.snd ≫ pullback.fst = pullback.fst := +by { rw iso.inv_comp_eq, simp } + +@[simp, reassoc] +lemma pullback_diagonal_map_id_iso_inv_snd_snd : + (pullback_diagonal_map_id_iso f g i).inv ≫ pullback.snd ≫ pullback.snd = pullback.snd := +by { rw iso.inv_comp_eq, simp } + +lemma pullback.diagonal_comp (f : X ⟶ Y) (g : Y ⟶ Z) [has_pullback f f] [has_pullback g g] + [has_pullback (f ≫ g) (f ≫ g)] : + diagonal (f ≫ g) = diagonal f ≫ (pullback_diagonal_map_id_iso f f g).inv ≫ pullback.snd := +by ext; simp + +lemma pullback_map_diagonal_is_pullback : is_pullback (pullback.fst ≫ f) + (pullback.map f g (f ≫ i) (g ≫ i) _ _ i (category.id_comp _).symm (category.id_comp _).symm) + (diagonal i) + (pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 _) (category.comp_id _) (category.comp_id _)) := +begin + apply is_pullback.of_iso_pullback _ (pullback_diagonal_map_id_iso f g i).symm, + { simp }, + { ext; simp }, + { constructor, ext; simp [condition] }, +end + +/-- The diagonal object of `X ×[Z] Y ⟶ X` is isomorphic to `Δ_{Y/Z} ×[Z] X`. -/ +def diagonal_obj_pullback_fst_iso {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : + diagonal_obj (pullback.fst : pullback f g ⟶ X) ≅ + pullback (pullback.snd ≫ g : diagonal_obj g ⟶ Z) f := +pullback_right_pullback_fst_iso _ _ _ ≪≫ pullback.congr_hom pullback.condition rfl ≪≫ + pullback_assoc _ _ _ _ ≪≫ pullback_symmetry _ _ ≪≫ pullback.congr_hom pullback.condition rfl + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_hom_fst_fst {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).hom ≫ pullback.fst ≫ pullback.fst = + pullback.fst ≫ pullback.snd := +by { delta diagonal_obj_pullback_fst_iso, simp } + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_hom_fst_snd {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).hom ≫ pullback.fst ≫ pullback.snd = + pullback.snd ≫ pullback.snd := +by { delta diagonal_obj_pullback_fst_iso, simp } + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_hom_snd {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).hom ≫ pullback.snd = pullback.fst ≫ pullback.fst := +by { delta diagonal_obj_pullback_fst_iso, simp } + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_inv_fst_fst {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).inv ≫ pullback.fst ≫ pullback.fst = + pullback.snd := +by { delta diagonal_obj_pullback_fst_iso, simp } + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_inv_fst_snd {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).inv ≫ pullback.fst ≫ pullback.snd = + pullback.fst ≫ pullback.fst := +by { delta diagonal_obj_pullback_fst_iso, simp } + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_inv_snd_fst {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).inv ≫ pullback.snd ≫ pullback.fst = pullback.snd := +by { delta diagonal_obj_pullback_fst_iso, simp } + +@[simp, reassoc] lemma diagonal_obj_pullback_fst_iso_inv_snd_snd {X Y Z : C} (f : X ⟶ Z) + (g : Y ⟶ Z) : + (diagonal_obj_pullback_fst_iso f g).inv ≫ pullback.snd ≫ pullback.snd = + pullback.fst ≫ pullback.snd := +by { delta diagonal_obj_pullback_fst_iso, simp } + +lemma diagonal_pullback_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : + diagonal (pullback.fst : pullback f g ⟶ _) = + (pullback_symmetry _ _).hom ≫ ((base_change f).map + (over.hom_mk (diagonal g) (by simp) : over.mk g ⟶ over.mk (pullback.snd ≫ g))).left ≫ + (diagonal_obj_pullback_fst_iso f g).inv := +by ext; simp + +end + +/-- +Given the following diagram with `S ⟶ S'` a monomorphism, + + X ⟶ X' + ↘ ↘ + S ⟶ S' + ↗ ↗ + Y ⟶ Y' + +This iso witnesses the fact that + + X ×[S] Y ⟶ (X' ×[S'] Y') ×[Y'] Y + | | + | | + ↓ ↓ +(X' ×[S'] Y') ×[X'] X ⟶ X' ×[S'] Y' + +is a pullback square. The diagonal map of this square is `pullback.map`. +Also see `pullback_lift_map_is_pullback`. +-/ +@[simps] +def pullback_fst_fst_iso {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') + (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f') + (e₂ : g ≫ i₃ = i₂ ≫ g') [mono i₃] : + pullback (pullback.fst : pullback (pullback.fst : pullback f' g' ⟶ _) i₁ ⟶ _) + (pullback.fst : pullback (pullback.snd : pullback f' g' ⟶ _) i₂ ⟶ _) ≅ pullback f g := +{ hom := pullback.lift (pullback.fst ≫ pullback.snd) (pullback.snd ≫ pullback.snd) + begin + rw [← cancel_mono i₃, category.assoc, category.assoc, category.assoc, category.assoc, e₁, e₂, + ← pullback.condition_assoc, pullback.condition_assoc, pullback.condition, + pullback.condition_assoc] + end, + inv := pullback.lift + (pullback.lift (pullback.map _ _ _ _ _ _ _ e₁ e₂) pullback.fst (pullback.lift_fst _ _ _)) + (pullback.lift (pullback.map _ _ _ _ _ _ _ e₁ e₂) pullback.snd (pullback.lift_snd _ _ _)) + begin + rw [pullback.lift_fst, pullback.lift_fst] + end, + hom_inv_id' := by ext; simp only [category.assoc, category.id_comp, lift_fst, lift_snd, + lift_fst_assoc, lift_snd_assoc, condition, ← condition_assoc], + inv_hom_id' := by ext; simp only [category.assoc, category.id_comp, lift_fst, lift_snd, + lift_fst_assoc, lift_snd_assoc], } + +lemma pullback_map_eq_pullback_fst_fst_iso_inv {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) + (f' : X' ⟶ S') + (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f') + (e₂ : g ≫ i₃ = i₂ ≫ g') [mono i₃] : + pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ = + (pullback_fst_fst_iso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ pullback.snd ≫ pullback.fst := +begin + ext; simp only [category.assoc, category.id_comp, lift_fst, lift_snd, lift_fst_assoc, + lift_snd_assoc, pullback_fst_fst_iso_inv, ← pullback.condition, ← pullback.condition_assoc], +end + +lemma pullback_lift_map_is_pullback {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') + (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f') + (e₂ : g ≫ i₃ = i₂ ≫ g') [mono i₃] : + is_pullback + (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) fst (lift_fst _ _ _)) + (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) snd (lift_snd _ _ _)) + pullback.fst pullback.fst := +is_pullback.of_iso_pullback ⟨by rw [lift_fst, lift_fst]⟩ + (pullback_fst_fst_iso f g f' g' i₁ i₂ i₃ e₁ e₂).symm (by simp) (by simp) + + +end category_theory.limits diff --git a/src/category_theory/limits/shapes/kernel_pair.lean b/src/category_theory/limits/shapes/kernel_pair.lean index 222a172f72cca..67c9e2e2a88ef 100644 --- a/src/category_theory/limits/shapes/kernel_pair.lean +++ b/src/category_theory/limits/shapes/kernel_pair.lean @@ -160,5 +160,44 @@ begin apply w } end +/-- If `a₁ a₂ : A ⟶ Y` is a kernel pair for `g : Y ⟶ Z`, then `a₁ ×[Z] X` and `a₂ ×[Z] X` +(`A ×[Z] X ⟶ Y ×[Z] X`) is a kernel pair for `Y ×[Z] X ⟶ X`. -/ +protected noncomputable +def pullback {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} + (h : is_kernel_pair g a₁ a₂) (f : X ⟶ Z) [has_pullback f g] [has_pullback f (a₁ ≫ g)] : + is_kernel_pair (pullback.fst : pullback f g ⟶ X) + (pullback.map f _ f _ (𝟙 X) a₁ (𝟙 Z) (by simp) $ category.comp_id _) + (pullback.map _ _ _ _ (𝟙 X) a₂ (𝟙 Z) (by simp) $ (category.comp_id _).trans h.1) := +begin + fconstructor, + { rw [pullback.lift_fst, pullback.lift_fst] }, + { fapply pullback_cone.is_limit_aux', + intro s, + refine ⟨pullback.lift (s.fst ≫ pullback.fst) + (h.lift' (s.fst ≫ pullback.snd) (s.snd ≫ pullback.snd) _).1 _, _, _, _⟩, + { simp_rw [category.assoc, ← pullback.condition, ← category.assoc, s.condition] }, + { rw [← category.assoc, (h.lift' _ _ _).2.1, category.assoc, + category.assoc, pullback.condition] }, + { rw limits.pullback_cone.mk_fst, + ext; simp only [category.assoc, pullback.lift_fst, pullback.lift_snd, pullback.lift_snd_assoc, + category.comp_id, (h.lift' _ _ _).2.1] }, + { rw limits.pullback_cone.mk_snd, + ext; simp only [category.assoc, pullback.lift_fst, pullback.lift_snd, pullback.lift_snd_assoc, + category.comp_id, (h.lift' _ _ _).2.2, s.condition] }, + { intros m h₁ h₂, + ext, + { rw pullback.lift_fst, + conv_rhs { rw [← h₁, category.assoc, pullback_cone.mk_fst] }, + congr' 1, + refine ((pullback.lift_fst _ _ _).trans $ category.comp_id _).symm }, + { rw pullback.lift_snd, + apply pullback_cone.is_limit.hom_ext h.2; + simp only [pullback_cone.mk_fst, pullback_cone.mk_snd, category.assoc, + (h.lift' _ _ _).2.1, (h.lift' _ _ _).2.2], + { conv_rhs { rw [← h₁, category.assoc, pullback_cone.mk_fst, pullback.lift_snd] } }, + { conv_rhs { rw [← h₂, category.assoc, pullback_cone.mk_snd, pullback.lift_snd] } } } } } +end + + end is_kernel_pair end category_theory