Commit 2024-10-03 17:44 24a4b4a6

View on Github →

refactor(AlgebraicGeometry): Introduce Scheme.toSpecΓ (#15082)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added def AlgebraicGeometry.Scheme.toSpecΓ

added theorem AlgebraicGeometry.Scheme.toSpecΓ_app_top

added theorem AlgebraicGeometry.Scheme.toSpecΓ_naturality

added theorem AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen

added theorem AlgebraicGeometry.SpecMap_ΓSpecIso_hom

added theorem AlgebraicGeometry.toOpen_toSpecΓ_app

deleted theorem AlgebraicGeometry.ΓSpec.SpecMap_ΓSpecIso_hom

deleted theorem AlgebraicGeometry.ΓSpec.adjunction_unit_app_app_top

deleted theorem AlgebraicGeometry.ΓSpec.adjunction_unit_map_basicOpen

deleted theorem AlgebraicGeometry.ΓSpec.adjunction_unit_naturality

deleted theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app'

deleted theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean