Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(category_theory/limits): cleanup equalizers #5214

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(category_theory/limits): cleanup equalizers #5214

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
95 changes: 37 additions & 58 deletions src/category_theory/limits/shapes/equalizers.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ Each of these has a dual.
## Main statements

* `equalizer.ι_mono` states that every equalizer map is a monomorphism
* `is_iso_limit_cone_parallel_pair_of_self` states that the identity on the domain of `f` is an equalizer
of `f` and `f`.
* `is_iso_limit_cone_parallel_pair_of_self` states that the identity on the domain of `f` is an
equalizer of `f` and `f`.

## Implementation notes
As with the other special shapes in the limits library, all the definitions here are given as
Expand Down Expand Up @@ -138,6 +138,19 @@ abbreviation cofork (f g : X ⟶ Y) := cocone (parallel_pair f g)

variables {f g : X ⟶ Y}

/-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms `t.π.app zero : t.X ⟶ X`
and `t.π.app one : t.X ⟶ Y`. Of these, only the first one is interesting, and we give it the
shorter name `fork.ι t`. -/
abbreviation fork.ι (t : fork f g) := t.π.app zero

/-- A cofork `t` on the parallel_pair `f g : X ⟶ Y` consists of two morphisms
`t.ι.app zero : X ⟶ t.X` and `t.ι.app one : Y ⟶ t.X`. Of these, only the second one is
interesting, and we give it the shorter name `cofork.π t`. -/
abbreviation cofork.π (t : cofork f g) := t.ι.app one

@[simp] lemma fork.ι_eq_app_zero (t : fork f g) : t.ι = t.π.app zero := rfl
@[simp] lemma cofork.π_eq_app_one (t : cofork f g) : t.π = t.ι.app one := rfl

@[simp, reassoc] lemma fork.app_zero_left (s : fork f g) :
s.π.app zero ≫ f = s.π.app one :=
by rw [←s.w left, parallel_pair_map_left]
Expand Down Expand Up @@ -175,38 +188,19 @@ def fork.of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) : fork f g :=
def cofork.of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) : cofork f g :=
{ X := P,
ι :=
{ app := λ X, begin cases X, exact f ≫ π, exact π, end,
naturality' := λ X Y f,
begin
cases X; cases Y; cases f; dsimp; simp,
{ dsimp, simp, },
{ exact w.symm },
{ dsimp, simp, },
end } }

/-- A fork `t` on the parallel pair `f g : X ⟶ Y` consists of two morphisms `t.π.app zero : t.X ⟶ X`
and `t.π.app one : t.X ⟶ Y`. Of these, only the first one is interesting, and we give it the
shorter name `fork.ι t`. -/
abbreviation fork.ι (t : fork f g) := t.π.app zero

