Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Module docstring

{"# Strong epimorphisms

In this file, we define strong epimorphisms. A strong epimorphism is an epimorphism f which has the (unique) left lifting property with respect to monomorphisms. Similarly, a strong monomorphisms in a monomorphism which has the (unique) right lifting property with respect to epimorphisms.

Main results

Besides the definition, we show that * the composition of two strong epimorphisms is a strong epimorphism, * 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

We also define classes StrongMonoCategory and StrongEpiCategory for categories in which every monomorphism or epimorphism is strong, and deduce that these categories are balanced.

TODO

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

References

[F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1] "}

CategoryTheory.StrongEpi structure

(f : P ⟶ Q)

Full source

/-- A strong epimorphism `f` is an epimorphism which has the left lifting property
with respect to monomorphisms. -/
class StrongEpi (f : P ⟶ Q) : Prop where
  /-- 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

Strong epimorphism

Informal description

A morphism $ f \colon P \to Q $ in a category is called a *strong epimorphism* if it is an epimorphism and has the left lifting property with respect to all monomorphisms. That is, for any monomorphism $ z \colon X \to Y $ and any commutative square formed by $ u \colon P \to X $, $ v \colon Q \to Y $, and $ f $, there exists a lift $ Q \to X $ making the diagram commute.

CategoryTheory.StrongEpi.mk' theorem

 {f : P ⟶ Q} [Epi f]
  (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

Full source

theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f]
    (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⟩ }

Characterization of Strong Epimorphisms via Lifting Property

Informal description

Let $f \colon P \to Q$ be an epimorphism in a category $\mathcal{C}$. If for every monomorphism $z \colon X \to Y$ and every commutative square formed by morphisms $u \colon P \to X$, $v \colon Q \to Y$ such that $u = z \circ v \circ f$, there exists a lift $\ell \colon Q \to X$ making the diagram commute, then $f$ is a strong epimorphism.

CategoryTheory.StrongMono structure

(f : P ⟶ Q)

Full source

/-- A strong monomorphism `f` is a monomorphism which has the right lifting property
with respect to epimorphisms. -/
class StrongMono (f : P ⟶ Q) : Prop where
  /-- 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

Strong monomorphism

Informal description

A morphism $ f \colon P \to Q $ in a category is called a *strong monomorphism* if it is a monomorphism and has the right lifting property with respect to all epimorphisms. That is, for any epimorphism $ z \colon X \to Y $ and any commutative square formed by $ u \colon X \to P $, $ v \colon Y \to Q $, and $ f $, there exists a lift $ Y \to P $ making the diagram commute.

CategoryTheory.StrongMono.mk' theorem

 {f : P ⟶ Q} [Mono f]
  (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

Full source

theorem StrongMono.mk' {f : P ⟶ Q} [Mono f]
    (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⟩

Characterization of Strong Monomorphisms via Lifting Property

Informal description

Let $f \colon P \to Q$ be a monomorphism in a category. If for every epimorphism $z \colon X \to Y$ and every commutative square formed by morphisms $u \colon X \to P$, $v \colon Y \to Q$ such that $u \circ z = f \circ v$, there exists a lift $Y \to P$ making the diagram commute, then $f$ is a strong monomorphism.

CategoryTheory.epi_of_strongEpi instance

(f : P ⟶ Q) [StrongEpi f] : Epi f

Full source

instance (priority := 100) epi_of_strongEpi (f : P ⟶ Q) [StrongEpi f] : Epi f :=
  StrongEpi.epi

Strong Epimorphisms are Epimorphisms

Informal description

For any strong epimorphism $f \colon P \to Q$ in a category, $f$ is an epimorphism.

CategoryTheory.mono_of_strongMono instance

(f : P ⟶ Q) [StrongMono f] : Mono f

Full source

instance (priority := 100) mono_of_strongMono (f : P ⟶ Q) [StrongMono f] : Mono f :=
  StrongMono.mono

Strong Monomorphisms are Monomorphisms

Informal description

For any strong monomorphism $f \colon P \to Q$ in a category, $f$ is a monomorphism.

CategoryTheory.strongEpi_comp theorem

[StrongEpi f] [StrongEpi g] : StrongEpi (f ≫ g)

Full source

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

Composition of Strong Epimorphisms is Strong Epimorphism

Informal description

Let $f \colon P \to Q$ and $g \colon Q \to R$ be strong epimorphisms in a category. Then their composition $f \circ g \colon P \to R$ is also a strong epimorphism.

CategoryTheory.strongMono_comp theorem

[StrongMono f] [StrongMono g] : StrongMono (f ≫ g)

Full source

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

Composition of Strong Monomorphisms is Strong Monomorphism

Informal description

If $f \colon P \to Q$ and $g \colon Q \to R$ are strong monomorphisms in a category, then their composition $f \circ g \colon P \to R$ is also a strong monomorphism.

CategoryTheory.strongEpi_of_strongEpi theorem

[StrongEpi (f ≫ g)] : StrongEpi g

Full source

/-- 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 := 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]
      exact
        CommSq.HasLift.mk'
          ⟨(CommSq.mk h₀).lift, by
            simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩ }

Strong Epimorphism Property Preserved Under Composition Factors

Informal description

If the composition $f \circ g$ of morphisms $f \colon P \to Q$ and $g \colon Q \to R$ in a category is a strong epimorphism, then $g$ is also a strong epimorphism.

CategoryTheory.strongMono_of_strongMono theorem

[StrongMono (f ≫ g)] : StrongMono f

Full source

/-- 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 := fun {X Y} z => by
      intros
      constructor
      intro u v sq
      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]⟩ }

