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] - chore(category_theory/limits): dualize strong_epi #11783

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(category_theory/limits): dualize strong_epi #11783

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
101048d
chore(category_theory/limits): dualize strong_epi
TwoFX Feb 2, 2022
43e559b
Add TODO
TwoFX Feb 3, 2022
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
5 changes: 4 additions & 1 deletion src/category_theory/abelian/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,11 +139,14 @@ def non_preadditive_abelian : non_preadditive_abelian C := { ..‹abelian C› }
end to_non_preadditive_abelian

section strong
local attribute [instance] abelian.normal_epi
local attribute [instance] abelian.normal_epi abelian.normal_mono

/-- In an abelian category, every epimorphism is strong. -/
lemma strong_epi_of_epi {P Q : C} (f : P ⟶ Q) [epi f] : strong_epi f := by apply_instance

/-- In an abelian category, every monomorphism is strong. -/
lemma strong_mono_of_mono {P Q : C} (f : P ⟶ Q) [mono f] : strong_mono f := by apply_instance

end strong

section mono_epi_iso
Expand Down
24 changes: 19 additions & 5 deletions src/category_theory/limits/shapes/regular_mono.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,9 +113,23 @@ def regular_of_is_pullback_fst_of_regular {P Q R S : C} {f : P ⟶ Q} {g : P ⟶
regular_mono f :=
regular_of_is_pullback_snd_of_regular comm.symm (pullback_cone.flip_is_limit t)

@[priority 100]
instance strong_mono_of_regular_mono (f : X ⟶ Y) [regular_mono f] : strong_mono f :=
{ mono := by apply_instance,
has_lift :=
begin
introsI,
have : v ≫ (regular_mono.left : Y ⟶ regular_mono.Z f) = v ≫ regular_mono.right,
{ apply (cancel_epi z).1,
simp only [regular_mono.w, ← reassoc_of h] },
obtain ⟨t, ht⟩ := regular_mono.lift' _ _ this,
refine arrow.has_lift.mk ⟨t, (cancel_mono f).1 _, ht⟩,
simp only [arrow.mk_hom, arrow.hom_mk'_left, category.assoc, ht, h]
end }

/-- A regular monomorphism is an isomorphism if it is an epimorphism. -/
lemma is_iso_of_regular_mono_of_epi (f : X ⟶ Y) [regular_mono f] [e : epi f] : is_iso f :=
@is_iso_limit_cone_parallel_pair_of_epi _ _ _ _ _ _ _ regular_mono.is_limit e
is_iso_of_epi_of_strong_mono _

/-- A regular epimorphism is a morphism which is the coequalizer of some parallel pair. -/
class regular_epi (f : X ⟶ Y) :=
Expand Down Expand Up @@ -199,10 +213,6 @@ def regular_of_is_pushout_fst_of_regular
regular_epi k :=
regular_of_is_pushout_snd_of_regular comm.symm (pushout_cocone.flip_is_colimit t)

/-- A regular epimorphism is an isomorphism if it is a monomorphism. -/
lemma is_iso_of_regular_epi_of_mono (f : X ⟶ Y) [regular_epi f] [m : mono f] : is_iso f :=
@is_iso_limit_cocone_parallel_pair_of_epi _ _ _ _ _ _ _ regular_epi.is_colimit m

@[priority 100]
instance strong_epi_of_regular_epi (f : X ⟶ Y) [regular_epi f] : strong_epi f :=
{ epi := by apply_instance,
Expand All @@ -217,4 +227,8 @@ instance strong_epi_of_regular_epi (f : X ⟶ Y) [regular_epi f] : strong_epi f
(by simp only [←category.assoc, ht, ←h, arrow.mk_hom, arrow.hom_mk'_right])⟩,
end }

/-- A regular epimorphism is an isomorphism if it is a monomorphism. -/
lemma is_iso_of_regular_epi_of_mono (f : X ⟶ Y) [regular_epi f] [m : mono f] : is_iso f :=
is_iso_of_mono_of_strong_epi _

end category_theory
51 changes: 48 additions & 3 deletions src/category_theory/limits/shapes/strong_epi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,10 @@ Besides the definition, we show that
* if `f ≫ g` is a strong epimorphism, then so is `g`,
* if `f` is both a strong epimorphism and a monomorphism, then it is an isomorphism

## Future work

There is also the dual notion of strong monomorphism.
## TODO

Show that the dual of a strong epimorphism is a strong monomorphism, and vice versa.

## References

Expand All @@ -43,11 +44,22 @@ class strong_epi (f : P ⟶ Q) : Prop :=
(has_lift : Π {X Y : C} {u : P ⟶ X} {v : Q ⟶ Y} {z : X ⟶ Y} [mono z] (h : u ≫ z = f ≫ v),
arrow.has_lift $ arrow.hom_mk' h)

/-- A strong monomorphism `f` is a monomorphism such that every commutative square with `f` at the
bottom and an epimorphism at the top has a lift. -/
class strong_mono (f : P ⟶ Q) : Prop :=
(mono : mono f)
(has_lift : Π {X Y : C} {u : X ⟶ P} {v : Y ⟶ Q} {z : X ⟶ Y} [epi z] (h : u ≫ f = z ≫ v),
arrow.has_lift $ arrow.hom_mk' h)

attribute [instance] strong_epi.has_lift
attribute [instance] strong_mono.has_lift

@[priority 100]
instance epi_of_strong_epi (f : P ⟶ Q) [strong_epi f] : epi f := strong_epi.epi

@[priority 100]
instance mono_of_strong_mono (f : P ⟶ Q) [strong_mono f] : mono f := strong_mono.mono

section
variables {R : C} (f : P ⟶ Q) (g : Q ⟶ R)

Expand All @@ -63,7 +75,19 @@ lemma strong_epi_comp [strong_epi f] [strong_epi g] : strong_epi (f ≫ g) :=
exact arrow.has_lift.mk ⟨(arrow.lift (arrow.hom_mk' h₁) : R ⟶ X), by simp, by simp⟩
end }

/-- If `f ≫ g` is a strong epimorphism, then so is g. -/
/-- The composition of two strong monomorphisms is a strong monomorphism. -/
lemma strong_mono_comp [strong_mono f] [strong_mono g] : strong_mono (f ≫ g) :=
{ mono := mono_comp _ _,
has_lift :=
begin
introsI,
have h₀ : (u ≫ f) ≫ g = z ≫ v, by simpa [category.assoc] using h,
let w : Y ⟶ Q := arrow.lift (arrow.hom_mk' h₀),
have h₁ : u ≫ f = z ≫ w, by rw arrow.lift_mk'_left,
exact arrow.has_lift.mk ⟨(arrow.lift (arrow.hom_mk' h₁) : Y ⟶ P), by simp, by simp⟩
end }

/-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/
lemma strong_epi_of_strong_epi [strong_epi (f ≫ g)] : strong_epi g :=
{ epi := epi_of_epi f g,
has_lift :=
Expand All @@ -74,15 +98,36 @@ lemma strong_epi_of_strong_epi [strong_epi (f ≫ g)] : strong_epi g :=
⟨(arrow.lift (arrow.hom_mk' h₀) : R ⟶ X), (cancel_mono z).1 (by simp [h]), by simp⟩,
end }

/-- If `f ≫ g` is a strong monomorphism, then so is `f`. -/
lemma strong_mono_of_strong_mono [strong_mono (f ≫ g)] : strong_mono f :=
{ mono := mono_of_mono f g,
has_lift :=
begin
introsI,
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g, by rw reassoc_of h,
exact arrow.has_lift.mk
⟨(arrow.lift (arrow.hom_mk' h₀) : Y ⟶ P), by simp, (cancel_epi z).1 (by simp [h])⟩
end }

/-- An isomorphism is in particular a strong epimorphism. -/
@[priority 100] instance strong_epi_of_is_iso [is_iso f] : strong_epi f :=
{ epi := by apply_instance,
has_lift := λ X Y u v z _ h, arrow.has_lift.mk ⟨inv f ≫ u, by simp, by simp [h]⟩ }

/-- An isomorphism is in particular a strong monomorphism. -/
@[priority 100] instance strong_mono_of_is_iso [is_iso f] : strong_mono f :=
{ mono := by apply_instance,
has_lift := λ X Y u v z _ h, arrow.has_lift.mk
⟨v ≫ inv f, by simp [← category.assoc, ← h], by simp⟩ }

end

/-- A strong epimorphism that is a monomorphism is an isomorphism. -/
lemma is_iso_of_mono_of_strong_epi (f : P ⟶ Q) [mono f] [strong_epi f] : is_iso f :=
⟨⟨arrow.lift $ arrow.hom_mk' $ show 𝟙 P ≫ f = f ≫ 𝟙 Q, by simp, by tidy⟩⟩

/-- A strong monomorphism that is an epimorphism is an isomorphism. -/
lemma is_iso_of_epi_of_strong_mono (f : P ⟶ Q) [epi f] [strong_mono f] : is_iso f :=
⟨⟨arrow.lift $ arrow.hom_mk' $ show 𝟙 P ≫ f = f ≫ 𝟙 Q, by simp, by tidy⟩⟩

end category_theory