AlgebraicGeometry.LocallyRingedSpace.Hom.ext
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext :
∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (x y : X.Hom Y), x.val = y.val → x = y
This theorem states that for any two locally ringed spaces `X` and `Y`, and any two homomorphisms `x` and `y` from `X` to `Y`, if the underlying topological space element of `x` is equal to that of `y`, then `x` and `y` are equal. In other words, the equality of locally ringed space homomorphisms is determined by the equality of their underlying topological space elements.
More concisely: If two homomorphisms between locally ringed spaces have equal underlying topological spaces, then they are equal.
|
AlgebraicGeometry.LocallyRingedSpace.Hom.prop
theorem AlgebraicGeometry.LocallyRingedSpace.Hom.prop :
∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (self : X.Hom Y) (x : ↑↑X.toPresheafedSpace),
IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.stalkMap self.val x)
The theorem `AlgebraicGeometry.LocallyRingedSpace.Hom.prop` states that for any two locally ringed spaces 'X' and 'Y', and any morphism from 'X' to 'Y', the induced morphism on the stalks at any point 'x' in 'X' is a local ring homomorphism. This means that the structure of the stalks as local rings is preserved under the morphism, a key property in the study of algebraic geometry.
More concisely: Given any morphism between locally ringed spaces, the induced homomorphism on stalks at each point is a local ring homomorphism.
|
AlgebraicGeometry.LocallyRingedSpace.localRing
theorem AlgebraicGeometry.LocallyRingedSpace.localRing :
∀ (self : AlgebraicGeometry.LocallyRingedSpace) (x : ↑↑self.toPresheafedSpace),
LocalRing ↑(self.presheaf.stalk x)
The theorem `AlgebraicGeometry.LocallyRingedSpace.localRing` states that for any locally ringed space and any point in its corresponding presheafed space, the stalk of the presheaf at that point forms a local ring. In algebraic geometry, this is a key property of locally ringed spaces which reflects the intuitive idea that they "locally look like" the spectrum of a ring.
More concisely: Given a locally ringed space and a point in its underlying topological space, the stalk of the structure sheaf at that point is a local ring.
|