Commit 2023-07-01 06:44 d9d26c4f

View on Github →

feat: port AlgebraicGeometry.Morphisms.OpenImmersion (#5638)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

added theorem AlgebraicGeometry.IsOpenImmersion.openCover_TFAE

added theorem AlgebraicGeometry.IsOpenImmersion.openCover_iff

added theorem AlgebraicGeometry.isOpenImmersion_iff_stalk

added theorem AlgebraicGeometry.isOpenImmersion_is_local_at_target

added theorem AlgebraicGeometry.isOpenImmersion_respectsIso

added theorem AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange

added theorem AlgebraicGeometry.isOpenImmersion_stableUnderComposition