Commit 2024-10-23 19:07 d747c920

View on Github →

feat(AlgebraicGeometry): spreading out morphisms on stalks (#17987)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.IsAffineOpen.isoSpec_hom

modified theorem AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec

added def AlgebraicGeometry.Scheme.Opens.toSpecΓ

Created Mathlib/AlgebraicGeometry/SpreadingOut.lean

added theorem AlgebraicGeometry.Scheme.IsGermInjective.Spec

added theorem AlgebraicGeometry.Scheme.IsGermInjective.of_openCover

added theorem AlgebraicGeometry.Scheme.exists_germ_injective

added theorem AlgebraicGeometry.Scheme.exists_le_and_germ_injective

added theorem AlgebraicGeometry.exists_lift_of_germInjective

added theorem AlgebraicGeometry.exists_lift_of_germInjective_aux

added theorem AlgebraicGeometry.injective_germ_basicOpen

added theorem AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion

added theorem AlgebraicGeometry.spread_out_of_isGermInjective

added theorem AlgebraicGeometry.spread_out_unique_of_isGermInjective

Modified Mathlib/AlgebraicGeometry/Stalk.lean

added def AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem

added theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ

added theorem AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