Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(category_theory/limits/shapes/diagonal): The diagonal object of …
…a morphism. (#15711) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
- Loading branch information
Showing
2 changed files
with
408 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Oops, something went wrong.