Commit 2023-05-21 15:13 6d77e3b4

View on Github →

feat: port AlgebraicGeometry.PresheafedSpace (#4093)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/PresheafedSpace.lean

added theorem AlgebraicGeometry.PresheafedSpace.Hom.ext

added structure AlgebraicGeometry.PresheafedSpace.Hom

added def AlgebraicGeometry.PresheafedSpace.comp

added theorem AlgebraicGeometry.PresheafedSpace.comp_base

added theorem AlgebraicGeometry.PresheafedSpace.comp_c

added theorem AlgebraicGeometry.PresheafedSpace.comp_c_app

added theorem AlgebraicGeometry.PresheafedSpace.congr_app

added def AlgebraicGeometry.PresheafedSpace.const

added theorem AlgebraicGeometry.PresheafedSpace.ext

added def AlgebraicGeometry.PresheafedSpace.forget

added theorem AlgebraicGeometry.PresheafedSpace.hext

added def AlgebraicGeometry.PresheafedSpace.id

added theorem AlgebraicGeometry.PresheafedSpace.id_base

added theorem AlgebraicGeometry.PresheafedSpace.id_c

added theorem AlgebraicGeometry.PresheafedSpace.id_c_app

added theorem AlgebraicGeometry.PresheafedSpace.isIso_of_components

added def AlgebraicGeometry.PresheafedSpace.isoOfComponents

added theorem AlgebraicGeometry.PresheafedSpace.mk_coe

added def AlgebraicGeometry.PresheafedSpace.ofRestrict

added theorem AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c

added def AlgebraicGeometry.PresheafedSpace.restrict

added def AlgebraicGeometry.PresheafedSpace.restrictTopIso

added theorem AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf

added def AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso

added def AlgebraicGeometry.PresheafedSpace.toRestrictTop

added def AlgebraicGeometry.PresheafedSpace.Γ

added theorem AlgebraicGeometry.PresheafedSpace.Γ_map_op

added theorem AlgebraicGeometry.PresheafedSpace.Γ_obj_op

added structure AlgebraicGeometry.PresheafedSpace

added def CategoryTheory.Functor.mapPresheaf

added theorem CategoryTheory.Functor.mapPresheaf_map_c

added theorem CategoryTheory.Functor.mapPresheaf_map_f

added theorem CategoryTheory.Functor.mapPresheaf_obj_X

added theorem CategoryTheory.Functor.mapPresheaf_obj_presheaf

added def CategoryTheory.NatTrans.onPresheaf