Commit 2024-10-10 07:55 7f9e70cc

View on Github →

refactor(Topology/Sheaves): Unbundle germ. (#15314)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

modified theorem AlgebraicGeometry.germ_injective_of_isIntegral

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

modified theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

deleted theorem AlgebraicGeometry.Proj.stalkIso'_germ'

modified theorem AlgebraicGeometry.Proj.stalkIso'_germ

modified theorem AlgebraicGeometry.germ_comp_stalkToFiberRingHom

deleted theorem AlgebraicGeometry.stalkToFiberRingHom_germ'

modified theorem AlgebraicGeometry.stalkToFiberRingHom_germ

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

modified theorem AlgebraicGeometry.Scheme.germ_residue

Modified Mathlib/AlgebraicGeometry/Restrict.lean

deleted theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom'

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.mem_basicOpen''

added theorem AlgebraicGeometry.Scheme.mem_basicOpen'

modified theorem AlgebraicGeometry.Scheme.mem_basicOpen

deleted theorem AlgebraicGeometry.Scheme.mem_basicOpen_top'

deleted theorem AlgebraicGeometry.Scheme.stalkMap_germ'

deleted theorem AlgebraicGeometry.Scheme.stalkMap_germ'_apply

modified theorem AlgebraicGeometry.Scheme.stalkMap_germ

modified theorem AlgebraicGeometry.Scheme.stalkMap_germ_apply

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/Stalk.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

modified theorem AlgebraicGeometry.StructureSheaf.germ_comp_stalkToFiberRingHom

modified theorem AlgebraicGeometry.StructureSheaf.germ_toOpen

deleted theorem AlgebraicGeometry.StructureSheaf.germ_to_top

deleted theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_germ'

modified theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_germ

modified theorem AlgebraicGeometry.StructureSheaf.toOpen_germ

added theorem AlgebraicGeometry.StructureSheaf.toOpen_Γgerm_apply

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

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

modified theorem smoothSheaf.eval_germ

modified theorem smoothSheafCommRing.evalHom_germ

modified theorem smoothSheafCommRing.eval_germ

Modified Mathlib/Geometry/RingedSpace/Basic.lean

modified theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ

added theorem AlgebraicGeometry.RingedSpace.mem_basicOpen'

modified theorem AlgebraicGeometry.RingedSpace.mem_basicOpen

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

deleted theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ'

deleted theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ'_apply

modified theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ

modified theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

Modified Mathlib/Geometry/RingedSpace/Stalks.lean

deleted theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ'

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

modified theorem TopCat.stalkToFiber_germ

Modified Mathlib/Topology/Sheaves/LocallySurjective.lean

Modified Mathlib/Topology/Sheaves/Operations.lean

Modified Mathlib/Topology/Sheaves/Sheafify.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

added def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk

added theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper

added theorem StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk

added theorem StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk

added theorem germ_skyscraperPresheafStalkOfSpecializes_hom

Modified Mathlib/Topology/Sheaves/Stalks.lean

modified def TopCat.Presheaf.germ

modified def TopCat.Presheaf.germToPullbackStalk

added theorem TopCat.Presheaf.germ_res'

modified theorem TopCat.Presheaf.germ_res

added theorem TopCat.Presheaf.germ_res_apply'

modified theorem TopCat.Presheaf.germ_res_apply

deleted theorem TopCat.Presheaf.germ_stalkSpecializes'

modified theorem TopCat.Presheaf.germ_stalkSpecializes

modified theorem TopCat.Presheaf.map_germ_eq_Γgerm

modified theorem TopCat.Presheaf.stalkFunctor_map_germ

added theorem TopCat.Presheaf.stalkFunctor_map_germ_apply'

added theorem TopCat.Presheaf.stalkFunctor_map_germ_apply

modified theorem TopCat.Presheaf.Γgerm_res_apply