Commit 2023-06-29 07:18 a5ab9709

View on Github →

feat: port AlgebraicGeometry.AffineScheme (#5394)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/AffineScheme.lean

added def AlgebraicGeometry.AffineScheme.Spec

added def AlgebraicGeometry.AffineScheme.equivCommRingCat

added def AlgebraicGeometry.AffineScheme.forgetToScheme

added def AlgebraicGeometry.AffineScheme.mk

added def AlgebraicGeometry.AffineScheme.of

added def AlgebraicGeometry.AffineScheme.ofHom

added def AlgebraicGeometry.AffineScheme.Γ

added def AlgebraicGeometry.AffineScheme

added theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec

added theorem AlgebraicGeometry.IsAffineOpen.basicOpenIsAffine

added theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app

added theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff

added theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le

added def AlgebraicGeometry.IsAffineOpen.fromSpec

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_range

added theorem AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion

added theorem AlgebraicGeometry.IsAffineOpen.isCompact

added theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk'

added theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk

added theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux'

added theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux

added theorem AlgebraicGeometry.IsAffineOpen.mapRestrictBasicOpen

added theorem AlgebraicGeometry.IsAffineOpen.opens_map_fromSpec_basicOpen

added theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff

added def AlgebraicGeometry.IsAffineOpen

added theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom

added def AlgebraicGeometry.Scheme.affineBasicOpen

added def AlgebraicGeometry.Scheme.affineOpens

added def AlgebraicGeometry.Scheme.isoSpec

added theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine

added def AlgebraicGeometry.basicOpenSectionsToAffine

added theorem AlgebraicGeometry.basicOpen_basicOpen_is_basicOpen

added theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter

added theorem AlgebraicGeometry.isAffineOfIso

added theorem AlgebraicGeometry.isAffineOpen_iff_of_isOpenImmersion

added theorem AlgebraicGeometry.isBasis_affine_open

added theorem AlgebraicGeometry.isBasis_basicOpen

added theorem AlgebraicGeometry.isLocalization_basicOpen

added theorem AlgebraicGeometry.isLocalization_of_eq_basicOpen

added theorem AlgebraicGeometry.mem_Spec_essImage

added theorem AlgebraicGeometry.of_affine_open_cover

added theorem AlgebraicGeometry.rangeIsAffineOpenOfOpenImmersion

added theorem AlgebraicGeometry.topIsAffineOpen

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op

Modified Mathlib/CategoryTheory/EssentialImage.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean