Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.PresheafedSpace.Hom

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AlgebraicGeometry.PresheafedSpace C → AlgebraicGeometry.PresheafedSpace C → Type (max u_2 v_1)

A morphism between presheafed spaces X and Y consists of a continuous map f between the underlying topological spaces, and a (note: contravariant!) map from the presheaf on Y to the pushforward of the presheaf on X via f.

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace

Cited by

32 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category