Documentation

Mathlib.CategoryTheory.MorphismProperty.Concrete

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.

source
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
Instances For
    source
    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
    Instances For
      source
      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
      Instances For
        source
        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
        source
        instance CategoryTheory.MorphismProperty.instIsMultiplicativeInjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] :
        (CategoryTheory.MorphismProperty.injective C).IsMultiplicative
        Equations
        • ⋯ = ⋯
        source
        instance CategoryTheory.MorphismProperty.instIsMultiplicativeSurjective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] :
        (CategoryTheory.MorphismProperty.surjective C).IsMultiplicative
        Equations
        • ⋯ = ⋯
        source
        instance CategoryTheory.MorphismProperty.instIsMultiplicativeBijective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] :
        (CategoryTheory.MorphismProperty.bijective C).IsMultiplicative
        Equations
        • ⋯ = ⋯
        source
        instance CategoryTheory.MorphismProperty.injective_respectsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] :
        (CategoryTheory.MorphismProperty.injective C).RespectsIso
        Equations
        • ⋯ = ⋯
        source
        instance CategoryTheory.MorphismProperty.surjective_respectsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] :
        (CategoryTheory.MorphismProperty.surjective C).RespectsIso
        Equations
        • ⋯ = ⋯
        source
        instance CategoryTheory.MorphismProperty.bijective_respectsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] :
        (CategoryTheory.MorphismProperty.bijective C).RespectsIso
        Equations
        • ⋯ = ⋯
        source
        @[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
        Instances For
          source
          @[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.
          Instances For
            source
            @[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.
            Instances For
              source
              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.
              Instances For
                source
                instance CategoryTheory.instHasFunctorialSurjectiveInjectiveFactorizationType :
                CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization (Type u)
                Equations