/-- A cofork `t` on the parallel_pair `f g : X ⟶ Y` consists of two morphisms
`t.ι.app zero : X ⟶ t.X` and `t.ι.app one : Y ⟶ t.X`. Of these, only the second one is
interesting, and we give it the shorter name `cofork.π t`. -/
abbreviation cofork.π (t : cofork f g) := t.ι.app one
{ app := λ X, walking_parallel_pair.cases_on X (f ≫ π) π,
naturality' := λ i j f, by { cases f; dsimp; simp [w] } } } -- See note [dsimp, simp]

@[simp] lemma fork.ι_of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
fork.ι (fork.of_ι ι w) = ι := rfl
@[simp] lemma cofork.π_of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
cofork.π (cofork.of_π π w) = π := rfl

lemma fork.ι_eq_app_zero (t : fork f g) : fork.ι t = t.π.app zero := rfl
lemma cofork.π_eq_app_one (t : cofork f g) : cofork.π t = t.ι.app one := rfl
lemma fork.ι_of_ι {P : C} (ι : P ⟶ X) (w : ι ≫ f = ι ≫ g) :
(fork.of_ι ι w).ι = ι := rfl
lemma cofork.π_of_π {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) :
(cofork.of_π π w).π = π := rfl

@[reassoc]
lemma fork.condition (t : fork f g) : fork.ι t ≫ f = fork.ι t ≫ g :=
lemma fork.condition (t : fork f g) : t.ι ≫ f = t.ι ≫ g :=
by rw [t.app_zero_left, t.app_zero_right]
@[reassoc]
lemma cofork.condition (t : cofork f g) : f ≫ cofork.π t = g ≫ cofork.π t :=
lemma cofork.condition (t : cofork f g) : f ≫ t.π = g ≫ t.π :=
by rw [t.left_app_one, t.right_app_one]

/-- To check whether two maps are equalized by both maps of a fork, it suffices to check it for the
Expand Down Expand Up @@ -735,26 +729,18 @@ variables {C} [split_mono f]
A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
Here we build the cone, and show in `split_mono_equalizes` that it is a limit cone.
-/
@[simps {rhs_md := semireducible}]
def cone_of_split_mono : cone (parallel_pair (𝟙 Y) (retraction f ≫ f)) :=
fork.of_ι f (by tidy)

@[simp] lemma cone_of_split_mono_π_app_zero : (cone_of_split_mono f).π.app zero = f := rfl
@[simp] lemma cone_of_split_mono_π_app_one : (cone_of_split_mono f).π.app one = f ≫ 𝟙 Y := rfl
fork.of_ι f (by simp)

/--
A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
-/
def split_mono_equalizes {X Y : C} (f : X ⟶ Y) [split_mono f] : is_limit (cone_of_split_mono f) :=
{ lift := λ s, s.π.app zero ≫ retraction f,
fac' := λ s,
begin
rintros (⟨⟩|⟨⟩),
{ rw [cone_of_split_mono_π_app_zero],
erw [category.assoc, ← s.π.naturality right, s.π.naturality left, category.comp_id], },
{ erw [cone_of_split_mono_π_app_one, category.comp_id, category.assoc,
← s.π.naturality right, category.id_comp], }
end,
uniq' := λ s m w, begin rw ←(w zero), simp, end, }
fork.is_limit.mk' _ $ λ s,
⟨s.ι ≫ retraction f,
by { dsimp, rw [category.assoc, ←s.condition], apply category.comp_id },
λ m hm, by simp [←hm]⟩

end

Expand All @@ -766,26 +752,19 @@ variables {C} [split_epi f]
A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
Here we build the cocone, and show in `split_epi_coequalizes` that it is a colimit cocone.
-/
@[simps {rhs_md := semireducible}]
def cocone_of_split_epi : cocone (parallel_pair (𝟙 X) (f ≫ section_ f)) :=
cofork.of_π f (by tidy)

@[simp] lemma cocone_of_split_epi_ι_app_one : (cocone_of_split_epi f).ι.app one = f := rfl
@[simp] lemma cocone_of_split_epi_ι_app_zero : (cocone_of_split_epi f).ι.app zero = 𝟙 X ≫ f := rfl
cofork.of_π f (by simp)

/--
A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
-/
def split_epi_coequalizes {X Y : C} (f : X ⟶ Y) [split_epi f] : is_colimit (cocone_of_split_epi f) :=
{ desc := λ s, section_ f ≫ s.ι.app one,
fac' := λ s,
begin
rintros (⟨⟩|⟨⟩),
{ erw [cocone_of_split_epi_ι_app_zero, category.assoc, category.id_comp, ←category.assoc,
s.ι.naturality right, functor.const.obj_map, category.comp_id], },
{ erw [cocone_of_split_epi_ι_app_one, ←category.assoc, s.ι.naturality right,
←s.ι.naturality left, category.id_comp] }
end,
uniq' := λ s m w, begin rw ←(w one), simp, end, }
def split_epi_coequalizes {X Y : C} (f : X ⟶ Y) [split_epi f] :
is_colimit (cocone_of_split_epi f) :=
cofork.is_colimit.mk' _ $ λ s,
⟨section_ f ≫ s.π,
by { dsimp, rw [← category.assoc, ← s.condition, category.id_comp] },
λ m hm, by simp [← hm]⟩

end

Expand Down