Commit 2023-06-14 02:02 9089d3e6

View on Github →

feat: port AlgebraicGeometry.Spec (#4599)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Spec.lean

added theorem AlgebraicGeometry.Spec.basicOpen_hom_ext

added def AlgebraicGeometry.Spec.locallyRingedSpaceMap

added theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp

added theorem AlgebraicGeometry.Spec.locallyRingedSpaceMap_id

added def AlgebraicGeometry.Spec.locallyRingedSpaceObj

added def AlgebraicGeometry.Spec.sheafedSpaceMap

added theorem AlgebraicGeometry.Spec.sheafedSpaceMap_comp

added theorem AlgebraicGeometry.Spec.sheafedSpaceMap_id

added def AlgebraicGeometry.Spec.sheafedSpaceObj

added def AlgebraicGeometry.Spec.toLocallyRingedSpace

added def AlgebraicGeometry.Spec.toPresheafedSpace

added theorem AlgebraicGeometry.Spec.toPresheafedSpace_map

added theorem AlgebraicGeometry.Spec.toPresheafedSpace_map_op

added theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj

added theorem AlgebraicGeometry.Spec.toPresheafedSpace_obj_op

added def AlgebraicGeometry.Spec.toSheafedSpace

added def AlgebraicGeometry.Spec.toTop

added def AlgebraicGeometry.Spec.topMap

added theorem AlgebraicGeometry.Spec.topMap_comp

added theorem AlgebraicGeometry.Spec.topMap_id

added def AlgebraicGeometry.Spec.topObj

added theorem AlgebraicGeometry.Spec_map_localization_isIso

added theorem AlgebraicGeometry.Spec_Γ_naturality

added def AlgebraicGeometry.SpecΓIdentity

added theorem AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk

added theorem AlgebraicGeometry.StructureSheaf.is_localized_module_toPushforwardStalkAlgHom_aux

added def AlgebraicGeometry.StructureSheaf.toPushforwardStalk

added def AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom

added theorem AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp

added theorem AlgebraicGeometry.localRingHom_comp_stalkIso

added theorem AlgebraicGeometry.stalkMap_toStalk

added def AlgebraicGeometry.toSpecΓ