Documentation

Mathlib.CategoryTheory.Sites.Continuous

Continuous functors between sites. #

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

Main definitions #

Main result #

References #

@[simp]
theorem CategoryTheory.PreOneHypercover.map_p₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D) :
∀ (x x_1 : E.I₀) (j : E.I₁ x x_1), (E.map F).p₁ j = F.map (E.p₁ j)
@[simp]
theorem CategoryTheory.PreOneHypercover.map_I₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D) (i₁ : E.I₀) (i₂ : E.I₀) :
(E.map F).I₁ i₁ i₂ = E.I₁ i₁ i₂
@[simp]
theorem CategoryTheory.PreOneHypercover.map_Y {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D) :
∀ (x x_1 : E.I₀) (j : E.I₁ x x_1), (E.map F).Y j = F.obj (E.Y j)
@[simp]
theorem CategoryTheory.PreOneHypercover.map_p₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D) :
∀ (x x_1 : E.I₀) (j : E.I₁ x x_1), (E.map F).p₂ j = F.map (E.p₂ j)
@[simp]
@[simp]

The image of a 1-pre-hypercover by a functor.

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

    If F : C ⥤ D, P : Dᵒᵖ ⥤ A and E is a 1-pre-hypercover of an object of X, then (E.map F).multifork P is a limit iff E.multifork (F.op ⋙ P) is a limit.

    Equations
    Instances For

      A 1-hypercover in C is preserved by a functor F : C ⥤ D if the mapped 1-pre-hypercover in D is a 1-hypercover for the given topology on D.

      Instances
        theorem CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [self : E.IsPreservedBy F K] (i₁ : E.I₀) (i₂ : E.I₀) ⦃W : D (p₁ : W F.obj (E.X i₁)) (p₂ : W F.obj (E.X i₂)) (w : CategoryTheory.CategoryStruct.comp p₁ (F.map (E.f i₁)) = CategoryTheory.CategoryStruct.comp p₂ (F.map (E.f i₂))) :
        (E.map F).sieve₁ p₁ p₂ K W
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.OneHypercover.map_toPreOneHypercover {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {X : C} (E : J.OneHypercover X) (F : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [E.IsPreservedBy F K] :
        (E.map F K).toPreOneHypercover = E.map F

        Given a 1-hypercover E : J.OneHypercover X of an object of C, a functor F : C ⥤ D such that E.IsPreversedBy F K for a Grothendieck topology K on D, this is the image of E by F, as a 1-hypercover of F.obj X for K.

        Equations
        • E.map F K = { toPreOneHypercover := E.map F, mem₀ := , mem₁ := }
        Instances For
          @[reducible, inline]

          The condition that a functor F : C ⥤ D sends 1-hypercovers for J : GrothendieckTopology C to 1-hypercovers for K : GrothendieckTopology D.

          Equations
          • F.PreservesOneHypercovers J K = ∀ {X : C} (E : J.OneHypercover X), E.IsPreservedBy F K
          Instances For

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

            Instances
              theorem CategoryTheory.Functor.isContinuous_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor D E} {F₁₂ : CategoryTheory.Functor C E} (e : F₁.comp F₂ F₁₂) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology E) [F₁.IsContinuous J K] [F₂.IsContinuous K L] :
              F₁₂.IsContinuous J L
              @[simp]
              theorem CategoryTheory.Functor.sheafPushforwardContinuous_map_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (A : Type u) [CategoryTheory.Category.{t, u} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K] :
              ∀ {X Y : CategoryTheory.Sheaf K A} (f : X Y) (X_1 : Cᵒᵖ), ((F.sheafPushforwardContinuous A J K).map f).val.app X_1 = f.val.app (Opposite.op (F.obj (Opposite.unop X_1)))
              @[simp]
              theorem CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (A : Type u) [CategoryTheory.Category.{t, u} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K] (ℱ : CategoryTheory.Sheaf K A) (X : Cᵒᵖ) :
              ((F.sheafPushforwardContinuous A J K).obj ).val.obj X = .val.obj (Opposite.op (F.obj (Opposite.unop X)))
              @[simp]
              theorem CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (A : Type u) [CategoryTheory.Category.{t, u} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K] (ℱ : CategoryTheory.Sheaf K A) :
              ∀ {X Y : Cᵒᵖ} (f : X Y), ((F.sheafPushforwardContinuous A J K).obj ).val.map f = .val.map (F.map f.unop).op

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

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

                The functor F.sheafPushforwardContinuous A J K : Sheaf K A ⥤ Sheaf J A is induced by the precomposition with F.op.

                Equations
                Instances For