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.

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