Commit 2023-06-22 15:02 a5e9328b

View on Github →

feat: port AlgebraicGeometry.OpenImmersion.Scheme (#5290)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/OpenImmersion/Scheme.lean

added theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq

added theorem AlgebraicGeometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq_aux

added theorem AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso

added def AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq

added def AlgebraicGeometry.IsOpenImmersion.isoRestrict

added def AlgebraicGeometry.IsOpenImmersion.lift

added theorem AlgebraicGeometry.IsOpenImmersion.lift_app

added theorem AlgebraicGeometry.IsOpenImmersion.lift_fac

added theorem AlgebraicGeometry.IsOpenImmersion.lift_uniq

added theorem AlgebraicGeometry.IsOpenImmersion.of_stalk_iso

added theorem AlgebraicGeometry.IsOpenImmersion.open_range

added theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right

added theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left

added theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left

added theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right

added theorem AlgebraicGeometry.IsOpenImmersion.to_iso

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme

added def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_val

added theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme_toLocallyRingedSpace

added def AlgebraicGeometry.Scheme.Hom.invApp

added def AlgebraicGeometry.Scheme.Hom.opensRange

added def AlgebraicGeometry.Scheme.OpenCover.add

added def AlgebraicGeometry.Scheme.OpenCover.bind

added theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace

added def AlgebraicGeometry.Scheme.OpenCover.copy

added def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover

added theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange

added theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range

added def AlgebraicGeometry.Scheme.OpenCover.inter

added def AlgebraicGeometry.Scheme.OpenCover.pullbackCover

added def AlgebraicGeometry.Scheme.OpenCover.pushforwardIso

added structure AlgebraicGeometry.Scheme.OpenCover

added def AlgebraicGeometry.Scheme.affineBasisCover

added def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine

added def AlgebraicGeometry.Scheme.affineBasisCoverRing

added theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis

added theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range

added theorem AlgebraicGeometry.Scheme.affineBasisCover_obj

added def AlgebraicGeometry.Scheme.affineCover

added theorem AlgebraicGeometry.Scheme.image_basicOpen

added def AlgebraicGeometry.Scheme.ofRestrict

added def AlgebraicGeometry.Scheme.openCoverOfIsIso

added def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop

added def AlgebraicGeometry.Scheme.restrict

added def AlgebraicGeometry.Scheme.restrictFunctor

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_app_aux

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_base

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_left

added theorem AlgebraicGeometry.Scheme.restrictFunctor_map_ofRestrict

added theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_hom

added theorem AlgebraicGeometry.Scheme.restrictFunctor_obj_left

added def AlgebraicGeometry.Scheme.restrictFunctorΓ

added theorem AlgebraicGeometry.image_morphismRestrict_preimage

added theorem AlgebraicGeometry.isIso_iff_isOpenImmersion

added theorem AlgebraicGeometry.isIso_iff_stalk_iso

added theorem AlgebraicGeometry.isPullback_morphismRestrict

added def AlgebraicGeometry.morphismRestrict

added def AlgebraicGeometry.morphismRestrictEq

added def AlgebraicGeometry.morphismRestrictOpensRange

added def AlgebraicGeometry.morphismRestrictRestrict

added def AlgebraicGeometry.morphismRestrictRestrictBasicOpen

added def AlgebraicGeometry.morphismRestrictStalkMap

added theorem AlgebraicGeometry.morphismRestrict_base_coe

added theorem AlgebraicGeometry.morphismRestrict_c_app

added theorem AlgebraicGeometry.morphismRestrict_comp

added theorem AlgebraicGeometry.morphismRestrict_val_base

added theorem AlgebraicGeometry.morphismRestrict_ι

added def AlgebraicGeometry.pullbackRestrictIsoRestrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict

added theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst

added theorem AlgebraicGeometry.Γ_map_morphismRestrict

Modified Mathlib/AlgebraicGeometry/Scheme.lean