Commit 2024-06-25 05:48 b0f8ad02

View on Github →

refactor(AlgebraicGeometry): Use Scheme.Hom.app as simp normal form (#14031)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.ιOpens_basicOpen_preimage

deleted theorem AlgebraicGeometry.IsAffineOpen.ιOpens_preimage

modified def AlgebraicGeometry.Scheme.isoSpec

modified theorem AlgebraicGeometry.of_affine_open_cover

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

modified def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine

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 def AlgebraicGeometry.Spec.homEquiv

added theorem AlgebraicGeometry.Spec.map_inj

added theorem AlgebraicGeometry.Spec.map_injective

added theorem AlgebraicGeometry.Spec.map_preimage

added theorem AlgebraicGeometry.Spec.preimage_map

deleted theorem AlgebraicGeometry.SpecMap_inj

deleted theorem AlgebraicGeometry.SpecMap_injective

deleted theorem AlgebraicGeometry.SpecMap_preimage

deleted theorem AlgebraicGeometry.SpecΓIdentity_hom_app_presheaf_obj

deleted theorem AlgebraicGeometry.SpecΓIdentity_naturality

deleted theorem AlgebraicGeometry.preimage_specMap

added theorem AlgebraicGeometry.ΓSpec.SpecMap_ΓSpecIso_hom

deleted theorem AlgebraicGeometry.ΓSpec.adjunction_unit_app_Spec

added theorem AlgebraicGeometry.ΓSpecIso_obj_hom

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

modified theorem AlgebraicGeometry.isAffineOpen_bot

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

deleted theorem AlgebraicGeometry.IsAffineOpen.map_isIso

added theorem AlgebraicGeometry.IsAffineOpen.preimage_of_isIso

deleted theorem AlgebraicGeometry.targetAffineLocallyOfOpenCover

added theorem AlgebraicGeometry.targetAffineLocally_of_openCover

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

deleted theorem AlgebraicGeometry.locallyOfFiniteTypeOfComp

added theorem AlgebraicGeometry.locallyOfFiniteType_of_comp

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

modified theorem AlgebraicGeometry.compact_open_induction_on

added theorem AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union

added theorem AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union

modified theorem AlgebraicGeometry.isCompact_basicOpen

deleted theorem AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union

deleted theorem AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union

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/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux

deleted theorem AlgebraicGeometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq_aux

modified def AlgebraicGeometry.Scheme.Hom.opensRange

modified theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace

Modified Mathlib/AlgebraicGeometry/Properties.lean

modified theorem AlgebraicGeometry.basicOpen_eq_bot_iff

modified theorem AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced

modified theorem AlgebraicGeometry.isIntegral_of_isAffine_of_isDomain

modified theorem AlgebraicGeometry.isReduced_of_isAffine_isReduced

modified theorem AlgebraicGeometry.reduce_to_affine_nbhd

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.ofRestrict_app_self

deleted theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app_self

added theorem AlgebraicGeometry.morphismRestrict_app

deleted theorem AlgebraicGeometry.morphismRestrict_c_app

Modified Mathlib/AlgebraicGeometry/Scheme.lean

deleted def AlgebraicGeometry.Scheme.Spec

modified theorem AlgebraicGeometry.Scheme.SpecΓIdentity_app

modified theorem AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app

modified theorem AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app

added theorem AlgebraicGeometry.Scheme.comp_app

deleted theorem AlgebraicGeometry.Scheme.comp_val_c_app

modified theorem AlgebraicGeometry.Scheme.id_app

added theorem AlgebraicGeometry.Scheme.inv_app

added theorem AlgebraicGeometry.Scheme.inv_app_top

deleted theorem AlgebraicGeometry.Scheme.inv_val_c_app

deleted theorem AlgebraicGeometry.Scheme.inv_val_c_app_top

modified def AlgebraicGeometry.Scheme.ΓSpecIso

modified theorem AlgebraicGeometry.Scheme.Γ_map

modified theorem AlgebraicGeometry.Scheme.Γ_map_op

modified theorem AlgebraicGeometry.Scheme.Γ_obj

added def AlgebraicGeometry.Spec.map

added theorem AlgebraicGeometry.Spec.map_app

added theorem AlgebraicGeometry.Spec.map_appLE

added theorem AlgebraicGeometry.Spec.map_base

added theorem AlgebraicGeometry.Spec.map_comp

added theorem AlgebraicGeometry.Spec.map_eqToHom

added theorem AlgebraicGeometry.Spec.map_id

added theorem AlgebraicGeometry.Spec.map_inv

added def AlgebraicGeometry.Spec

deleted theorem AlgebraicGeometry.SpecMap_app

deleted theorem AlgebraicGeometry.SpecMap_appLE

deleted theorem AlgebraicGeometry.SpecMap_comp

deleted theorem AlgebraicGeometry.SpecMap_eqToHom

deleted theorem AlgebraicGeometry.SpecMap_id

deleted theorem AlgebraicGeometry.SpecMap_inv

added theorem AlgebraicGeometry.Spec_carrier

deleted theorem AlgebraicGeometry.Spec_map_base

deleted theorem AlgebraicGeometry.Spec_obj_carrier

deleted theorem AlgebraicGeometry.Spec_obj_presheaf

deleted theorem AlgebraicGeometry.Spec_obj_sheaf

added theorem AlgebraicGeometry.Spec_presheaf

added theorem AlgebraicGeometry.Spec_sheaf

modified theorem AlgebraicGeometry.basicOpen_eq_of_affine'

deleted def AlgebraicGeometry.specMap

deleted def AlgebraicGeometry.specObj

Modified Mathlib/AlgebraicGeometry/Sites/BigZariski.lean