Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.SheafedSpace

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max u (u_1 + 1)) v)

A SheafedSpace C is a topological space equipped with a sheaf of Cs.

Defined in

Mathlib.Geometry.RingedSpace.SheafedSpace

Cited by

142 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category