mathlib documentation

category_theory.limits.shapes.strong_epi

Strong epimorphisms #

In this file, we define strong epimorphisms. A strong epimorphism is an epimorphism f, such that for every commutative square with f at the top and a monomorphism at the bottom, there is a diagonal morphism making the two triangles commute. This lift is necessarily unique (as shown in comma.lean).

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 such that every commutative square with f at the top and a monomorphism at the bottom has a lift.

Instances of this typeclass
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 such that every commutative square with f at the bottom and an epimorphism at the top has a lift.

Instances of this typeclass
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.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