Commit 2024-07-23 21:13 4261f994

View on Github →

refactor(AlgebraicGeometry): Introduce Scheme.Opens. (#15001) Introduced Scheme.Opens as the type of open sets of a scheme. Provided instance : CoeOut X.Opens Scheme to replace the notation X ∣_ᵤ U, and renamed Scheme.ιOpens to Scheme.Opens.ι to enable dot notation.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map

modified theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le

modified theorem AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen

modified theorem AlgebraicGeometry.IsAffineOpen.map_fromSpec

modified theorem AlgebraicGeometry.IsAffineOpen.preimage_of_isIso

deleted theorem AlgebraicGeometry.IsAffineOpen.ιOpens_basicOpen_preimage

added theorem AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage

modified def AlgebraicGeometry.IsAffineOpen

modified def AlgebraicGeometry.Scheme.affineOpens

modified def AlgebraicGeometry.affineOpensRestrict

modified theorem AlgebraicGeometry.iSup_affineOpens_eq_top

modified theorem AlgebraicGeometry.isAffineOpen_top

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

modified theorem AlgebraicGeometry.Scheme.OpenCover.ext_elem

modified theorem AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover

deleted def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop

modified theorem AlgebraicGeometry.Scheme.zero_of_zero_cover

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

modified theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint

modified theorem AlgebraicGeometry.Scheme.germToFunctionField_injective

modified theorem AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen

modified theorem AlgebraicGeometry.germ_injective_of_isIntegral

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

modified theorem AlgebraicGeometry.ΓSpecIso_obj_hom

Modified Mathlib/AlgebraicGeometry/Limits.lean

modified theorem AlgebraicGeometry.isAffineOpen_bot

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

modified theorem AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top

modified theorem AlgebraicGeometry.IsLocalAtSource.of_iSup_eq_top

modified theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top

modified theorem AlgebraicGeometry.IsLocalAtTarget.of_iSup_eq_top

modified theorem AlgebraicGeometry.IsLocalAtTarget.restrict

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

modified theorem AlgebraicGeometry.Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact

modified theorem AlgebraicGeometry.compact_open_induction_on

modified theorem AlgebraicGeometry.isCompact_basicOpen

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

modified theorem AlgebraicGeometry.IsAffineOpen.isQuasiSeparated

modified theorem AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen

modified theorem AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated

modified theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Noetherian.lean

modified theorem AlgebraicGeometry.noetherianSpace_of_isAffineOpen

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

modified theorem AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv

modified def AlgebraicGeometry.IsOpenImmersion.ΓIso

modified theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_hom_map

modified theorem AlgebraicGeometry.IsOpenImmersion.ΓIso_inv

modified theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_appLE

modified theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality

modified theorem AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv

modified theorem AlgebraicGeometry.Scheme.Hom.image_le_image_of_le

modified theorem AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter

modified theorem AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE

modified def AlgebraicGeometry.Scheme.Hom.opensRange

modified theorem AlgebraicGeometry.Scheme.Hom.preimage_image_eq

modified theorem AlgebraicGeometry.Scheme.image_basicOpen

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

modified theorem AlgebraicGeometry.basicOpen_eq_bot_iff

modified theorem AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot

modified theorem AlgebraicGeometry.map_injective_of_isIntegral

modified theorem AlgebraicGeometry.reduce_to_affine_global

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Opens.eq_presheaf_map_eqToHom

added theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom

added theorem AlgebraicGeometry.Scheme.Opens.nonempty_iff

added theorem AlgebraicGeometry.Scheme.Opens.opensRange_ι

added theorem AlgebraicGeometry.Scheme.Opens.range_ι

added def AlgebraicGeometry.Scheme.Opens.stalkIso

added def AlgebraicGeometry.Scheme.Opens.toScheme

added theorem AlgebraicGeometry.Scheme.Opens.toScheme_carrier

added theorem AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map

added theorem AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj

added def AlgebraicGeometry.Scheme.Opens.topIso

added def AlgebraicGeometry.Scheme.Opens.ι

added theorem AlgebraicGeometry.Scheme.Opens.ι_app

added theorem AlgebraicGeometry.Scheme.Opens.ι_appIso

added theorem AlgebraicGeometry.Scheme.Opens.ι_appLE

added theorem AlgebraicGeometry.Scheme.Opens.ι_app_self

added theorem AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen

added theorem AlgebraicGeometry.Scheme.Opens.ι_image_top

added theorem AlgebraicGeometry.Scheme.Opens.ι_preimage_self

deleted theorem AlgebraicGeometry.Scheme.eq_restrict_presheaf_map_eqToHom

modified theorem AlgebraicGeometry.Scheme.map_basicOpen'

deleted theorem AlgebraicGeometry.Scheme.map_basicOpen

modified theorem AlgebraicGeometry.Scheme.map_basicOpen_map

deleted theorem AlgebraicGeometry.Scheme.ofRestrict_app_self

added def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop

deleted def AlgebraicGeometry.Scheme.resTop

modified def AlgebraicGeometry.Scheme.restrictFunctor

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_hom

modified theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_left

modified def AlgebraicGeometry.Scheme.restrictIsoOfEq

modified def AlgebraicGeometry.Scheme.restrictRestrict

modified def AlgebraicGeometry.Scheme.restrictRestrictComm

modified theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict

modified theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict

deleted theorem AlgebraicGeometry.Scheme.ιOpens_image_top

added theorem AlgebraicGeometry.eqToHom_eq_homOfLE

modified theorem AlgebraicGeometry.image_morphismRestrict_preimage

modified theorem AlgebraicGeometry.isPullback_morphismRestrict

modified def AlgebraicGeometry.morphismRestrict

modified def AlgebraicGeometry.morphismRestrictEq

modified def AlgebraicGeometry.morphismRestrictRestrict

modified def AlgebraicGeometry.morphismRestrictRestrictBasicOpen

modified def AlgebraicGeometry.morphismRestrictStalkMap

modified theorem AlgebraicGeometry.morphismRestrict_app'

modified theorem AlgebraicGeometry.morphismRestrict_app

modified theorem AlgebraicGeometry.morphismRestrict_appLE

modified theorem AlgebraicGeometry.morphismRestrict_base_coe

modified theorem AlgebraicGeometry.morphismRestrict_id

modified theorem AlgebraicGeometry.morphismRestrict_val_base

modified theorem AlgebraicGeometry.morphismRestrict_ι

deleted theorem AlgebraicGeometry.opensRange_ιOpens

modified def AlgebraicGeometry.opensRestrict

modified def AlgebraicGeometry.pullbackRestrictIsoRestrict

modified theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict

modified theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst

modified theorem AlgebraicGeometry.Γ_map_morphismRestrict

Modified Mathlib/AlgebraicGeometry/Scheme.lean

modified def AlgebraicGeometry.Scheme.Hom.appLE

modified theorem AlgebraicGeometry.Scheme.Hom.appLE_eq_app

modified theorem AlgebraicGeometry.Scheme.Hom.app_eq_appLE

modified theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom

modified theorem AlgebraicGeometry.Scheme.app_eq

modified def AlgebraicGeometry.Scheme.basicOpen

modified theorem AlgebraicGeometry.Scheme.basicOpen_appLE

modified theorem AlgebraicGeometry.Scheme.basicOpen_zero

modified theorem AlgebraicGeometry.Scheme.id_app

modified theorem AlgebraicGeometry.Scheme.inv_app

modified theorem AlgebraicGeometry.Scheme.mem_basicOpen_top'

modified theorem AlgebraicGeometry.Scheme.mem_zeroLocus_iff

modified theorem AlgebraicGeometry.Scheme.preimage_basicOpen

added theorem AlgebraicGeometry.Scheme.preimage_comp

modified theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op

modified def AlgebraicGeometry.Scheme.zeroLocus

modified theorem AlgebraicGeometry.Scheme.zeroLocus_def

modified theorem AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ

modified theorem AlgebraicGeometry.Scheme.zeroLocus_isClosed

modified theorem AlgebraicGeometry.Scheme.zeroLocus_singleton

Modified Mathlib/AlgebraicGeometry/Stalk.lean

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq