Commit 2025-10-15 10:06 c368e9e4

chore(AlgebraicGeometry): autumn cleaning (#30426) (everything is in the AlgebraicGeometry namespace; "x" means auto-generated)

Important change

Added instance {X Y : Scheme.{u}} : CoeFun (X ⟶ Y) (fun _ ↦ X → Y). In particular, the preferred way to apply f : X ⟶ Y to x : X is f x instead of f.base x, and the lemma names should be updated accordingly. The pretty printer doesn't work yet but this will be added in a future PR.

Renamed

Scheme.Hom.image_le_image_of_le -> Scheme.Hom.image_mono Scheme.Hom.image_preimage_eq_opensRange_inter -> Scheme.Hom.image_preimage_eq_opensRange_inf Scheme.Hom.map_mem_image_iff -> Scheme.Hom.apply_mem_image_iff Scheme.basic_open_isOpenImmersion -> Scheme.isOpenImmersion_SpecMap_localizationAway IsOpenImmersion.to_iso -> IsOpenImmersion.isIso IsOpenImmersion.of_stalk_iso -> IsOpenImmersion.of_isIso_stalkMap IsOpenImmersion.iff_stalk_iso -> IsOpenImmersion.iff_isIso_stalkMap isIso_iff_stalk_iso -> isIso_iff_isIso_stalkMap IsOpenImmersion.range_pullback_snd_of_left -> IsOpenImmersion.range_pullbackSnd IsOpenImmersion.opensRange_pullback_snd_of_left -> Scheme.Hom.opensRange_pullbackSnd IsOpenImmersion.range_pullback_fst_of_right -> IsOpenImmersion.range_pullbackFst IsOpenImmersion.opensRange_pullback_fst_of_right -> Scheme.Hom.opensRange_pullbackFst IsOpenImmersion.map_ΓIso_hom -> IsOpenImmersion.app_ΓIso_hom isBasis_affine_open -> Scheme.isBasis_affineOpens Scheme.Hom.ι_base_apply -> Scheme.Hom.ι_apply Scheme.map_basicOpen -> Scheme.Opens.ι_image_basicOpen' Scheme.map_basicOpen_map -> Scheme.Opens.ι_image_basicOpen_topIso_inv Scheme.Hom.le_preimage_resLE_iff -> Scheme.Hom.le_resLE_preimage_iff Scheme.Hom.coe_resLE_base -> Scheme.Hom.coe_resLE_apply Scheme.Hom.preimage_iSup_eq_top -> Scheme.Hom.iSup_preimage_eq_top Scheme.Hom.preimage_le_preimage_of_le -> Scheme.Hom.preimage_mono Scheme.preimage_comp -> Scheme.Hom.comp_preimage Scheme.id.base -> Scheme.Hom.id_base Scheme.id_app -> Scheme.Hom.id_app Scheme.id_appTop -> Scheme.Hom.id_appTop Scheme.comp_toLRSHom -> Scheme.Hom.comp_toLRSHom Scheme.comp_toLRSHom_assoc -> Scheme.Hom.comp_toLRSHom_assoc Scheme.comp_coeBase -> Scheme.Hom.comp_base Scheme.comp_coeBase_assoc -> Scheme.Hom.comp_base_assoc Scheme.comp_base -> Scheme.Hom.comp_base Scheme.comp_base_assoc -> Scheme.Hom.comp_base_assoc Scheme.comp_base_apply -> Scheme.Hom.comp_apply Scheme.comp_app -> Scheme.Hom.comp_app Scheme.comp_app_assoc -> Scheme.Hom.comp_app_assoc Scheme.comp_appTop -> Scheme.Hom.comp_appTop Scheme.comp_appTop_assoc -> Scheme.Hom.comp_appTop_assoc Scheme.appLE_comp_appLE -> Scheme.Hom.appLE_comp_appLE Scheme.comp_appLE -> Scheme.Hom.comp_appLE Scheme.comp_appLE_assoc -> Scheme.Hom.comp_appLE_assoc Scheme.congr_app -> Scheme.Hom.congr_app Scheme.app_eq -> Scheme.Hom.app_eq Scheme.eqToHom_c_app -> Scheme.Hom.eqToHom_app Scheme.inv_app -> Scheme.Hom.inv_app Scheme.inv_appTop -> Scheme.Hom.inv_appTop Spec.map_base_apply -> Spec.map_apply Scheme.iso_hom_base_inv_base -> Scheme.hom_base_inv_base Scheme.iso_hom_base_inv_base_apply -> Scheme.hom_inv_apply Scheme.iso_inv_base_hom_base -> Scheme.inv_base_hom_base Scheme.iso_inv_base_hom_base_apply -> Scheme.inv_hom_apply Scheme.stalkMap_id -> Scheme.Hom.stalkMap_id Scheme.stalkMap_comp -> Scheme.Hom.stalkMap_comp Scheme.stalkSpecializes_stalkMap -> Scheme.Hom.stalkSpecializes_stalkMap Scheme.stalkSpecializes_stalkMap_assoc -> Scheme.Hom.stalkSpecializes_stalkMap_assoc Scheme.stalkSpecializes_stalkMap_apply -> Scheme.Hom.stalkSpecializes_stalkMap_apply Scheme.stalkMap_congr -> Scheme.Hom.stalkMap_congr Scheme.stalkMap_congr_assoc -> Scheme.Hom.stalkMap_congr_assoc Scheme.stalkMap_congr_hom -> Scheme.Hom.stalkMap_congr_hom Scheme.stalkMap_congr_hom_assoc -> Scheme.Hom.stalkMap_congr_hom_assoc Scheme.stalkMap_congr_point -> Scheme.Hom.stalkMap_congr_point Scheme.stalkMap_congr_point_assoc -> Scheme.Hom.stalkMap_congr_point_assoc Scheme.stalkMap_hom_inv -> Scheme.Hom.stalkMap_hom_inv Scheme.stalkMap_hom_inv_assoc -> Scheme.Hom.stalkMap_hom_inv_assoc Scheme.stalkMap_hom_inv_apply -> Scheme.Hom.stalkMap_hom_inv_apply Scheme.stalkMap_inv_hom -> Scheme.Hom.stalkMap_inv_hom Scheme.stalkMap_inv_hom_assoc -> Scheme.Hom.stalkMap_inv_hom_assoc Scheme.stalkMap_inv_hom_apply -> Scheme.Hom.stalkMap_inv_hom_apply Scheme.stalkMap_germ -> Scheme.Hom.germ_stalkMap Scheme.stalkMap_germ_assoc -> Scheme.Hom.germ_stalkMap_assoc Scheme.stalkMap_germ_apply -> Scheme.Hom.germ_stalkMap_apply Scheme.arrowStalkMapIsoOfEq -> Scheme.Hom.arrowStalkMapIsoOfEq quasiCompact_iff_spectral -> quasiCompact_iff_isSpectralMap IsAffineOpen.Spec_map_appLE_fromSpec -> IsAffineOpen.SpecMap_appLE_fromSpec IsAffineOpen.Spec_map_appLE_fromSpec_assoc -> IsAffineOpen.SpecMap_appLE_fromSpec_assoc AffineSpace.map_Spec_map -> AffineSpace.map_SpecMap Scheme.Pullback.Triplet.Spec_map_tensor_isPullback -> Scheme.Pullback.Triplet.isPullback_SpecMap_tensor Scheme.Pullback.Triplet.Spec_map_tensorInl_fromSpecResidueField -> Scheme.Pullback.Triplet.SpecMap_tensorInl_fromSpecResidueField Scheme.Spec_map_presheaf_map_eqToHom -> Scheme.SpecMap_presheaf_map_eqToHom Scheme.Spec_map_residue_apply -> Scheme.SpecMap_residue_apply Scheme.Hom.Spec_map_residueFieldMap_fromSpecResidueField -> Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField Scheme.Spec_map_stalkSpecializes_fromSpecStalk -> Scheme.SpecMap_stalkSpecializes_fromSpecStalk Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc -> Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc Scheme.Spec_map_stalkMap_fromSpecStalk -> Scheme.SpecMap_stalkMap_fromSpecStalk Scheme.Spec_map_stalkMap_fromSpecStalk_assoc -> Scheme.SpecMap_stalkMap_fromSpecStalk_assoc IsClosedImmersion.Spec_map_residue -> IsClosedImmersion.SpecMap_residue Spec_map_localization_isIso -> isIso_SpecMap_stakMap_localization stalkwise_Spec_map_iff -> stalkwise_SpecMap_iff IsPreimmersion.Spec_map_iff -> IsPreimmersion.SpecMap_iff IsPreimmersion.mk_Spec_map -> IsPreimmersion.mk_SpecMap diagonal_Spec_map -> diagonal_SpecMap isPullback_Spec_map_isPushout -> isPullback_SpecMap_of_isPushout isPullback_Spec_map_pushout -> isPullback_SpecMap_pushout IsOpenImmersion.forget_preservesOfLeft -> x IsOpenImmersion.forget_preservesOfRight -> x IsOpenImmersion.pullback_snd_of_left -> x IsOpenImmersion.pullback_fst_of_right -> x IsOpenImmersion.pullback_to_base -> x IsOpenImmersion.forgetToTop_preserves_of_left -> x IsOpenImmersion.forgetToTop_preserves_of_right -> x fromGlued_stalk_iso -> x fromGlued_open_map -> isOpenMap_fromGlued fromGlued_isOpenEmbedding -> isOpenEmbedding_fromGlued fromGlued_open_immersion -> x IsAffineOpen.isoSpec_hom_base_apply -> IsAffineOpen.isoSpec_hom_apply isoSpec_hom_base_apply -> isoSpec_hom_apply Scheme.Pullback.Triplet.specTensorTo_base_fst -> Scheme.Pullback.Triplet.fst_SpecTensorTo_apply Scheme.Pullback.Triplet.specTensorTo_base_snd -> Scheme.Pullback.Triplet.snd_SpecTensorTo_apply Scheme.toSpecΓ_base -> Scheme.toSpecΓ_apply basicOpen_union_eq_self_iff -> iSup_basicOpen_eq_self_iff self_le_basicOpen_union_iff -> self_le_iSup_basicOpen_iff Scheme.Opens.toSpecΓ_SpecMap_map -> Scheme.Opens.toSpecΓ_SpecMap_presheaf_map Scheme.Opens.toSpecΓ_SpecMap_map_assoc -> Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc isIso_iff_isOpenImmersion -> isIso_iff_isOpenImmersion_and_epi_base isCompactOpen_iff_eq_finset_affine_union -> isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens isCompactOpen_iff_eq_basicOpen_union -> isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen

Removed

Scheme.presheaf_map_eqToHom_op affinePreimage instance : Inhabited Scheme Γ_map_morphismRestrict eqToHom_eq_homOfLE

Added

instance {X Y : Scheme.{u}} : CoeFun (X ⟶ Y) (fun _ ↦ X → Y) Scheme.Opens.toSpecΓ_preimage_basicOpen Scheme.Hom.isSpectralMap isCompact_iff_finite_and_eq_biUnion_affineOpens Scheme.Hom.coe_image Scheme.Hom.comp_image Scheme.Hom.id_image Scheme.Hom.inv_image Scheme.Hom.mem_preimage Scheme.Hom.coe_preimage Scheme.Hom.preimage_sup Scheme.Hom.preimage_inf Scheme.Hom.preimage_top Scheme.Hom.preimage_bot Scheme.Hom.id_preimage Scheme.Opens.mem_ι_image_iff IsAffine.iff_of_isIso SpecMap_ΓSpecIso_inv_toSpecΓ SpecMap_ΓSpecIso_inv_toSpecΓ_assoc toSpecΓ_SpecMap_ΓSpecIso_inv toSpecΓ_SpecMap_ΓSpecIso_inv_assoc Scheme.Opens.toSpecΓ_SpecMap_map_top Scheme.Opens.toSpecΓ_SpecMap_map_top_assoc Scheme.Opens.toSpecΓ_naturality Scheme.Opens.toSpecΓ_naturality_assoc IsAffineOpen.fromSpec_toSpecΓ IsAffineOpen.fromSpec_toSpecΓ_assoc IsAffineOpen.preimage_of_isOpenImmersion Scheme.Hom.image_le_opensRange Scheme.Hom.image_preimage_le Scheme.Opens.mem_basicOpen_toScheme Scheme.homOfLE_appLE Scheme.opensRange_homOfLE