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 #
Functor.IsContinuous
: a functor between sites is continuous if the precomposition with this functor preserves sheaves with values in the categoryType t
for a certain auxiliary universet
.Functor.sheafPushforwardContinuous
: the induced functorSheaf K A ⥤ Sheaf J A
for a continuous functorG : (C, J) ⥤ (D, K)
. In case this is part of a morphism of sites, this would be understood as the pushforward functor even though it goes in the opposite direction as the functorG
. (Here, the auxiliary universet
in the assumption thatG
is continuous is the one such that morphisms in the categoryA
are inType t
.)Functor.PreservesOneHypercovers
: a type-class expressing that a functor preserves 1-hypercovers of a certain size
Main result #
Functor.isContinuous_of_preservesOneHypercovers
: if the topology onC
is generated by 1-hypercovers of sizew
and thatF : C ⥤ D
preserves 1-hypercovers of sizew
, thenF
is continuous (for any auxiliary universe parametert
). This is an instance forw = max u₁ v₁
whenC : Type u₁
and[Category.{v₁} C]
References #
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
- E.isLimitMapMultiforkEquiv F P = Equiv.refl (CategoryTheory.Limits.IsLimit ((E.map F).multifork P))
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
.
- mem₀ : (E.map F).sieve₀ ∈ K (F.obj X)
- mem₁ (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
Instances
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
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.
- op_comp_isSheaf_of_types (G : CategoryTheory.Sheaf K (Type t)) : CategoryTheory.Presieve.IsSheaf J (F.op.comp G.val)
Instances
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
- F.sheafPushforwardContinuousCompSheafToPresheafIso A J K = CategoryTheory.Iso.refl ((F.sheafPushforwardContinuous A J K).comp (CategoryTheory.sheafToPresheaf J A))