Skip to content

Commit

Permalink
fix errors; lint
Browse files Browse the repository at this point in the history
  • Loading branch information
@mattrobball
mattrobball committed Feb 17, 2023
1 parent cbc27d7 commit 118d7ed
Showing 1 changed file with 54 additions and 49 deletions.
103 changes: 54 additions & 49 deletions Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,38 +50,41 @@ variable {P Q : C}
/-- A strong epimorphism `f` is an epimorphism which has the left lifting property
with respect to monomorphisms. -/
class StrongEpi (f : P ⟶ Q) : Prop where
Epi : Epi f
/-- The epimorphism condition on `f` -/
epi : Epi f
/-- The left lifting property with respect to all monomorphism -/
llp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Mono z], HasLiftingProperty f z
#align category_theory.strong_epi CategoryTheory.StrongEpi
#align category_theory.strong_epi.epi CategoryTheory.StrongEpi.epi


theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f]
(hf :
∀ (X Y : C) (z : X ⟶ Y) (hz : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v),
sq.HasLift) :
(hf : ∀ (X Y : C) (z : X ⟶ Y)
(_ : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v), sq.HasLift) :
StrongEpi f :=
{ Epi := inferInstance
llp := fun X Y z hz => ⟨fun u v sq => hf X Y z hz u v sq⟩ }
{ epi := inferInstance
llp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩ }
#align category_theory.strong_epi.mk' CategoryTheory.StrongEpi.mk'

/-- A strong monomorphism `f` is a monomorphism which has the right lifting property
with respect to epimorphisms. -/
class StrongMono (f : P ⟶ Q) : Prop where
Mono : Mono f
/-- The monomorphism condition on `f` -/
mono : Mono f
/-- The right lifting property with respect to all epimorphisms -/
rlp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Epi z], HasLiftingProperty z f
#align category_theory.strong_mono CategoryTheory.StrongMono

theorem StrongMono.mk' {f : P ⟶ Q} [Mono f]
(hf :
∀ (X Y : C) (z : X ⟶ Y) (hz : Epi z) (u : X ⟶ P) (v : Y ⟶ Q) (sq : CommSq u z f v),
sq.HasLift) :
StrongMono f :=
{ Mono := inferInstance
rlp := fun X Y z hz => ⟨fun u v sq => hf X Y z hz u v sq⟩ }
(hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Epi z) (u : X ⟶ P)
(v : Y ⟶ Q) (sq : CommSq u z f v), sq.HasLift) : StrongMono f where
mono := inferInstance
rlp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩
#align category_theory.strong_mono.mk' CategoryTheory.StrongMono.mk'

attribute [instance] strong_epi.llp
attribute [instance] StrongEpi.llp

attribute [instance] strong_mono.rlp
attribute [instance] StrongMono.rlp

instance (priority := 100) epi_of_strongEpi (f : P ⟶ Q) [StrongEpi f] : Epi f :=
StrongEpi.epi
Expand All @@ -97,103 +100,103 @@ variable {R : C} (f : P ⟶ Q) (g : Q ⟶ R)