Strong monomorphisms are preserved under composition factors

Informal description

If the composition $f \circ g$ is a strong monomorphism, then $f$ is also a strong monomorphism.

CategoryTheory.strongEpi_of_isIso instance

[IsIso f] : StrongEpi f

Full source

/-- An isomorphism is in particular a strong epimorphism. -/
instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f where
  epi := by infer_instance
  llp {_ _} _ := HasLiftingProperty.of_left_iso _ _

Isomorphisms are Strong Epimorphisms

Informal description

Every isomorphism $f$ in a category is a strong epimorphism.

CategoryTheory.strongMono_of_isIso instance

[IsIso f] : StrongMono f

Full source

/-- An isomorphism is in particular a strong monomorphism. -/
instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f where
  mono := by infer_instance
  rlp {_ _} _ := HasLiftingProperty.of_right_iso _ _

Isomorphisms are Strong Monomorphisms

Informal description

Every isomorphism in a category is a strong monomorphism.

CategoryTheory.StrongEpi.of_arrow_iso theorem

{A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongEpi f] : StrongEpi g

Full source

theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
    (e : Arrow.mkArrow.mk f ≅ Arrow.mk g) [h : StrongEpi f] : StrongEpi g :=
  { epi := by
      rw [Arrow.iso_w' e]
      infer_instance
    llp := fun {X Y} z => by
      intro
      apply HasLiftingProperty.of_arrow_iso_left e z }

Strong Epimorphism Property Preserved Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f \colon A \to B$ and $g \colon A' \to B'$ be morphisms in $\mathcal{C}$. If there exists an isomorphism $e$ between the arrows $\text{Arrow.mk}(f)$ and $\text{Arrow.mk}(g)$, and $f$ is a strong epimorphism, then $g$ is also a strong epimorphism.

CategoryTheory.StrongMono.of_arrow_iso theorem

{A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongMono f] : StrongMono g

Full source

theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
    (e : Arrow.mkArrow.mk f ≅ Arrow.mk g) [h : StrongMono f] : StrongMono g :=
  { mono := by
      rw [Arrow.iso_w' e]
      infer_instance
    rlp := fun {X Y} z => by
      intro
      apply HasLiftingProperty.of_arrow_iso_right z e }

Strong Monomorphism Property Preserved Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f \colon A \to B$ and $g \colon A' \to B'$ be morphisms in $\mathcal{C}$. If there exists an isomorphism between the arrows $\text{Arrow.mk}\, f$ and $\text{Arrow.mk}\, g$ (viewed as objects in the arrow category), and $f$ is a strong monomorphism, then $g$ is also a strong monomorphism.

CategoryTheory.StrongEpi.iff_of_arrow_iso theorem

{A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g

Full source

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

Strong Epimorphism Property is Preserved Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f \colon A \to B$ and $g \colon A' \to B'$ be morphisms in $\mathcal{C}$. Given an isomorphism $e$ between the arrows $\text{Arrow.mk}(f)$ and $\text{Arrow.mk}(g)$, the morphism $f$ is a strong epimorphism if and only if $g$ is a strong epimorphism.

CategoryTheory.StrongMono.iff_of_arrow_iso theorem

{A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g

Full source

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

Strong Monomorphism Property is Preserved Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $f \colon A \to B$ and $g \colon A' \to B'$ be morphisms in $\mathcal{C}$. Given an isomorphism $e$ between the arrows $\text{Arrow.mk}\, f$ and $\text{Arrow.mk}\, g$ (viewed as objects in the arrow category), $f$ is a strong monomorphism if and only if $g$ is a strong monomorphism.

CategoryTheory.isIso_of_mono_of_strongEpi theorem

(f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f

Full source

/-- 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 simp⟩⟩

Strong epimorphism that is a monomorphism is an isomorphism

Informal description

Let $ f \colon P \to Q $ be a morphism in a category. If $ f $ is both a monomorphism and a strong epimorphism, then $ f $ is an isomorphism.

CategoryTheory.isIso_of_epi_of_strongMono theorem

(f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f

Full source

/-- 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 simp⟩⟩

Strong Monomorphism that is an Epimorphism is an Isomorphism

Informal description

Let $ f \colon P \to Q $ be a morphism in a category. If $ f $ is both an epimorphism and a strong monomorphism, then $ f $ is an isomorphism.

CategoryTheory.StrongEpiCategory structure

Full source

/-- 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

Strong epi category

Informal description

A category is called a strong epi category if every epimorphism in the category is a strong epimorphism, meaning it has the unique left lifting property with respect to all monomorphisms.

CategoryTheory.StrongMonoCategory structure

Full source

/-- 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

Strong Mono Category

Informal description

A category is called a *strong mono category* if every monomorphism in the category is a strong monomorphism, meaning it has the unique right lifting property with respect to all epimorphisms.

CategoryTheory.strongEpi_of_epi theorem

[StrongEpiCategory C] (f : P ⟶ Q) [Epi f] : StrongEpi f

Full source

theorem strongEpi_of_epi [StrongEpiCategory C] (f : P ⟶ Q) [Epi f] : StrongEpi f :=
  StrongEpiCategory.strongEpi_of_epi _

Epimorphisms are Strong in a Strong Epi Category

Informal description

In a strong epi category $C$, every epimorphism $f \colon P \to Q$ is a strong epimorphism.

CategoryTheory.strongMono_of_mono theorem

[StrongMonoCategory C] (f : P ⟶ Q) [Mono f] : StrongMono f

Full source

theorem strongMono_of_mono [StrongMonoCategory C] (f : P ⟶ Q) [Mono f] : StrongMono f :=
  StrongMonoCategory.strongMono_of_mono _

Monomorphisms are Strong in a Strong Mono Category

Informal description

In a strong mono category $C$, every monomorphism $f \colon P \to Q$ is a strong monomorphism.

CategoryTheory.balanced_of_strongEpiCategory instance

[StrongEpiCategory C] : Balanced C

Full source

instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C where
  isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _

Strong Epi Categories are Balanced

Informal description

Every strong epi category is balanced, meaning that every morphism which is both a monomorphism and an epimorphism is an isomorphism.

CategoryTheory.balanced_of_strongMonoCategory instance

[StrongMonoCategory C] : Balanced C

Full source

instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C where
  isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _

Strong Mono Categories are Balanced

Informal description

Every strong mono category is balanced, meaning that every morphism which is both a monomorphism and an epimorphism is an isomorphism.