Mathlib Changelog
v4
Changelog
About
Github
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Γ