Morphism properties defined in concrete categories

In this file, we define the class of morphisms MorphismProperty.injective, MorphismProperty.surjective, MorphismProperty.bijective in concrete categories, and show that it is stable under composition and respect isomorphisms.

We introduce type-classes HasSurjectiveInjectiveFactorization and HasFunctorialSurjectiveInjectiveFactorization expressing that in a concrete category C, all morphisms can be factored (resp. factored functorially) as a surjective map followed by an injective map.

def CategoryTheory.MorphismProperty.injective (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : MorphismProperty C

Injectiveness (in a concrete category) as a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.injective C f = Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

def CategoryTheory.MorphismProperty.surjective (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : MorphismProperty C

Surjectiveness (in a concrete category) as a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.surjective C f = Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

def CategoryTheory.MorphismProperty.bijective (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : MorphismProperty C

Bijectiveness (in a concrete category) as a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.bijective C f = Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem CategoryTheory.MorphismProperty.bijective_eq_sup (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : MorphismProperty.bijective C = MorphismProperty.injective C ⊓ MorphismProperty.surjective C

instance CategoryTheory.MorphismProperty.instIsMultiplicativeInjective (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : (MorphismProperty.injective C).IsMultiplicative

instance CategoryTheory.MorphismProperty.instIsMultiplicativeSurjective (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : (MorphismProperty.surjective C).IsMultiplicative

instance CategoryTheory.MorphismProperty.instIsMultiplicativeBijective (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : (MorphismProperty.bijective C).IsMultiplicative

instance CategoryTheory.MorphismProperty.injective_respectsIso (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : (MorphismProperty.injective C).RespectsIso

instance CategoryTheory.MorphismProperty.surjective_respectsIso (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : (MorphismProperty.surjective C).RespectsIso

instance CategoryTheory.MorphismProperty.bijective_respectsIso (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : (MorphismProperty.bijective C).RespectsIso

@[reducible, inline]

abbrev CategoryTheory.ConcreteCategory.HasSurjectiveInjectiveFactorization (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : Prop

The property that any morphism in a concrete category can be factored as a surjective map followed by an injective map.

Equations

• CategoryTheory.ConcreteCategory.HasSurjectiveInjectiveFactorization C = (CategoryTheory.MorphismProperty.surjective C).HasFactorization (CategoryTheory.MorphismProperty.injective C)

@[reducible, inline]

abbrev CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : Prop

The property that any morphism in a concrete category can be functorially factored as a surjective map followed by an injective map.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData (C : Type u) [Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] : Type (max u v)

The structure containing the data of a functorial factorization of morphisms as a surjective map followed by an injective map in a concrete category.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.functorialSurjectiveInjectiveFactorizationData : ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData (Type u)

In the category of types, any map can be functorially factored as a surjective map followed by an injective map.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationTypeHomObjForget : ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization (Type u)