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'.

source
def CategoryTheory.Subpresheaf.range {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :
Subpresheaf F

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

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Subpresheaf.range_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) (U : Cᵒᵖ) :
      (range p).obj U = Set.range (p.app U)
      source
      theorem CategoryTheory.Subpresheaf.range_id {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) :
      range (CategoryStruct.id F) = ⊤
      source
      @[simp]
      theorem CategoryTheory.Subpresheaf.range_ι {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) :
      range G.ι = G
      source
      def 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) :
      F' ⟶ G.toPresheaf

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

      Equations
        Instances For
          source
          @[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
          source
          @[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) :
          CategoryStruct.comp (lift f hf) G.ι = f
          source
          @[simp]
          theorem CategoryTheory.Subpresheaf.lift_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {G : Subpresheaf F} (hf : range f ≤ G) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) :
          CategoryStruct.comp (lift f hf) (CategoryStruct.comp G.ι h) = CategoryStruct.comp f h
          source
          def CategoryTheory.Subpresheaf.toRange {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :
          F' ⟶ (range p).toPresheaf

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

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Subpresheaf.toRange_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :
              CategoryStruct.comp (toRange p) (range p).ι = p
              source
              @[simp]
              theorem CategoryTheory.Subpresheaf.toRange_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) :
              CategoryStruct.comp (toRange p) (CategoryStruct.comp (range p).ι h) = CategoryStruct.comp p h
              source
              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
              source
              @[simp]
              theorem CategoryTheory.Subpresheaf.range_toRange {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :
              range (toRange p) = ⊤
              source
              theorem CategoryTheory.Subpresheaf.epi_iff_range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :
              Epi p ↔ range p = ⊤
              source
              theorem CategoryTheory.Subpresheaf.range_eq_top {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) [Epi p] :
              range p = ⊤
              source
              instance CategoryTheory.Subpresheaf.instEpiFunctorOppositeTypeToRange {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) :
              Epi (toRange p)
              source
              instance CategoryTheory.Subpresheaf.instIsIsoFunctorOppositeTypeToRangeOfMono {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (p : F' ⟶ F) [Mono p] :
              IsIso (toRange p)
              source
              theorem CategoryTheory.Subpresheaf.range_comp_le {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :
              range (CategoryStruct.comp f g) ≤ range g
              source
              def CategoryTheory.Subpresheaf.image {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') :
              Subpresheaf F'

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

              Equations
                Instances For
                  source
                  @[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
                  source
                  theorem CategoryTheory.Subpresheaf.image_top {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') :
                  ⊤.image f = range f
                  source
                  @[simp]
                  theorem CategoryTheory.Subpresheaf.image_iSup {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} {ι : Type u_1} (G : ι → Subpresheaf F) (f : F ⟶ F') :
                  (⨆ (i : ι), G i).image f = ⨆ (i : ι), (G i).image f
                  source
                  theorem CategoryTheory.Subpresheaf.image_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') (g : F' ⟶ F'') :
                  G.image (CategoryStruct.comp f g) = (G.image f).image g
                  source
                  theorem CategoryTheory.Subpresheaf.range_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') (g : F' ⟶ F'') :
                  range (CategoryStruct.comp f g) = (range f).image g
                  source
                  def CategoryTheory.Subpresheaf.preimage {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :
                  Subpresheaf F'

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Subpresheaf.preimage_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) (n : Cᵒᵖ) :
                      (G.preimage p).obj n = p.app n ⁻¹' G.obj n
                      source
                      @[simp]
                      theorem CategoryTheory.Subpresheaf.preimage_id {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) :
                      G.preimage (CategoryStruct.id F) = G
                      source
                      theorem CategoryTheory.Subpresheaf.preimage_comp {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F'' ⟶ F') (g : F' ⟶ F) :
                      G.preimage (CategoryStruct.comp f g) = (G.preimage g).preimage f
                      source
                      theorem CategoryTheory.Subpresheaf.image_le_iff {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F ⟶ F') (G' : Subpresheaf F') :
                      G.image f ≤ G' ↔ G ≤ G'.preimage f
                      source
                      def CategoryTheory.Subpresheaf.fromPreimage {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :
                      (G.preimage p).toPresheaf ⟶ G.toPresheaf

                      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
                          source
                          theorem CategoryTheory.Subpresheaf.fromPreimage_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :
                          CategoryStruct.comp (G.fromPreimage p) G.ι = CategoryStruct.comp (G.preimage p).ι p
                          source
                          theorem CategoryTheory.Subpresheaf.fromPreimage_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) :
                          CategoryStruct.comp (G.fromPreimage p) (CategoryStruct.comp G.ι h) = CategoryStruct.comp (G.preimage p).ι (CategoryStruct.comp p h)
                          source
                          theorem CategoryTheory.Subpresheaf.preimage_eq_top_iff {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) :
                          G.preimage p = ⊤ ↔ range p ≤ G
                          source
                          @[simp]
                          theorem CategoryTheory.Subpresheaf.preimage_image_of_epi {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (p : F' ⟶ F) [hp : Epi p] :
                          (G.preimage p).image p = G