Skip to content

Commit

Permalink
fix(category_theory/limits): avoid a rewrite in a definition (leanpro…
Browse files Browse the repository at this point in the history 
…ver-community#2458)

The proof that every equalizer of `f` and `g` is an isomorphism if `f = g` had an ugly rewrite in a definition (introduced by yours truly). This PR reformulates the proof in a cleaner way by working with two morphisms `f` and `g` and a proof of `f = g` right from the start, which is easy to specialze to the case `(f, f)`, instead of trying to reduce the `(f, g)` case to the `(f, f)` case by rewriting.

This also lets us get rid of `fork.eq_of_ι_ι`, unless someone wants to keep it, but personally I don't think that using it is ever a good idea.
  • Loading branch information
@TwoFX @anrddh
TwoFX authored and anrddh committed May 16, 2020
1 parent 9c60b00 commit d9941af
Show file tree
Hide file tree
Showing 2 changed files with 60 additions and 128 deletions.
182 changes: 57 additions & 125 deletions src/category_theory/limits/shapes/equalizers.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -284,21 +284,6 @@ def cofork.is_colimit.mk (t : cofork f g)
(by erw [←s.w left, ←t.w left, category.assoc, fac]; refl) (fac s),
uniq' := uniq }

section
local attribute [ext] cone

/-- The fork induced by the ι map of some fork `t` is the same as `t` -/
lemma fork.eq_of_ι_ι (t : fork f g) : t = fork.of_ι (fork.ι t) (fork.condition t) :=
begin
have h : t.π = (fork.of_ι (fork.ι t) (fork.condition t)).π,
{ ext j, cases j,
{ refl },
{ rw ←fork.app_zero_left, refl } },
tidy
end

end

/-- This is a helper construction that can be useful when verifying that a category has all
equalizers. Given `F : walking_parallel_pair ⥤ C`, which is really the same as
`parallel_pair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`,
Expand All @@ -313,21 +298,6 @@ def cone.of_fork
{ app := λ X, t.π.app X ≫ eq_to_hom (by tidy),
naturality' := λ j j' g, by { cases j; cases j'; cases g; dsimp; simp } } }

section
local attribute [ext] cocone

/-- The cofork induced by the π map of some fork `t` is the same as `t` -/
lemma cofork.eq_of_π_π (t : cofork f g) : t = cofork.of_π (cofork.π t) (cofork.condition t) :=
begin
have h : t.ι = (cofork.of_π (cofork.π t) (cofork.condition t)).ι,
{ ext j, cases j,
{ rw ←cofork.left_app_one, refl },
{ refl } },
tidy
end

end

/-- This is a helper construction that can be useful when verifying that a category has all
coequalizers. Given `F : walking_parallel_pair ⥤ C`, which is really the same as
`parallel_pair (F.map left) (F.map right)`, and a cofork on `F.map left` and `F.map right`,
Expand Down Expand Up @@ -435,59 +405,44 @@ lemma mono_of_is_limit_parallel_pair {c : cone (parallel_pair f g)} (i : is_limi
end

section
/-- The identity determines a cone on the equalizer diagram of f and f -/
def cone_parallel_pair_self : cone (parallel_pair f f) :=
{ X := X,
π :=
{ app := λ j, match j with | zero := 𝟙 X | one := f end } }

@[simp] lemma cone_parallel_pair_self_π_app_zero : (cone_parallel_pair_self f).π.app zero = 𝟙 X :=
rfl
variables {f g}

@[simp] lemma cone_parallel_pair_self_X : (cone_parallel_pair_self f).X = X := rfl
/-- The identity determines a cone on the equalizer diagram of `f` and `g` if `f = g`. -/
def id_fork (h : f = g) : fork f g :=
fork.of_ι (𝟙 X) $ h ▸ rfl

/-- The identity on X is an equalizer of (f, f) -/
def is_limit_cone_parallel_pair_self : is_limit (cone_parallel_pair_self f) :=
{ lift := λ s, s.π.app zero,
fac' := λ s j,
match j with
| zero := category.comp_id _
| one := fork.app_zero_left _
end,
uniq' := λ s m w, by { convert w zero, erw category.comp_id } }
/-- The identity on `X` is an equalizer of `(f, g)`, if `f = g`. -/
def is_limit_id_fork (h : f = g) : is_limit (id_fork h) :=
fork.is_limit.mk _
(λ s, fork.ι s)
(λ s, category.comp_id _)
(λ s m h, by { convert h zero, exact (category.comp_id _).symm })

/-- Every equalizer of (f, f) is an isomorphism -/
def limit_cone_parallel_pair_self_is_iso (c : cone (parallel_pair f f)) (h : is_limit c) :
is_iso (c.π.app zero) :=
let c' := cone_parallel_pair_self f,
z : c ≅ c' := is_limit.unique_up_to_iso h (is_limit_cone_parallel_pair_self f) in
is_iso.of_iso (functor.map_iso (cones.forget _) z)
/-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
def is_iso_limit_cone_parallel_pair_of_eq (h₀ : f = g) {c : cone (parallel_pair f g)}
(h : is_limit c) : is_iso (c.π.app zero) :=
is_iso.of_iso $ is_limit.cone_point_unique_up_to_iso h $ is_limit_id_fork h₀

/-- The equalizer of (f, f) is an isomorphism -/
def equalizer.ι_of_self [has_limit (parallel_pair f f)] : is_iso (equalizer.ι f f) :=
limit_cone_parallel_pair_self_is_iso _ _ $ limit.is_limit _
/-- The equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
def equalizer.ι_of_eq [has_limit (parallel_pair f g)] (h : f = g) : is_iso (equalizer.ι f g) :=
is_iso_limit_cone_parallel_pair_of_eq h $ limit.is_limit _

/-- Every equalizer of (f, g), where f = g, is an isomorphism -/
def limit_cone_parallel_pair_self_is_iso' (c : cone (parallel_pair f g)) (h₀ : is_limit c)
(h₁ : f = g) : is_iso (c.π.app zero) :=
begin
rw fork.eq_of_ι_ι c at *,
have h₂ : is_limit (fork.of_ι (c.π.app zero) rfl : fork f f), by convert h₀,
exact limit_cone_parallel_pair_self_is_iso f (fork.of_ι (c.π.app zero) rfl) h₂
end

/-- The equalizer of (f, g), where f = g, is an isomorphism -/
def equalizer.ι_of_self' [has_limit (parallel_pair f g)] (h : f = g) : is_iso (equalizer.ι f g) :=
limit_cone_parallel_pair_self_is_iso' _ _ _ (limit.is_limit _) h
/-- Every equalizer of `(f, f)` is an isomorphism. -/
def is_iso_limit_cone_parallel_pair_of_self {c : cone (parallel_pair f f)} (h : is_limit c) :
is_iso (c.π.app zero) :=
is_iso_limit_cone_parallel_pair_of_eq rfl h

/-- An equalizer that is an epimorphism is an isomorphism -/
def epi_limit_cone_parallel_pair_is_iso (c : cone (parallel_pair f g))
/-- An equalizer that is an epimorphism is an isomorphism. -/
def is_iso_limit_cone_parallel_pair_of_epi {c : cone (parallel_pair f g)}
(h : is_limit c) [epi (c.π.app zero)] : is_iso (c.π.app zero) :=
limit_cone_parallel_pair_self_is_iso' f g c h $
(cancel_epi (c.π.app zero)).1 (fork.condition c)
is_iso_limit_cone_parallel_pair_of_eq ((cancel_epi _).1 (fork.condition c)) h

end

/-- The equalizer of `(f, f)` is an isomorphism. -/
def equalizer.ι_of_self [has_limit (parallel_pair f f)] : is_iso (equalizer.ι f f) :=
equalizer.ι_of_eq rfl

section
variables [has_colimit (parallel_pair f g)]

Expand Down Expand Up @@ -550,68 +505,45 @@ lemma epi_of_is_colimit_parallel_pair {c : cocone (parallel_pair f g)} (i : is_c
end

section
variables {f g}

/-- The identity determines a cocone on the coequalizer diagram of f and f -/
def cocone_parallel_pair_self : cocone (parallel_pair f f) :=
{ X := Y,
ι :=
{ app := λ j, match j with | zero := f | one := 𝟙 Y end,
naturality' := λ j j' g,
begin
cases g,
{ refl },
{ erw category.comp_id f },
{ dsimp, simp }
end } }

@[simp] lemma cocone_parallel_pair_self_ι_app_one : (cocone_parallel_pair_self f).ι.app one = 𝟙 Y :=
rfl

@[simp] lemma cocone_parallel_pair_self_X : (cocone_parallel_pair_self f).X = Y := rfl

/-- The identity on Y is a colimit of (f, f) -/
def is_colimit_cocone_parallel_pair_self : is_colimit (cocone_parallel_pair_self f) :=
{ desc := λ s, s.ι.app one,
fac' := λ s j,
match j with
| zero := cofork.left_app_one _
| one := category.id_comp _
end,
uniq' := λ s m w, by { convert w one, erw category.id_comp } }

/-- Every coequalizer of (f, f) is an isomorphism -/
def colimit_cocone_parallel_pair_self_is_iso (c : cocone (parallel_pair f f)) (h : is_colimit c) :
is_iso (c.ι.app one) :=
let c' := cocone_parallel_pair_self f,
z : c' ≅ c := is_colimit.unique_up_to_iso (is_colimit_cocone_parallel_pair_self f) h in
is_iso.of_iso $ functor.map_iso (cocones.forget _) z
/-- The identity determines a cocone on the coequalizer diagram of `f` and `g`, if `f = g`. -/
def id_cofork (h : f = g) : cofork f g :=
cofork.of_π (𝟙 Y) $ h ▸ rfl

/-- The coequalizer of (f, f) is an isomorphism -/
def coequalizer.π_of_self [has_colimit (parallel_pair f f)] : is_iso (coequalizer.π f f) :=
colimit_cocone_parallel_pair_self_is_iso _ _ $ colimit.is_colimit _
/-- The identity on `Y` is a coequalizer of `(f, g)`, where `f = g`. -/
def is_colimit_id_cofork (h : f = g) : is_colimit (id_cofork h) :=
cofork.is_colimit.mk _
(λ s, cofork.π s)
(λ s, category.id_comp _)
(λ s m h, by { convert h one, exact (category.id_comp _).symm })

/-- Every coequalizer of (f, g), where f = g, is an isomorphism -/
def colimit_cocone_parallel_pair_self_is_iso' (c : cocone (parallel_pair f g)) (h₀ : is_colimit c)
(h₁ : f = g) : is_iso (c.ι.app one) :=
begin
rw cofork.eq_of_π_π c at *,
have h₂ : is_colimit (cofork.of_π (c.ι.app one) rfl : cofork f f), by convert h₀,
exact colimit_cocone_parallel_pair_self_is_iso f (cofork.of_π (c.ι.app one) rfl) h₂
end
/-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
def is_iso_colimit_cocone_parallel_pair_of_eq (h₀ : f = g) {c : cocone (parallel_pair f g)}
(h : is_colimit c) : is_iso (c.ι.app one) :=
is_iso.of_iso $ is_colimit.cone_point_unique_up_to_iso (is_colimit_id_cofork h₀) h

/-- The coequalizer of (f, g), where f = g, is an isomorphism -/
def coequalizer.π_of_self' [has_colimit (parallel_pair f g)] (h : f = g) :
/-- The coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
def coequalizer.π_of_eq [has_colimit (parallel_pair f g)] (h : f = g) :
is_iso (coequalizer.π f g) :=
colimit_cocone_parallel_pair_self_is_iso' _ _ _ (colimit.is_colimit _) h
is_iso_colimit_cocone_parallel_pair_of_eq h $ colimit.is_colimit _

/-- Every coequalizer of `(f, f)` is an isomorphism. -/
def is_iso_colimit_cocone_parallel_pair_of_self {c : cocone (parallel_pair f f)}
(h : is_colimit c) : is_iso (c.ι.app one) :=
is_iso_colimit_cocone_parallel_pair_of_eq rfl h

/-- A coequalizer that is a monomorphism is an isomorphism -/
def mono_limit_cocone_parallel_pair_is_iso (c : cocone (parallel_pair f g))
/-- A coequalizer that is a monomorphism is an isomorphism. -/
def is_iso_limit_cocone_parallel_pair_of_epi {c : cocone (parallel_pair f g)}
(h : is_colimit c) [mono (c.ι.app one)] : is_iso (c.ι.app one) :=
colimit_cocone_parallel_pair_self_is_iso' f g c h $
(cancel_mono (c.ι.app one)).1 (cofork.condition c)
is_iso_colimit_cocone_parallel_pair_of_eq ((cancel_mono _).1 (cofork.condition c)) h

end

/-- The coequalizer of `(f, f)` is an isomorphism. -/
def coequalizer.π_of_self [has_colimit (parallel_pair f f)] : is_iso (coequalizer.π f f) :=
coequalizer.π_of_eq rfl

variables (C)

/-- `has_equalizers` represents a choice of equalizer for every pair of morphisms -/
Expand Down
6 changes: 3 additions & 3 deletions src/category_theory/limits/shapes/kernels.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ def kernel.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : {l : W ⟶ kernel f /
/-- Every kernel of the zero morphism is an isomorphism -/
def kernel.ι_zero_is_iso [has_limit (parallel_pair (0 : X ⟶ Y) 0)] :
is_iso (kernel.ι (0 : X ⟶ Y)) :=
limit_cone_parallel_pair_self_is_iso _ _ (limit.is_limit _)
equalizer.ι_of_self _

end

Expand Down Expand Up @@ -258,12 +258,12 @@ variables [has_zero_morphisms.{v} C]
/-- The kernel of the cokernel of an epimorphism is an isomorphism -/
instance kernel.of_cokernel_of_epi [has_colimit (parallel_pair f 0)]
[has_limit (parallel_pair (cokernel.π f) 0)] [epi f] : is_iso (kernel.ι (cokernel.π f)) :=
equalizer.ι_of_self' _ _ $ cokernel.π_of_epi f
equalizer.ι_of_eq $ cokernel.π_of_epi f

/-- The cokernel of the kernel of a monomorphism is an isomorphism -/
instance cokernel.of_kernel_of_mono [has_limit (parallel_pair f 0)]
[has_colimit (parallel_pair (kernel.ι f) 0)] [mono f] : is_iso (cokernel.π (kernel.ι f)) :=
coequalizer.π_of_self' _ _ $ kernel.ι_of_mono f
coequalizer.π_of_eq $ kernel.ι_of_mono f

end has_zero_object

Expand Down

0 comments on commit d9941af

Please sign in to comment.