Commit 2024-06-19 15:38 1e77bedd

View on Github →

chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own file. (#13942)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Created Mathlib/AlgebraicGeometry/Cover/Open.lean

added def AlgebraicGeometry.Scheme.AffineOpenCover.openCover

added structure AlgebraicGeometry.Scheme.AffineOpenCover

added def AlgebraicGeometry.Scheme.OpenCover.Hom.comp

added def AlgebraicGeometry.Scheme.OpenCover.Hom.id

added structure AlgebraicGeometry.Scheme.OpenCover.Hom

added def AlgebraicGeometry.Scheme.OpenCover.add

added def AlgebraicGeometry.Scheme.OpenCover.affineRefinement

added def AlgebraicGeometry.Scheme.OpenCover.bind

added theorem AlgebraicGeometry.Scheme.OpenCover.comp_app

added theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply

added theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace

added def AlgebraicGeometry.Scheme.OpenCover.copy

added def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover

added def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement

added theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange

added theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range

added theorem AlgebraicGeometry.Scheme.OpenCover.id_app

added theorem AlgebraicGeometry.Scheme.OpenCover.id_idx_apply

added def AlgebraicGeometry.Scheme.OpenCover.inter

added def AlgebraicGeometry.Scheme.OpenCover.pullbackCover'

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 def AlgebraicGeometry.Scheme.affineOpenCover

added def AlgebraicGeometry.Scheme.openCoverOfIsIso

added def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop

added theorem AlgebraicGeometry.Scheme.openCover_affineOpenCover

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

deleted def AlgebraicGeometry.Scheme.AffineOpenCover.openCover

deleted structure AlgebraicGeometry.Scheme.AffineOpenCover

modified def AlgebraicGeometry.Scheme.Hom.opensRange

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.affineRefinement

deleted def AlgebraicGeometry.Scheme.OpenCover.bind

deleted theorem AlgebraicGeometry.Scheme.OpenCover.comp_app

deleted theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply

deleted theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace

deleted def AlgebraicGeometry.Scheme.OpenCover.copy

deleted def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover

deleted def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement

deleted theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange

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.pushforwardIso

deleted structure AlgebraicGeometry.Scheme.OpenCover

deleted def AlgebraicGeometry.Scheme.affineBasisCover

deleted def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine

deleted def AlgebraicGeometry.Scheme.affineBasisCoverRing

deleted theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis

deleted theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range

deleted theorem AlgebraicGeometry.Scheme.affineBasisCover_obj

deleted def AlgebraicGeometry.Scheme.affineCover

deleted def AlgebraicGeometry.Scheme.affineOpenCover

added theorem AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset

deleted def AlgebraicGeometry.Scheme.openCoverOfIsIso

deleted def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop

deleted theorem AlgebraicGeometry.Scheme.openCover_affineOpenCover

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean