Commit 2026-02-10 19:14 fd83ef42

View on Github →

chore(AlgebraicGeometry): refactor structureSheaf (#35090) We redefine structureSheaf to unify its construction with tilde.

Estimated changes

Modified Mathlib/Algebra/Category/Ring/FilteredColimits.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.Spec.algebraMap_stalkIso_inv

added theorem AlgebraicGeometry.Spec.germ_stalkMapIso_hom

added def AlgebraicGeometry.Spec.stalkIso

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

modified theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec

deleted theorem AlgebraicGeometry.toOpen_toSpecΓ_app

added theorem AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app'

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

deleted def ModuleCat.Tilde.const

deleted theorem ModuleCat.Tilde.const_apply

deleted theorem ModuleCat.Tilde.exists_const

deleted theorem ModuleCat.Tilde.germ_comp_stalkToFiberLinearMap

deleted def ModuleCat.Tilde.isFraction

deleted def ModuleCat.Tilde.isFractionPrelocal

deleted def ModuleCat.Tilde.isLocallyFraction

deleted theorem ModuleCat.Tilde.isLocallyFraction_pred

deleted theorem ModuleCat.Tilde.isUnit_toStalk

deleted theorem ModuleCat.Tilde.localizationToStalk_mk

deleted theorem ModuleCat.Tilde.res_const

deleted theorem ModuleCat.Tilde.sections_smul_localizations_def

deleted theorem ModuleCat.Tilde.stalkToFiberLinearMap_germ

deleted theorem ModuleCat.Tilde.stalkToFiberLinearMap_toStalk

deleted theorem ModuleCat.Tilde.toOpen_germ

deleted theorem ModuleCat.Tilde.toStalk_comp_stalkToFiberLinearMap

deleted def ModuleCat.tildeInType

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

modified theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv

Modified Mathlib/AlgebraicGeometry/Sites/Etale.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

modified def AlgebraicGeometry.Spec.locallyRingedSpaceObj

deleted theorem AlgebraicGeometry.localRingHom_comp_stalkIso_apply'

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

Modified Mathlib/AlgebraicGeometry/Stalk.lean

deleted theorem AlgebraicGeometry.Spec.algebraMap_stalkIso_inv

deleted theorem AlgebraicGeometry.Spec.germ_stalkMapIso_hom

deleted def AlgebraicGeometry.Spec.stalkIso

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

added def AlgebraicGeometry.Localizations.comapFun

added theorem AlgebraicGeometry.Localizations.comapFun_mk

deleted def AlgebraicGeometry.PrimeSpectrum.Top

modified def AlgebraicGeometry.Spec.structureSheaf

deleted theorem AlgebraicGeometry.StructureSheaf.IsFraction.eq_mk'

modified def AlgebraicGeometry.StructureSheaf.IsFraction

deleted def AlgebraicGeometry.StructureSheaf.Localizations

added theorem AlgebraicGeometry.StructureSheaf.algebraMap_self_map

deleted def AlgebraicGeometry.StructureSheaf.basicOpenIso

deleted theorem AlgebraicGeometry.StructureSheaf.coe_openToLocalization

deleted def AlgebraicGeometry.StructureSheaf.comap

deleted def AlgebraicGeometry.StructureSheaf.comapFun

deleted theorem AlgebraicGeometry.StructureSheaf.comapFunIsLocallyFraction

deleted theorem AlgebraicGeometry.StructureSheaf.comap_apply

deleted theorem AlgebraicGeometry.StructureSheaf.comap_basicOpen

deleted theorem AlgebraicGeometry.StructureSheaf.comap_comp

deleted theorem AlgebraicGeometry.StructureSheaf.comap_const

deleted theorem AlgebraicGeometry.StructureSheaf.comap_id'

deleted theorem AlgebraicGeometry.StructureSheaf.comap_id

deleted theorem AlgebraicGeometry.StructureSheaf.comap_id_eq_map

added def AlgebraicGeometry.StructureSheaf.commRingCatStalkEquivModuleStalk

modified def AlgebraicGeometry.StructureSheaf.const

modified theorem AlgebraicGeometry.StructureSheaf.const_add

added theorem AlgebraicGeometry.StructureSheaf.const_algebraMap

deleted theorem AlgebraicGeometry.StructureSheaf.const_apply'

modified theorem AlgebraicGeometry.StructureSheaf.const_apply

modified theorem AlgebraicGeometry.StructureSheaf.const_congr

added theorem AlgebraicGeometry.StructureSheaf.const_eq_const_of_smul_eq_smul

modified theorem AlgebraicGeometry.StructureSheaf.const_ext

modified theorem AlgebraicGeometry.StructureSheaf.const_mul

modified theorem AlgebraicGeometry.StructureSheaf.const_mul_rev

modified theorem AlgebraicGeometry.StructureSheaf.const_one

modified theorem AlgebraicGeometry.StructureSheaf.const_self

modified theorem AlgebraicGeometry.StructureSheaf.const_zero

modified theorem AlgebraicGeometry.StructureSheaf.exists_const

added theorem AlgebraicGeometry.StructureSheaf.exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const

deleted theorem AlgebraicGeometry.StructureSheaf.germ_comp_stalkToFiberRingHom

added theorem AlgebraicGeometry.StructureSheaf.germ_stalkToLocalizationₗ

deleted theorem AlgebraicGeometry.StructureSheaf.germ_toOpen

added def AlgebraicGeometry.StructureSheaf.germₗ

modified theorem AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom

modified def AlgebraicGeometry.StructureSheaf.isFractionPrelocal

modified def AlgebraicGeometry.StructureSheaf.isLocallyFraction

deleted theorem AlgebraicGeometry.StructureSheaf.isLocallyFraction_pred

added theorem AlgebraicGeometry.StructureSheaf.isUnit_basicOpen

added theorem AlgebraicGeometry.StructureSheaf.isUnit_basicOpen_end

modified theorem AlgebraicGeometry.StructureSheaf.isUnit_toStalk

added theorem AlgebraicGeometry.StructureSheaf.isUnit_toStalkₗ'

deleted theorem AlgebraicGeometry.StructureSheaf.isUnit_to_basicOpen_self

deleted def AlgebraicGeometry.StructureSheaf.localizationToStalk

deleted theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_mk'

deleted theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_of

deleted theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkSpecializes

deleted theorem AlgebraicGeometry.StructureSheaf.localization_toBasicOpen

added def AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ

added theorem AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ_mk

deleted theorem AlgebraicGeometry.StructureSheaf.locally_const_basicOpen

added def AlgebraicGeometry.StructureSheaf.modulePresheafStalkIso

deleted theorem AlgebraicGeometry.StructureSheaf.normalize_finite_fraction_representation

deleted theorem AlgebraicGeometry.StructureSheaf.openAlgebra_map

deleted def AlgebraicGeometry.StructureSheaf.openToLocalization

deleted theorem AlgebraicGeometry.StructureSheaf.openToLocalization_apply

added def AlgebraicGeometry.StructureSheaf.openToLocalizationₗ

deleted theorem AlgebraicGeometry.StructureSheaf.res_const'

modified theorem AlgebraicGeometry.StructureSheaf.res_const

added def AlgebraicGeometry.StructureSheaf.sectionsSubalgebra

added def AlgebraicGeometry.StructureSheaf.sectionsSubalgebraSubmodule

added def AlgebraicGeometry.StructureSheaf.sectionsSubmodule

deleted def AlgebraicGeometry.StructureSheaf.sectionsSubring

added theorem AlgebraicGeometry.StructureSheaf.smul_const

deleted def AlgebraicGeometry.StructureSheaf.stalkIso

added def AlgebraicGeometry.StructureSheaf.stalkIsoₗ

deleted theorem AlgebraicGeometry.StructureSheaf.stalkSpecializes_stalk_to_fiber

deleted def AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom

deleted theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_germ

deleted theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_toStalk

added def AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ

deleted def AlgebraicGeometry.StructureSheaf.toBasicOpen

deleted theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_injective

deleted theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_mk'

deleted theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_surjective

deleted theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_to_map

added def AlgebraicGeometry.StructureSheaf.toBasicOpenₗ

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_injective

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_mk

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpenₗ_surjective

deleted theorem AlgebraicGeometry.StructureSheaf.toOpen_apply

deleted theorem AlgebraicGeometry.StructureSheaf.toOpen_comp_comap

deleted theorem AlgebraicGeometry.StructureSheaf.toOpen_eq_const

deleted theorem AlgebraicGeometry.StructureSheaf.toOpen_germ

deleted theorem AlgebraicGeometry.StructureSheaf.toOpen_res

deleted theorem AlgebraicGeometry.StructureSheaf.toOpen_Γgerm_apply

added def AlgebraicGeometry.StructureSheaf.toOpenₗ

added theorem AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const

added theorem AlgebraicGeometry.StructureSheaf.toOpenₗ_germ

deleted def AlgebraicGeometry.StructureSheaf.toStalk

deleted theorem AlgebraicGeometry.StructureSheaf.toStalk_comp_stalkToFiberRingHom

added theorem AlgebraicGeometry.StructureSheaf.toStalk_smul

added def AlgebraicGeometry.StructureSheaf.toStalkₗ'

added theorem AlgebraicGeometry.StructureSheaf.toStalkₗ'_stalkToFiberRingHom

added def AlgebraicGeometry.StructureSheaf.toStalkₗ

deleted theorem AlgebraicGeometry.StructureSheaf.to_global_factors

added def AlgebraicGeometry.comap

added def AlgebraicGeometry.comapFun

added theorem AlgebraicGeometry.comap_apply

added theorem AlgebraicGeometry.comap_basicOpen

added theorem AlgebraicGeometry.comap_comp

added theorem AlgebraicGeometry.comap_const

added theorem AlgebraicGeometry.comap_id'

added theorem AlgebraicGeometry.comap_id

added theorem AlgebraicGeometry.comap_id_eq_map

added def AlgebraicGeometry.comapₗ

added theorem AlgebraicGeometry.comapₗ_const

added theorem AlgebraicGeometry.comapₗ_eq_localRingHom

added theorem AlgebraicGeometry.isLocallyFraction_comapFun

added def AlgebraicGeometry.moduleStructurePresheaf

deleted def AlgebraicGeometry.structurePresheafInCommRing

added def AlgebraicGeometry.structurePresheafInCommRingCat

added def AlgebraicGeometry.structurePresheafInModuleCat

added theorem AlgebraicGeometry.structureSheafInType.add_apply

added theorem AlgebraicGeometry.structureSheafInType.mul_apply

added theorem AlgebraicGeometry.structureSheafInType.smul_apply

added theorem AlgebraicGeometry.toOpen_comp_comap

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

added theorem PrimeSpectrum.le_basicOpen_pow