Structures · Category theory
CategoryTheory.GrothendieckTopology.IsLocalSite
A local site is a site that has a terminal object with only a single covering sieve.
- Defined in
- Mathlib.CategoryTheory.Sites.LocalSite
- Shape
- One type argument · adds eq_top_of_mem
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- CategoryTheory.GrothendieckTopology.IsLocalSite.point
- CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso
- CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulConstantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom
- CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality
- CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom_assoc
- CategoryTheory.GrothendieckTopology.IsLocalSite.eq_top_of_mem
- CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.ΓCoconstantSheafAdj
- CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafConstantSheafOfHasColimitsOfSizeOfHasProducts
- CategoryTheory.GrothendieckTopology.IsLocalSite.fullyFaithfulCoconstantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.Γ_isLeftAdjoint
- CategoryTheory.GrothendieckTopology.IsLocalSite.pointSheafFiberIso
- CategoryTheory.GrothendieckTopology.IsLocalSite.instIsRightAdjointSheafCoconstantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.constantΓCoconstantTriple
- CategoryTheory.GrothendieckTopology.IsLocalSite.faithful_constantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.instFaithfulSheafCoconstantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.full_constantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.toHasLimitsOfShape
- CategoryTheory.GrothendieckTopology.IsLocalSite.from_terminal_mem_of_mem
- CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafCoconstantSheaf
- CategoryTheory.GrothendieckTopology.IsLocalSite.instIsLeftAdjointSheafΓOfHasColimitsOfSizeOfHasProducts
- CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberNatIso
- CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafConstantSheafOfHasColimitsOfSizeOfHasProducts
- CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso_naturality_assoc
- CategoryTheory.GrothendieckTopology.IsLocalSite.point.congr_simp
- CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheafΓNatIsoId