Commit 2024-06-25 01:47 214438ff

View on Github →

feat(AlgebraicGeometry) Add more API (#14052)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map

added def AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv

added def AlgebraicGeometry.affineOpensRestrict

added theorem AlgebraicGeometry.affineOpensRestrict_symm_apply_coe

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

added def AlgebraicGeometry.Spec.homEquiv

added def AlgebraicGeometry.Spec.preimage

added theorem AlgebraicGeometry.SpecMap_inj

added theorem AlgebraicGeometry.SpecMap_injective

added theorem AlgebraicGeometry.SpecMap_preimage

added theorem AlgebraicGeometry.preimage_specMap

modified def AlgebraicGeometry.ΓSpec.adjunction

added theorem AlgebraicGeometry.ΓSpec.adjunction_unit_naturality

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added def AlgebraicGeometry.IsOpenImmersion.opensEquiv

added theorem AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_fst_of_right

added theorem AlgebraicGeometry.IsOpenImmersion.opensRange_pullback_snd_of_left

added theorem AlgebraicGeometry.Scheme.Hom.app_invApp'

added theorem AlgebraicGeometry.Scheme.Hom.app_invApp

modified def AlgebraicGeometry.Scheme.Hom.invApp

added theorem AlgebraicGeometry.Scheme.Hom.invApp_app

added theorem AlgebraicGeometry.Scheme.Hom.invApp_naturality

added theorem AlgebraicGeometry.Scheme.Hom.inv_invApp

added theorem AlgebraicGeometry.Scheme.Hom.openEmbedding

modified def AlgebraicGeometry.Scheme.Hom.opensRange

modified def AlgebraicGeometry.Scheme.ofRestrict

added theorem AlgebraicGeometry.Scheme.ofRestrict_app

added theorem AlgebraicGeometry.Scheme.ofRestrict_appLE

modified def AlgebraicGeometry.Scheme.restrict

added theorem AlgebraicGeometry.Scheme.restrict_presheaf_map

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.morphismRestrict_app'

added theorem AlgebraicGeometry.morphismRestrict_appLE

added theorem AlgebraicGeometry.opensRange_ιOpens

added def AlgebraicGeometry.opensRestrict

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added def AlgebraicGeometry.Scheme.Hom.appLE

added theorem AlgebraicGeometry.Scheme.Hom.appLE_congr

added theorem AlgebraicGeometry.Scheme.Hom.appLE_map'

added theorem AlgebraicGeometry.Scheme.Hom.appLE_map

added theorem AlgebraicGeometry.Scheme.Hom.app_eq_appLE

added theorem AlgebraicGeometry.Scheme.Hom.map_appLE'

added theorem AlgebraicGeometry.Scheme.Hom.map_appLE

added theorem AlgebraicGeometry.Scheme.Hom.naturality

modified def AlgebraicGeometry.Scheme.Spec

deleted theorem AlgebraicGeometry.Scheme.Spec_map_appLE

deleted theorem AlgebraicGeometry.Scheme.Spec_map_base

deleted theorem AlgebraicGeometry.Scheme.Spec_map_c_app

deleted theorem AlgebraicGeometry.Scheme.Spec_obj_carrier

deleted theorem AlgebraicGeometry.Scheme.Spec_obj_presheaf

deleted theorem AlgebraicGeometry.Scheme.Spec_obj_sheaf

added theorem AlgebraicGeometry.Scheme.SpecΓIdentity_app

added theorem AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app

added theorem AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app

added theorem AlgebraicGeometry.Scheme.appLE_comp_appLE

added theorem AlgebraicGeometry.Scheme.comp_appLE

deleted def AlgebraicGeometry.Scheme.specMap

deleted theorem AlgebraicGeometry.Scheme.specMap_comp

deleted theorem AlgebraicGeometry.Scheme.specMap_id

deleted def AlgebraicGeometry.Scheme.specObj

deleted theorem AlgebraicGeometry.Scheme.specObj_toLocallyRingedSpace

added theorem AlgebraicGeometry.Scheme.toOpen_eq

added def AlgebraicGeometry.Scheme.ΓSpecIso

added theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv

added theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality

added theorem AlgebraicGeometry.Scheme.ΓSpecIso_naturality

added theorem AlgebraicGeometry.SpecMap_app

added theorem AlgebraicGeometry.SpecMap_appLE

added theorem AlgebraicGeometry.SpecMap_comp

added theorem AlgebraicGeometry.SpecMap_eqToHom

added theorem AlgebraicGeometry.SpecMap_id

added theorem AlgebraicGeometry.SpecMap_inv

added theorem AlgebraicGeometry.Spec_map_base

added theorem AlgebraicGeometry.Spec_obj_carrier

added theorem AlgebraicGeometry.Spec_obj_presheaf

added theorem AlgebraicGeometry.Spec_obj_sheaf

added theorem AlgebraicGeometry.Spec_toLocallyRingedSpace

added def AlgebraicGeometry.specMap

added def AlgebraicGeometry.specObj