Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-24 21:41
2b9299ee
View on Github →
feat(AlgebraicGeometry): API for zero locus (
#20812
)
Estimated changes
Modified
Mathlib/AlgebraicGeometry/AffineScheme.lean
added
theorem
AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus
added
theorem
AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus
modified
theorem
AlgebraicGeometry.IsAffineOpen.isoSpec_hom
added
theorem
AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ
added
theorem
AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec
added
theorem
AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv
added
theorem
AlgebraicGeometry.Scheme.Opens.toSpecΓ_appTop
added
theorem
AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus
modified
theorem
AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine
added
theorem
AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus
added
theorem
AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus
added
theorem
AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus
added
theorem
AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ
added
theorem
AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus
added
theorem
AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv
added
theorem
AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus
deleted
theorem
AlgebraicGeometry.Scheme.toΓSpec_image_zeroLocus_eq_of_isAffine
deleted
theorem
AlgebraicGeometry.Scheme.toΓSpec_preimage_zeroLocus_eq
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_biInf
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_iInf
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_inf
Modified
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
Modified
Mathlib/AlgebraicGeometry/OpenImmersion.lean
added
theorem
AlgebraicGeometry.Scheme.Hom.map_mem_image_iff
modified
theorem
AlgebraicGeometry.Scheme.image_basicOpen
added
theorem
AlgebraicGeometry.Scheme.image_zeroLocus
Modified
Mathlib/AlgebraicGeometry/Scheme.lean
added
theorem
AlgebraicGeometry.Scheme.basicOpen_add_le
added
theorem
AlgebraicGeometry.Scheme.basicOpen_one
added
theorem
AlgebraicGeometry.Scheme.codisjoint_zeroLocus
added
theorem
AlgebraicGeometry.Scheme.preimage_zeroLocus
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_map
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_map_of_eq
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_mono
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_span
added
theorem
AlgebraicGeometry.Scheme.zeroLocus_univ
added
theorem
AlgebraicGeometry.Spec_zeroLocus
added
theorem
AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus
Modified
Mathlib/Order/BooleanAlgebra.lean
added
theorem
codisjoint_iff_compl_le_left
added
theorem
codisjoint_iff_compl_le_right
Modified
Mathlib/Topology/Sets/Opens.lean
added
theorem
TopologicalSpace.Opens.mem_bot
added
theorem
TopologicalSpace.Opens.mem_inf