Induced topologies

In this file we study various topologies induced by a functor. Let F : C ⥤ D be a functor, J a Grothendieck topology on C and K a Grothendieck topology on D.

• CategoryTheory.Functor.inducedTopology F K: The finest topology on C making F continuous.
• CategoryTheory.Functor.restrictedTopology F K: The coarsest topology on C containing all sieves whose image generate a covering sieve of K. In general, this does not make F cover preserving.

TODOs

• Define the finest topology on the codomain making a functor cocontinuous (@chrisflav).

References

• SGA4, III, 3

def CategoryTheory.Functor.inducedTopology {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (K : GrothendieckTopology D) : GrothendieckTopology C

The induced topology by a topology on D along a functor F : C ⥤ D is the finest topology on C making F continuous. SGA4, III, 3.1

Equations

• F.inducedTopology K = CategoryTheory.Sheaf.finestTopology (Set.range fun (G : CategoryTheory.Sheaf K (Type (max ?u.2 ?u.4 ?u.1 ?u.3))) => F.op.comp G.obj)

instance CategoryTheory.Functor.instIsContinuousInducedTopology {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {K : GrothendieckTopology D} : F.IsContinuous (F.inducedTopology K) K

@[simp]

theorem CategoryTheory.Functor.le_inducedTopology_iff {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {K : GrothendieckTopology D} {J : GrothendieckTopology C} : J ≤ F.inducedTopology K ↔ F.IsContinuous J K

theorem CategoryTheory.Functor.mem_inducedTopology_iff {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {K : GrothendieckTopology D} [LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C] (X : C) (S : Sieve X) (G : Functor (Functor Cᵒᵖ (Type (max u₁ v₁ u₂ v₂))) (Functor Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)))) (adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op) : S ∈ (F.inducedTopology K) X ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)

SGA4, III, Proposition 3.2

theorem CategoryTheory.Functor.induced_induced_le {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} (G : Functor D E) (J : GrothendieckTopology E) : F.inducedTopology (G.inducedTopology J) ≤ (F.comp G).inducedTopology J

theorem CategoryTheory.Functor.inducedTopology_eq_of_iso {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {K : GrothendieckTopology D} {F G : Functor C D} (e : F ≅ G) : F.inducedTopology K = G.inducedTopology K

def CategoryTheory.Functor.restrictedTopology {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) (K : GrothendieckTopology D) : GrothendieckTopology C

The coarsest topology containing all sieves whose image under F generates a covering sieve of K.

Equations

• F.restrictedTopology K = (CategoryTheory.Precoverage.comap F K.toPrecoverage).toGrothendieck

theorem CategoryTheory.Functor.mem_restrictedTopology_of_functorPushforward_mem {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {K : GrothendieckTopology D} {X : C} {S : Sieve X} (hS : Sieve.functorPushforward F S ∈ K (F.obj X)) : S ∈ (F.restrictedTopology K) X

theorem CategoryTheory.Functor.inducedTopology_le_restrictedTopology {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {K : GrothendieckTopology D} : F.inducedTopology K ≤ F.restrictedTopology K

theorem CategoryTheory.Functor.restrictedTopology_eq_inducedTopology {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {K : GrothendieckTopology D} [F.IsContinuous (F.restrictedTopology K) K] : F.restrictedTopology K = F.inducedTopology K

If F is continuous with the restricted topology, the restricted topology agrees with the induced topology. This holds for example if G is locally faithful, locally full and cover dense.

theorem CategoryTheory.Functor.restrictedTopology_eq_inducedTopology_of_isContinuous {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} {J : GrothendieckTopology C} {K : GrothendieckTopology D} [F.IsContinuous J K] (h : F.restrictedTopology K = J) : F.inducedTopology K = J

Variant of Functor.restrictedTopology_eq_inducedTopology that is sometimes easier to use.

theorem CategoryTheory.Precoverage.toGrothendieck_comap_le_restrictedTopology {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {F : Functor C D} (K : Precoverage D) : (comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck