mathlib3 documentation

category_theory.limits.shapes.strong_epi

Strong epimorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We also define classes strong_mono_category and strong_epi_category 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 #

source
@[class]
structure category_theory.strong_epi {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) :
Prop

A strong epimorphism f is an epimorphism which has the left lifting property with respect to monomorphisms.

Instances of this typeclass
source
theorem category_theory.strong_epi.mk' {C : Type u} [category_theory.category C] {P Q : C} {f : P ⟶ Q} [category_theory.epi f] (hf : ∀ (X Y : C) (z : X ⟶ Y), category_theory.mono z → ∀ (u : P ⟶ X) (v : Q ⟶ Y) (sq : category_theory.comm_sq u f z v), sq.has_lift) :
category_theory.strong_epi f
source
@[class]
structure category_theory.strong_mono {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) :
Prop

A strong monomorphism f is a monomorphism which has the right lifting property with respect to epimorphisms.

Instances of this typeclass
source
theorem category_theory.strong_mono.mk' {C : Type u} [category_theory.category C] {P Q : C} {f : P ⟶ Q} [category_theory.mono f] (hf : ∀ (X Y : C) (z : X ⟶ Y), category_theory.epi z → ∀ (u : X ⟶ P) (v : Y ⟶ Q) (sq : category_theory.comm_sq u z f v), sq.has_lift) :
category_theory.strong_mono f
source
@[protected, instance]
def category_theory.epi_of_strong_epi {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.strong_epi f] :
category_theory.epi f
source
@[protected, instance]
def category_theory.mono_of_strong_mono {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.strong_mono f] :
category_theory.mono f
source
theorem category_theory.strong_epi_comp {C : Type u} [category_theory.category C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.strong_epi f] [category_theory.strong_epi g] :
category_theory.strong_epi (f ≫ g)

The composition of two strong epimorphisms is a strong epimorphism.

source
theorem category_theory.strong_mono_comp {C : Type u} [category_theory.category C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.strong_mono f] [category_theory.strong_mono g] :
category_theory.strong_mono (f ≫ g)

The composition of two strong monomorphisms is a strong monomorphism.

source
theorem category_theory.strong_epi_of_strong_epi {C : Type u} [category_theory.category C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.strong_epi (f ≫ g)] :
category_theory.strong_epi g

If f ≫ g is a strong epimorphism, then so is g.

source
theorem category_theory.strong_mono_of_strong_mono {C : Type u} [category_theory.category C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.strong_mono (f ≫ g)] :
category_theory.strong_mono f

If f ≫ g is a strong monomorphism, then so is f.

source
@[protected, instance]
def category_theory.strong_epi_of_is_iso {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.is_iso f] :
category_theory.strong_epi f

An isomorphism is in particular a strong epimorphism.

source
@[protected, instance]
def category_theory.strong_mono_of_is_iso {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.is_iso f] :
category_theory.strong_mono f

An isomorphism is in particular a strong monomorphism.

source
theorem category_theory.strong_epi.of_arrow_iso {C : Type u} [category_theory.category C] {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) [h : category_theory.strong_epi f] :
category_theory.strong_epi g
source
theorem category_theory.strong_mono.of_arrow_iso {C : Type u} [category_theory.category C] {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) [h : category_theory.strong_mono f] :
category_theory.strong_mono g
source
theorem category_theory.strong_epi.iff_of_arrow_iso {C : Type u} [category_theory.category C] {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) :
category_theory.strong_epi f ↔ category_theory.strong_epi g
source
theorem category_theory.strong_mono.iff_of_arrow_iso {C : Type u} [category_theory.category C] {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'} (e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) :
category_theory.strong_mono f ↔ category_theory.strong_mono g
source
theorem category_theory.is_iso_of_mono_of_strong_epi {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.mono f] [category_theory.strong_epi f] :
category_theory.is_iso f

A strong epimorphism that is a monomorphism is an isomorphism.

source
theorem category_theory.is_iso_of_epi_of_strong_mono {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.epi f] [category_theory.strong_mono f] :
category_theory.is_iso f

A strong monomorphism that is an epimorphism is an isomorphism.

source
@[class]
structure category_theory.strong_epi_category (C : Type u) [category_theory.category C] :
Prop

A strong epi category is a category in which every epimorphism is strong.

Instances of this typeclass
source
@[class]
structure category_theory.strong_mono_category (C : Type u) [category_theory.category C] :
Prop

A strong mono category is a category in which every monomorphism is strong.

Instances of this typeclass
source
theorem category_theory.strong_epi_of_epi {C : Type u} [category_theory.category C] {P Q : C} [category_theory.strong_epi_category C] (f : P ⟶ Q) [category_theory.epi f] :
category_theory.strong_epi f
source
theorem category_theory.strong_mono_of_mono {C : Type u} [category_theory.category C] {P Q : C} [category_theory.strong_mono_category C] (f : P ⟶ Q) [category_theory.mono f] :
category_theory.strong_mono f
source
@[protected, instance]
def category_theory.balanced_of_strong_epi_category {C : Type u} [category_theory.category C] [category_theory.strong_epi_category C] :
category_theory.balanced C
source
@[protected, instance]
def category_theory.balanced_of_strong_mono_category {C : Type u} [category_theory.category C] [category_theory.strong_mono_category C] :
category_theory.balanced C