Commit 2024-10-12 05:37 33614d2c

View on Github →

feat(AlgebraicGeometry): API for affine opens (#15259)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.Spec_map_appLE_fromSpec

deleted theorem AlgebraicGeometry.IsAffineOpen.SpecΓIdentity_hom_app_fromSpec

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le

added theorem AlgebraicGeometry.IsAffineOpen.fromSpec_top

added def AlgebraicGeometry.IsAffineOpen.isoSpec

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_app_top

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom_val_base_apply

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_app_top

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι

added theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint

added theorem AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app

added theorem AlgebraicGeometry.Scheme.isoSpec_Spec

added theorem AlgebraicGeometry.Scheme.isoSpec_Spec_hom

added theorem AlgebraicGeometry.Scheme.isoSpec_Spec_inv

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added theorem AlgebraicGeometry.Scheme.toSpecΓ_val_base