Documentation

Mathlib.CategoryTheory.Sites.CoverPreserving

Cover-preserving and continuous functors between sites. #

We define the notion of continuous functor between sites: these are functors G such that the precomposition with G.op preserves sheaves of types (and actually sheaves in any category).

In order to show that a functor is continuous, we define cover-preserving functors between sites as functors that push covering sieves to covering sieves. Then, a cover-preserving and compatible-preserving functor is continuous.

Main definitions #

Main results #

References #

A functor G : (C, J) ⥤ (D, K) between sites is cover-preserving if for all covering sieves R in C, R.functorPushforward G is a covering sieve in D.

Instances For

    A functor G : (C, J) ⥤ (D, K) between sites is called compatible preserving if for each compatible family of elements at C and valued in G.op ⋙ ℱ, and each commuting diagram f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂, x g₁ and x g₂ coincide when restricted via fᵢ. This is actually stronger than merely preserving compatible families because of the definition of functorPushforward used.

    Instances For
      theorem CategoryTheory.CompatiblePreserving.compatible {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} (self : CategoryTheory.CompatiblePreserving K G) (ℱ : CategoryTheory.SheafOfTypes K) {Z : C} {T : CategoryTheory.Presieve Z} {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp .val) T} :
      x.Compatible∀ {Y₁ Y₂ : C} {X : D} (f₁ : X G.obj Y₁) (f₂ : X G.obj Y₂) {g₁ : Y₁ Z} {g₂ : Y₂ Z} (hg₁ : T g₁) (hg₂ : T g₂), CategoryTheory.CategoryStruct.comp f₁ (G.map g₁) = CategoryTheory.CategoryStruct.comp f₂ (G.map g₂).val.map f₁.op (x g₁ hg₁) = .val.map f₂.op (x g₂ hg₂)
      theorem CategoryTheory.compatiblePreservingOfDownwardsClosed {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hF : {c : C} → {d : D} → (d F.obj c)(c' : C) × (F.obj c' d)) :

      A functor F is continuous if the precomposition with F.op sends sheaves of Type w to sheaves.

      Instances
        theorem CategoryTheory.Functor.isContinuous_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor D A} {F₁₂ : CategoryTheory.Functor C A} (e : F₁.comp F₂ F₁₂) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology A) [F₁.IsContinuous J K] [F₂.IsContinuous K L] :
        F₁₂.IsContinuous J L

        If F is cover-preserving and compatible-preserving, then F is a continuous functor.

        This result is basically .

        The induced functor Sheaf K A ⥤ Sheaf J A given by G.op ⋙ _ if G is a continuous functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For