Commit 2024-11-24 13:54 6c225037

View on Github →

chore(AlgebraicGeometry) add Scheme.Hom.appTop (#19130) to hide the defeq abuse f ⁻¹ᵁ ⊤ = ⊤

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop

deleted theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_app_top

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop

deleted theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_app_top

modified theorem AlgebraicGeometry.ext_of_isAffine

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

added theorem AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop

deleted theorem AlgebraicGeometry.AffineSpace.SpecIso_hom_app_top

added theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord

deleted theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord

deleted theorem AlgebraicGeometry.AffineSpace.homOfVector_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop

deleted theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_app_top

added theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord

deleted theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.map_appTop_coord

deleted theorem AlgebraicGeometry.AffineSpace.map_app_top_coord

added theorem AlgebraicGeometry.AffineSpace.reindex_appTop_coord

deleted theorem AlgebraicGeometry.AffineSpace.reindex_app_top_coord

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.Scheme.toSpecΓ_appTop

deleted theorem AlgebraicGeometry.Scheme.toSpecΓ_app_top

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

added theorem AlgebraicGeometry.HasRingHomProperty.appTop

deleted theorem AlgebraicGeometry.HasRingHomProperty.app_top

added theorem RingHom.IsStableUnderBaseChange.pullback_fst_appTop

deleted theorem RingHom.IsStableUnderBaseChange.pullback_fst_app_top

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Opens.ι_appTop

added theorem AlgebraicGeometry.Scheme.homOfLE_appTop

added theorem AlgebraicGeometry.morphismRestrict_appTop

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.comp_appTop

added theorem AlgebraicGeometry.Scheme.id_appTop

added theorem AlgebraicGeometry.Scheme.inv_appTop

deleted theorem AlgebraicGeometry.Scheme.inv_app_top

added theorem AlgebraicGeometry.Scheme.preimage_basicOpen_top

modified theorem AlgebraicGeometry.Scheme.Γ_map

modified theorem AlgebraicGeometry.Scheme.Γ_map_op

Modified Mathlib/AlgebraicGeometry/Stalk.lean

added theorem AlgebraicGeometry.Scheme.fromSpecStalk_appTop

Modified Mathlib/AlgebraicGeometry/ValuativeCriterion.lean