Commit 2026-04-01 16:05 74c1ec45

View on Github →

feat(Geometry/Manifold): a smooth map induces a morphism of locally ringed spaces (#35661)

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

added theorem ContMDiff.subtypeVal_comp_iff

added theorem ContMDiffAt.subtypeVal_comp_iff

added theorem ContMDiffWithinAt.subtypeVal_comp_iff

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

added theorem ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

added def ChartedSpace.locallyRingedSpace

added def ChartedSpace.locallyRingedSpaceMap

added def ChartedSpace.locallyRingedSpaceMapAux

added theorem ChartedSpace.locallyRingedSpace_comp

added theorem ChartedSpace.locallyRingedSpace_id

added def ChartedSpace.restrictLocallyRingedSpaceIso

added theorem ChartedSpace.stalkMap_locallyRingedSpaceMapAux

added theorem ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom

deleted def IsManifold.locallyRingedSpace

Modified Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

added def ContMDiff.smoothSheafCommRingHom

added def ContMDiff.smoothSheafHom