Commit 2024-11-09 09:38 c804d44f

View on Github →

refactor(AlgebraicGeometry): replace OpenCover by Cover @IsOpenImmersion (#18727) This prepares for more general notions of IsLocalAtTarget etc. notions and is one option for defining sites defined by morphism properties.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Created Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

added def AlgebraicGeometry.Scheme.AffineCover.cover

added structure AlgebraicGeometry.Scheme.AffineCover

added def AlgebraicGeometry.Scheme.Cover.Hom.comp

added def AlgebraicGeometry.Scheme.Cover.Hom.id

added structure AlgebraicGeometry.Scheme.Cover.Hom

added def AlgebraicGeometry.Scheme.Cover.add

added def AlgebraicGeometry.Scheme.Cover.bind

added theorem AlgebraicGeometry.Scheme.Cover.comp_app

added theorem AlgebraicGeometry.Scheme.Cover.comp_idx_apply

added def AlgebraicGeometry.Scheme.Cover.copy

added theorem AlgebraicGeometry.Scheme.Cover.iUnion_range

added theorem AlgebraicGeometry.Scheme.Cover.id_app

added theorem AlgebraicGeometry.Scheme.Cover.id_idx_apply

added def AlgebraicGeometry.Scheme.Cover.inter

added def AlgebraicGeometry.Scheme.Cover.pullbackCover'

added def AlgebraicGeometry.Scheme.Cover.pullbackCover

added def AlgebraicGeometry.Scheme.Cover.pullbackHom

added theorem AlgebraicGeometry.Scheme.Cover.pullbackHom_map

added def AlgebraicGeometry.Scheme.Cover.pushforwardIso

added structure AlgebraicGeometry.Scheme.Cover

added theorem AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop

added def AlgebraicGeometry.Scheme.coverOfIsIso

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

modified def AlgebraicGeometry.Scheme.AffineOpenCover.openCover

deleted structure AlgebraicGeometry.Scheme.AffineOpenCover

deleted def AlgebraicGeometry.Scheme.OpenCover.Hom.comp

deleted def AlgebraicGeometry.Scheme.OpenCover.Hom.id

deleted structure AlgebraicGeometry.Scheme.OpenCover.Hom

deleted def AlgebraicGeometry.Scheme.OpenCover.add

deleted def AlgebraicGeometry.Scheme.OpenCover.bind

deleted theorem AlgebraicGeometry.Scheme.OpenCover.comp_app

deleted theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply

deleted def AlgebraicGeometry.Scheme.OpenCover.copy

deleted theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range

deleted theorem AlgebraicGeometry.Scheme.OpenCover.id_app

deleted theorem AlgebraicGeometry.Scheme.OpenCover.id_idx_apply

deleted def AlgebraicGeometry.Scheme.OpenCover.inter

deleted def AlgebraicGeometry.Scheme.OpenCover.pullbackCover'

deleted def AlgebraicGeometry.Scheme.OpenCover.pullbackCover

deleted def AlgebraicGeometry.Scheme.OpenCover.pullbackHom

deleted theorem AlgebraicGeometry.Scheme.OpenCover.pullbackHom_map

deleted def AlgebraicGeometry.Scheme.OpenCover.pushforwardIso

deleted structure AlgebraicGeometry.Scheme.OpenCover

deleted def AlgebraicGeometry.Scheme.openCoverOfIsIso

Modified Mathlib/AlgebraicGeometry/Gluing.lean

added def AlgebraicGeometry.Scheme.Cover.fromGlued

added theorem AlgebraicGeometry.Scheme.Cover.fromGlued_injective

added theorem AlgebraicGeometry.Scheme.Cover.fromGlued_isOpenEmbedding

added theorem AlgebraicGeometry.Scheme.Cover.fromGlued_open_map

added def AlgebraicGeometry.Scheme.Cover.glueMorphisms

added def AlgebraicGeometry.Scheme.Cover.gluedCover

added def AlgebraicGeometry.Scheme.Cover.gluedCoverT'

added theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst

added theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd

added theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst

added theorem AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd

added theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle

added theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst

added theorem AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd

added theorem AlgebraicGeometry.Scheme.Cover.hom_ext

added theorem AlgebraicGeometry.Scheme.Cover.ι_fromGlued

added theorem AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms

deleted def AlgebraicGeometry.Scheme.OpenCover.fromGlued

deleted theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_injective

deleted theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_isOpenEmbedding

deleted theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued_open_map

deleted def AlgebraicGeometry.Scheme.OpenCover.glueMorphisms

deleted def AlgebraicGeometry.Scheme.OpenCover.gluedCover

deleted def AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'

deleted theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_fst

deleted theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_fst_snd

deleted theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_fst

deleted theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd

deleted theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle

deleted theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle_fst

deleted theorem AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle_snd

deleted theorem AlgebraicGeometry.Scheme.OpenCover.hom_ext

deleted theorem AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued

deleted theorem AlgebraicGeometry.Scheme.OpenCover.ι_glueMorphisms

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Noetherian.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/PullbackCarrier.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

added theorem CategoryTheory.IsPullback.hasPullback

added theorem CategoryTheory.IsPushout.hasPushout

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

modified theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'

modified theorem CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk'