Commit 2023-07-07 04:14 be46ce4b

View on Github →

feat: port AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (#5224)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

added theorem AlgebraicGeometry.HomogeneousLocalization.mem_basicOpen

added def AlgebraicGeometry.Proj.stalkIso'

added def AlgebraicGeometry.Proj.toLocallyRingedSpace

added def AlgebraicGeometry.Proj.toSheafedSpace

added def AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFraction

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.addMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mulMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.negMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.oneMem'

added theorem AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zeroMem'

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isFractionPrelocal

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.sectionsSubring

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafCompForget

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing

added def AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structureSheafInType

added theorem AlgebraicGeometry.germ_comp_stalkToFiberRingHom

added def AlgebraicGeometry.homogeneousLocalizationToStalk

added def AlgebraicGeometry.openToLocalization

added theorem AlgebraicGeometry.res_apply

added def AlgebraicGeometry.sectionInBasicOpen

added def AlgebraicGeometry.stalkToFiberRingHom

added theorem AlgebraicGeometry.stalkToFiberRingHom_germ'

added theorem AlgebraicGeometry.stalkToFiberRingHom_germ