Commit 2023-11-12 21:46 ace6e091

View on Github →

perf(AlgebraicGeometry): Fix slow and bad proofs (#7747) Fixed AlgebraicGeometry/AffineSchemes.lean, AlgebraicGeometry/Morphisms/QuasiSeparated.lean and AlgebraicGeometry/Morphisms/RingHomProperties.lean.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.toRingEquiv_toRingHom

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec

modified theorem AlgebraicGeometry.IsAffineOpen.basicOpenIsAffine

added def AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine

added theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen

modified theorem AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app

modified theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff

modified theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le

modified def AlgebraicGeometry.IsAffineOpen.fromSpec

deleted theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_eq

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_self

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpec_base_preimage

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpec_image_top

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen'

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf

modified theorem AlgebraicGeometry.IsAffineOpen.fromSpec_range

modified theorem AlgebraicGeometry.IsAffineOpen.imageIsOpenImmersion

deleted theorem AlgebraicGeometry.IsAffineOpen.isCompact

added theorem AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen

added theorem AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen

modified theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk'

modified theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk

deleted theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux'

deleted theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk_aux

modified theorem AlgebraicGeometry.IsAffineOpen.mapRestrictBasicOpen

added theorem AlgebraicGeometry.IsAffineOpen.opensFunctor_map_basicOpen

deleted theorem AlgebraicGeometry.IsAffineOpen.opens_map_fromSpec_basicOpen

modified theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff

added theorem AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion

deleted theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom

modified def AlgebraicGeometry.Scheme.affineBasicOpen

modified theorem AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine

deleted def AlgebraicGeometry.basicOpenSectionsToAffine

deleted theorem AlgebraicGeometry.basicOpen_basicOpen_is_basicOpen

modified theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter

deleted theorem AlgebraicGeometry.isAffineOpen_iff_of_isOpenImmersion

deleted theorem AlgebraicGeometry.isLocalization_basicOpen

deleted theorem AlgebraicGeometry.isLocalization_of_eq_basicOpen

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.SpecΓIdentity_hom_app_presheaf_obj

added theorem AlgebraicGeometry.SpecΓIdentity_naturality

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.eq_restrict_presheaf_map_eqToHom

added theorem AlgebraicGeometry.Scheme.map_basicOpen'

added theorem AlgebraicGeometry.Scheme.map_basicOpen

added theorem AlgebraicGeometry.Scheme.map_basicOpen_map

added theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app_self

modified theorem AlgebraicGeometry.image_morphismRestrict_preimage

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom

added theorem AlgebraicGeometry.Scheme.basicOpen_restrict

added theorem AlgebraicGeometry.Scheme.inv_val_c_app_top

Modified Mathlib/RingTheory/LocalProperties.lean

added theorem RingHom.OfLocalizationSpanTarget.ofIsLocalization

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem Localization.coe_algEquiv

added theorem Localization.coe_algEquiv_symm

Modified Mathlib/Topology/Category/TopCat/Opens.lean

added theorem OpenEmbedding.functor_obj_injective

added theorem TopologicalSpace.Opens.map_top

Modified Mathlib/Topology/Sheaves/Presheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

added theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff

Modified lean-toolchain