/-- The composition of two strong epimorphisms is a strong epimorphism. -/
theorem strongEpi_comp [StrongEpi f] [StrongEpi g] : StrongEpi (f ≫ g) :=
{ Epi := epi_comp _ _
{ epi := epi_comp _ _
llp := by
intros
infer_instance }
#align category_theory.strong_epi_comp CategoryTheory.strongEpi_comp

/-- The composition of two strong monomorphisms is a strong monomorphism. -/
theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) :=
{ Mono := mono_comp _ _
{ mono := mono_comp _ _
rlp := by
intros
infer_instance }
#align category_theory.strong_mono_comp CategoryTheory.strongMono_comp

/-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/
theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
{ Epi := epi_of_epi f g
llp := by
intros
{ epi := epi_of_epi f g
llp := fun {X} {Y} z _ => by
constructor
intro u v sq
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [category.assoc, sq.w]
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
exact
comm_sq.has_lift.mk'
⟨(comm_sq.mk h₀).lift, by
simp only [← cancel_mono z, category.assoc, comm_sq.fac_right, sq.w], by simp⟩ }
CommSq.HasLift.mk'
⟨(CommSq.mk h₀).lift, by
simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩ }
#align category_theory.strong_epi_of_strong_epi CategoryTheory.strongEpi_of_strongEpi

/-- If `f ≫ g` is a strong monomorphism, then so is `f`. -/
theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f :=
{ Mono := mono_of_mono f g
rlp := by
{ mono := mono_of_mono f g
rlp := fun {X} {Y} z => by
intros
constructor
intro u v sq
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by rw [reassoc_of sq.w]
exact comm_sq.has_lift.mk' ⟨(comm_sq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩ }
have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by
rw [←Category.assoc, eq_whisker sq.w, Category.assoc]
exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩ }
#align category_theory.strong_mono_of_strong_mono CategoryTheory.strongMono_of_strongMono

/-- An isomorphism is in particular a strong epimorphism. -/
instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f
where
Epi := by infer_instance
llp X Y z hz := HasLiftingProperty.of_left_iso _ _
epi := by infer_instance
llp {X} {Y} z := HasLiftingProperty.of_left_iso _ _
#align category_theory.strong_epi_of_is_iso CategoryTheory.strongEpi_of_isIso

/-- An isomorphism is in particular a strong monomorphism. -/
instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f
where
Mono := by infer_instance
rlp X Y z hz := HasLiftingProperty.of_right_iso _ _
mono := by infer_instance
rlp {X} {Y} z := HasLiftingProperty.of_right_iso _ _
#align category_theory.strong_mono_of_is_iso CategoryTheory.strongMono_of_isIso

theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
(e : Arrow.mk f ≅ Arrow.mk g) [h : StrongEpi f] : StrongEpi g :=
{ Epi := by
rw [arrow.iso_w' e]
{ epi := by
rw [Arrow.iso_w' e]
haveI := epi_comp f e.hom.right
apply epi_comp
llp := fun X Y z => by
llp := fun {X} {Y} z => by
intro
apply has_lifting_property.of_arrow_iso_left e z }
apply HasLiftingProperty.of_arrow_iso_left e z }
#align category_theory.strong_epi.of_arrow_iso CategoryTheory.StrongEpi.of_arrow_iso

theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
(e : Arrow.mk f ≅ Arrow.mk g) [h : StrongMono f] : StrongMono g :=
{ Mono := by
rw [arrow.iso_w' e]
{ mono := by
rw [Arrow.iso_w' e]
haveI := mono_comp f e.hom.right
apply mono_comp
rlp := fun X Y z => by
rlp := fun {X} {Y} z => by
intro
apply has_lifting_property.of_arrow_iso_right z e }
apply HasLiftingProperty.of_arrow_iso_right z e }
#align category_theory.strong_mono.of_arrow_iso CategoryTheory.StrongMono.of_arrow_iso

theorem StrongEpi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
(e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g := by
constructor <;> intro
exacts[strong_epi.of_arrow_iso e, strong_epi.of_arrow_iso e.symm]
exacts[StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]
#align category_theory.strong_epi.iff_of_arrow_iso CategoryTheory.StrongEpi.iff_of_arrow_iso

theorem StrongMono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
(e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g := by
constructor <;> intro
exacts[strong_mono.of_arrow_iso e, strong_mono.of_arrow_iso e.symm]
exacts[StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]
#align category_theory.strong_mono.iff_of_arrow_iso CategoryTheory.StrongMono.iff_of_arrow_iso

end

/-- A strong epimorphism that is a monomorphism is an isomorphism. -/
theorem isIso_of_mono_of_strongEpi (f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f :=
⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by tidy⟩⟩
⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by aesop_cat⟩⟩
#align category_theory.is_iso_of_mono_of_strong_epi CategoryTheory.isIso_of_mono_of_strongEpi

/-- A strong monomorphism that is an epimorphism is an isomorphism. -/
theorem isIso_of_epi_of_strongMono (f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f :=
⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by tidy⟩⟩
⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by aesop_cat⟩⟩
#align category_theory.is_iso_of_epi_of_strong_mono CategoryTheory.isIso_of_epi_of_strongMono

section
Expand All @@ -202,11 +205,13 @@ variable (C)

/-- A strong epi category is a category in which every epimorphism is strong. -/
class StrongEpiCategory : Prop where
/-- A strong epi category is a category in which every epimorphism is strong. -/
strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], StrongEpi f
#align category_theory.strong_epi_category CategoryTheory.StrongEpiCategory

/-- A strong mono category is a category in which every monomorphism is strong. -/
class StrongMonoCategory : Prop where
/-- A strong mono category is a category in which every monomorphism is strong. -/
strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], StrongMono f
#align category_theory.strong_mono_category CategoryTheory.StrongMonoCategory

Expand All @@ -222,23 +227,23 @@ theorem strongMono_of_mono [StrongMonoCategory C] (f : P ⟶ Q) [Mono f] : Stron

section

attribute [local instance] strong_epi_of_epi
attribute [local instance] strongEpi_of_epi

instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C
where isIso_of_mono_of_epi _ _ _ _ _ := is_iso_of_mono_of_strong_epi _
where isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _
#align category_theory.balanced_of_strong_epi_category CategoryTheory.balanced_of_strongEpiCategory

end

section

attribute [local instance] strong_mono_of_mono
attribute [local instance] strongMono_of_mono

instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C
where isIso_of_mono_of_epi _ _ _ _ _ := is_iso_of_epi_of_strong_mono _
where isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _
#align category_theory.balanced_of_strong_mono_category CategoryTheory.balanced_of_strongMonoCategory

end

end CategoryTheory

#lint

0 comments on commit 118d7ed

Please sign in to comment.