Documentation

Mathlib.CategoryTheory.Preadditive.Injective

Injective objects and categories with enough injectives #

An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

Instances
    theorem CategoryTheory.Injective.factors {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : C} [self : CategoryTheory.Injective J] {X : C} {Y : C} (g : X J) (f : X Y) [CategoryTheory.Mono f] :

    An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

    An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • J : C

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • injective : CategoryTheory.Injective self.J

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • f : X self.J

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • mono : CategoryTheory.Mono self.f

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    Instances For

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

      A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

      • presentation : ∀ (X : C), Nonempty (CategoryTheory.InjectivePresentation X)

        A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

      Instances

        A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

        Let J be injective and g a morphism into J, then g can be factored through any monomorphism.

        Equations
        Instances For

          The axiom of choice says that every nonempty type is an injective object in Type.

          Equations
          • =

          Injective.under X provides an arbitrarily chosen injective object equipped with a monomorphism Injective.ι : X ⟶ Injective.under X.

          Equations
          Instances For

            The monomorphism Injective.ι : X ⟶ Injective.under X from the arbitrarily chosen injective object under X.

            Equations
            Instances For
              @[reducible, inline]

              When C has enough injective, Injective.d f : Y ⟶ syzygies f is the composition cokernel.π fι (cokernel f).

              (When C is abelian, we have exact f (injective.d f).)

              Equations
              Instances For

                Given an adjunction F ⊣ G such that F preserves monos, G maps an injective presentation of X to an injective presentation of G(X).

                Equations
                • adj.mapInjectivePresentation X I = { J := G.obj I.J, injective := , f := G.map I.f, mono := }
                Instances For

                  Given an adjunction F ⊣ G such that F preserves monomorphisms and is faithful, then any injective presentation of F(X) can be pulled back to an injective presentation of X. This is similar to mapInjectivePresentation.

                  Equations
                  • adj.injectivePresentationOfMap X I = { J := G.obj I.J, injective := , f := (adj.homEquiv X I.J) I.f, mono := }
                  Instances For

                    Given an equivalence of categories F, an injective presentation of F(X) induces an injective presentation of X.

                    Equations
                    • F.injectivePresentationOfMapInjectivePresentation X I = F.toAdjunction.injectivePresentationOfMap X I
                    Instances For