The standard conservative family of points for the site attached to a topological space

If X is a topological space, any x : X defines a point of the site attached to X.

TODO

• Redefine the stalks functors in Mathlib/Topology/Sheaves/Stalks.lean using GrothendieckTopology.Point.presheafFiber.

def Opens.pointGrothendieckTopology {X : Type u} [TopologicalSpace X] (x : X) : (grothendieckTopology X).Point

Given a topological space X and x : X, this is the point of the site (Opens X, Opens.grothendieckTopology X) corresponding to x.

Equations

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

def Opens.pointsGrothendieckTopology (X : Type u) [TopologicalSpace X] : CategoryTheory.ObjectProperty (grothendieckTopology X).Point

When X is a topological space, this is the obvious conservative family of points on the site (Opens X, Opens.grothendieckTopology X).

Equations

• Opens.pointsGrothendieckTopology X = CategoryTheory.ObjectProperty.ofObj Opens.pointGrothendieckTopology

@[implicit_reducible]

instance Opens.instSmallPointOpensGrothendieckTopologyPointsGrothendieckTopology (X : Type u_1) [TopologicalSpace X] : CategoryTheory.ObjectProperty.Small.{u_1, u_1, u_1 + 1} (pointsGrothendieckTopology X)

Equations

• ⋯ = ⋯

theorem Opens.isConservativeFamilyOfPoints_pointsGrothendieckTopology (X : Type u) [TopologicalSpace X] : (pointsGrothendieckTopology X).IsConservativeFamilyOfPoints

instance Opens.instHasEnoughPointsOpensGrothendieckTopology {X : Type u} [TopologicalSpace X] : (grothendieckTopology X).HasEnoughPoints

instance Opens.instSubsingletonObjOpensFiber {X : Type u} [TopologicalSpace X] (U : TopologicalSpace.Opens X) (Φ : (grothendieckTopology X).Point) : Subsingleton (Φ.fiber.obj U)

instance Opens.instIsThinPointOpensGrothendieckTopology {X : Type u} [TopologicalSpace X] : Quiver.IsThin (grothendieckTopology X).Point

def Opens.pointGrothendieckTopologyHomEquiv {X : Type u} [TopologicalSpace X] {x y : X} : (pointGrothendieckTopology x ⟶ pointGrothendieckTopology y) ≃ x ⤳ y

A point x of a topological space X specializes to y if and only iff there is a (unique) morphism between the corresponding points of the site (Opens X, grothendieckTopology X).

Equations

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