Commit 2023-06-01 14:13 950706ec

View on Github →

feat: port AlgebraicGeometry.StructureSheaf (#4522)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/StructureSheaf.lean

added def AlgebraicGeometry.PrimeSpectrum.Top

added def AlgebraicGeometry.Spec.structureSheaf

added theorem AlgebraicGeometry.StructureSheaf.IsFraction.eq_mk'

added def AlgebraicGeometry.StructureSheaf.IsFraction

added def AlgebraicGeometry.StructureSheaf.Localizations

added def AlgebraicGeometry.StructureSheaf.basicOpenIso

added theorem AlgebraicGeometry.StructureSheaf.coe_openToLocalization

added def AlgebraicGeometry.StructureSheaf.comap

added def AlgebraicGeometry.StructureSheaf.comapFun

added theorem AlgebraicGeometry.StructureSheaf.comapFunIsLocallyFraction

added theorem AlgebraicGeometry.StructureSheaf.comap_apply

added theorem AlgebraicGeometry.StructureSheaf.comap_comp

added theorem AlgebraicGeometry.StructureSheaf.comap_const

added theorem AlgebraicGeometry.StructureSheaf.comap_id'

added theorem AlgebraicGeometry.StructureSheaf.comap_id

added theorem AlgebraicGeometry.StructureSheaf.comap_id_eq_map

added def AlgebraicGeometry.StructureSheaf.const

added theorem AlgebraicGeometry.StructureSheaf.const_add

added theorem AlgebraicGeometry.StructureSheaf.const_apply'

added theorem AlgebraicGeometry.StructureSheaf.const_apply

added theorem AlgebraicGeometry.StructureSheaf.const_congr

added theorem AlgebraicGeometry.StructureSheaf.const_ext

added theorem AlgebraicGeometry.StructureSheaf.const_mul

added theorem AlgebraicGeometry.StructureSheaf.const_mul_cancel'

added theorem AlgebraicGeometry.StructureSheaf.const_mul_cancel

added theorem AlgebraicGeometry.StructureSheaf.const_mul_rev

added theorem AlgebraicGeometry.StructureSheaf.const_one

added theorem AlgebraicGeometry.StructureSheaf.const_self

added theorem AlgebraicGeometry.StructureSheaf.const_zero

added theorem AlgebraicGeometry.StructureSheaf.exists_const

added theorem AlgebraicGeometry.StructureSheaf.germ_comp_stalkToFiberRingHom

added theorem AlgebraicGeometry.StructureSheaf.germ_toOpen

added theorem AlgebraicGeometry.StructureSheaf.germ_to_top

added def AlgebraicGeometry.StructureSheaf.globalSectionsIso

added theorem AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom

added def AlgebraicGeometry.StructureSheaf.isFractionPrelocal

added def AlgebraicGeometry.StructureSheaf.isLocallyFraction

added theorem AlgebraicGeometry.StructureSheaf.isLocallyFraction_pred

added theorem AlgebraicGeometry.StructureSheaf.isUnit_toStalk

added theorem AlgebraicGeometry.StructureSheaf.isUnit_to_basicOpen_self

added def AlgebraicGeometry.StructureSheaf.localizationToStalk

added theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_mk'

added theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_of

added theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkSpecializes

added theorem AlgebraicGeometry.StructureSheaf.localizationToStalk_stalkToFiberRingHom

added theorem AlgebraicGeometry.StructureSheaf.localization_toBasicOpen

added theorem AlgebraicGeometry.StructureSheaf.locally_const_basicOpen

added theorem AlgebraicGeometry.StructureSheaf.normalize_finite_fraction_representation

added theorem AlgebraicGeometry.StructureSheaf.openAlgebra_map

added def AlgebraicGeometry.StructureSheaf.openToLocalization

added theorem AlgebraicGeometry.StructureSheaf.openToLocalization_apply

added theorem AlgebraicGeometry.StructureSheaf.res_apply

added theorem AlgebraicGeometry.StructureSheaf.res_const'

added theorem AlgebraicGeometry.StructureSheaf.res_const

added def AlgebraicGeometry.StructureSheaf.sectionsSubring

added theorem AlgebraicGeometry.StructureSheaf.stalkAlgebra_map

added def AlgebraicGeometry.StructureSheaf.stalkIso

added theorem AlgebraicGeometry.StructureSheaf.stalkSpecializes_stalk_to_fiber

added def AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom

added theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_germ'

added theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_germ

added theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_localizationToStalk

added theorem AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom_toStalk

added def AlgebraicGeometry.StructureSheaf.toBasicOpen

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_injective

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_mk'

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_surjective

added theorem AlgebraicGeometry.StructureSheaf.toBasicOpen_to_map

added def AlgebraicGeometry.StructureSheaf.toOpen

added theorem AlgebraicGeometry.StructureSheaf.toOpen_apply

added theorem AlgebraicGeometry.StructureSheaf.toOpen_comp_comap

added theorem AlgebraicGeometry.StructureSheaf.toOpen_eq_const

added theorem AlgebraicGeometry.StructureSheaf.toOpen_germ

added theorem AlgebraicGeometry.StructureSheaf.toOpen_res

added def AlgebraicGeometry.StructureSheaf.toStalk

added theorem AlgebraicGeometry.StructureSheaf.toStalk_comp_stalkToFiberRingHom

added theorem AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes

added theorem AlgebraicGeometry.StructureSheaf.to_global_factors

added def AlgebraicGeometry.structurePresheafCompForget

added def AlgebraicGeometry.structurePresheafInCommRing

added def AlgebraicGeometry.structureSheafInType