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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty C

Injectiveness (in a concrete category) as a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.injective C f = Function.Injective ⇑f

def CategoryTheory.MorphismProperty.surjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty C

Surjectiveness (in a concrete category) as a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.surjective C f = Function.Surjective ⇑f

def CategoryTheory.MorphismProperty.bijective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty C

Bijectiveness (in a concrete category) as a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.bijective C f = Function.Bijective ⇑f

theorem CategoryTheory.MorphismProperty.bijective_eq_sup (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.bijective C = CategoryTheory.MorphismProperty.injective C ⊓ CategoryTheory.MorphismProperty.surjective C

instance CategoryTheory.MorphismProperty.instIsMultiplicativeInjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : (CategoryTheory.MorphismProperty.injective C).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.instIsMultiplicativeSurjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : (CategoryTheory.MorphismProperty.surjective C).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.instIsMultiplicativeBijective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : (CategoryTheory.MorphismProperty.bijective C).IsMultiplicative

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.injective_respectsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : (CategoryTheory.MorphismProperty.injective C).RespectsIso

theorem CategoryTheory.MorphismProperty.surjective_respectsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : (CategoryTheory.MorphismProperty.surjective C).RespectsIso

theorem CategoryTheory.MorphismProperty.bijective_respectsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : (CategoryTheory.MorphismProperty.bijective C).RespectsIso

@[reducible, inline]

abbrev CategoryTheory.ConcreteCategory.HasSurjectiveInjectiveFactorization (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : 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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : 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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : 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 : CategoryTheory.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.instHasFunctorialSurjectiveInjectiveFactorizationType : CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization (Type u)

Equations

• CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationType = ⋯