Commit 2024-04-07 14:48 f19f1aa2

View on Github →

feat(AlgebraicGeometry/OpenImmersion): The category structure on the type of open covers of a scheme. (#11946) Morphisms are refinements between open covers.

Estimated changes

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added def AlgebraicGeometry.Scheme.OpenCover.Hom.comp

added def AlgebraicGeometry.Scheme.OpenCover.Hom.id

added structure AlgebraicGeometry.Scheme.OpenCover.Hom

added theorem AlgebraicGeometry.Scheme.OpenCover.comp_app

added theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply

added theorem AlgebraicGeometry.Scheme.OpenCover.id_app

added theorem AlgebraicGeometry.Scheme.OpenCover.id_idx_apply