Documentation

Mathlib.CategoryTheory.Subpresheaf.Image

The image of a subpresheaf #

Given a morphism of presheaves of types p : F' ⟶ F, we define its range Subpresheaf.range p. More generally, if G' : Subpresheaf F', we define G'.image p : Subpresheaf F as the image of G' by f, and if G : Subpresheaf F, we define its preimage G.preimage f : Subpresheaf F'.

The range of a morphism of presheaves of types, as a subpresheaf of the target.

Equations
Instances For
    @[simp]

    If the image of a morphism falls in a subpresheaf, then the morphism factors through it.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.Subpresheaf.lift_app_coe {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' F) {G : Subpresheaf F} (hf : range f G) (U : Cᵒᵖ) (x : F'.obj U) :
      ((lift f hf).app U x) = f.app U x
      @[simp]
      theorem CategoryTheory.Subpresheaf.lift_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' F) {G : Subpresheaf F} (hf : range f G) :

      Given a morphism p : F' ⟶ F of presheaves of types, this is the morphism from F' to its range.

      Equations
      Instances For
        theorem CategoryTheory.Subpresheaf.toRange_app_val {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' F) {i : Cᵒᵖ} (x : F'.obj i) :
        ((toRange p).app i x) = p.app i x

        The image of a subpresheaf by a morphism of presheaves of types.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Subpresheaf.image_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F F') (i : Cᵒᵖ) :
          (G.image f).obj i = f.app i '' G.obj i

          The preimage of a subpresheaf by a morphism of presheaves of types.

          Equations
          Instances For

            Given a morphism p : F' ⟶ F of presheaves of types and G : Subpresheaf F, this is the morphism from the preimage of G by p to G.

            Equations
            Instances For
              @[deprecated CategoryTheory.Subpresheaf.range (since := "2025-01-25")]

              Alias of CategoryTheory.Subpresheaf.range.


              The range of a morphism of presheaves of types, as a subpresheaf of the target.

              Equations
              Instances For
                @[deprecated CategoryTheory.Subpresheaf.range_id (since := "2025-01-25")]

                Alias of CategoryTheory.Subpresheaf.range_id.

                @[deprecated CategoryTheory.Subpresheaf.toRange (since := "2025-01-25")]

                Alias of CategoryTheory.Subpresheaf.toRange.


                Given a morphism p : F' ⟶ F of presheaves of types, this is the morphism from F' to its range.

                Equations
                Instances For
                  @[deprecated CategoryTheory.Subpresheaf.toRange_ι (since := "2025-01-25")]

                  Alias of CategoryTheory.Subpresheaf.toRange_ι.

                  @[deprecated CategoryTheory.Subpresheaf.range_comp_le (since := "2025-01-25")]

                  Alias of CategoryTheory.Subpresheaf.range_comp_le.