AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac
theorem AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac :
∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
[H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] (H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base),
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H') f = g
The theorem `AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac` states that for any three locally ringed spaces `X`, `Y`, and `Z`, and morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, given that `f` is an open immersion and the range of `g` is a subset of the range of `f`, the composition of the lift of `g` along `f` and `f` is equal to `g`. In other words, if we 'lift' `g` along `f` (which is an open immersion), and then apply `f`, we get back `g`. This can be seen as a property of 'lifting' operations in the category of locally ringed spaces.
More concisely: Given locally ringed spaces X, Y, Z and morphisms f : X -> Z and g : Y -> Z with f an open immersion and g(Y) a subset of f(X), the lift of g along f, followed by f, equals g.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
{f : X ⟶ Y} [self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f], OpenEmbedding ⇑f.base
This theorem states that for any category `C`, and any two presheafed spaces `X` and `Y` over `C`, if there is a morphism `f` from `X` to `Y` that is an open immersion, then the underlying continuous map of `f` is an open embedding. In the context of algebraic geometry, this basically means that the morphism `f` maps open sets to open sets in a homeomorphic way, preserving the topological structure.
More concisely: Given any category `C`, if `f: X �� /******/ Y` is a morphism of presheafed spaces over `C` that is an open immersion, then the underlying continuous map `\overline{f}: \underline{X} \rightarrow \underline{Y}` is an open embedding.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
{f : X ⟶ Y} [self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
CategoryTheory.IsIso (f.c.app (Opposite.op (⋯.functor.obj U)))
This theorem states that for any Category `C` and two Algebraic Geometry Presheafed Spaces `X` and `Y` within this category, given a morphism `f` from `X` to `Y`, if `f` is an open immersion, then the underlying sheaf morphism induced by `f` is an isomorphism on each open subset `U` of the space `X`. This is expressed by stating that for each `U`, the application of the morphism `f.c` to the opposite of the object `U` in the Category is an isomorphism. Here, `Opposite.op` is a function that creates the opposite object of a given object in a certain category, and `f.c.app` refers to the application of the morphism `f.c`.
More concisely: Given any open immersion $f: X \to Y$ of Algebraic Geometry Presheafed Spaces in a Category $C$, the induced sheaf morphism $f.c$ is an isomorphism on each open subset $U$ of $X$.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace :
∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y)
[inst : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f.val = X
The theorem `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace` states that for any two LocallyRingedSpaces `X` and `Y`, and a morphism `f` from `X` to `Y`, if `f` is an open immersion of LocallyRingedSpaces (as defined by `AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion`), then the result of applying the function `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace` to `Y` and the underlying morphism of `f` (i.e., `f.val`) yields `X`. In other words, if an open immersion from `X` to `Y` exists, then transforming `Y` via this open immersion results in `X`.
More concisely: If `f: X -> Y` is an open immersion of Locally Ringed Spaces, then `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f.val = X`.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C}
(f : X ⟶ Z) [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
(H : Set.range ⇑g.base ⊆ Set.range ⇑f.base),
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H) f = g
This theorem, `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac`, states that for any category `C`, any presheafed spaces `X`, `Y`, and `Z` over `C`, a morphism `f` from `X` to `Z`, where `f` is an open immersion, and a morphism `g` from `Y` to `Z`, given that the image of the base of `g` is a subset of the image of the base of `f`, the composition of the lift of `g` along `f` and `f` is `g`.
In simpler terms, the theorem states that if you have two maps where one (`f`) is an open immersion and the image of the other (`g`) is contained within the image of the first, then you can "lift" the second map along the first so that they compose to give the second map again. This is a fundamental property in the theory of algebraic geometry.
More concisely: Given presheafed spaces X, Y, Z over a category C, an open immersion f : X -> Z, and a morphism g : Y -> Z with image(base g) subset image(base f), the lift of g along f and f equals g.
|
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso
theorem AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasLimits C]
[inst_2 : CategoryTheory.Limits.HasColimits C] [inst_3 : CategoryTheory.ConcreteCategory C]
[inst_4 : (CategoryTheory.forget C).ReflectsIsomorphisms]
[inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)]
[inst_6 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
{X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y),
OpenEmbedding ⇑f.base →
∀ [H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.stalkMap f x)],
AlgebraicGeometry.SheafedSpace.IsOpenImmersion f
This theorem is about sheafed spaces in the context of a concrete category `C`. Suppose `X` and `Y` are sheafed spaces in this category, and `C` has special properties: it has limits and colimits, its forgetful functor reflects isomorphisms, and preserves limits and filtered colimits. Then, if a morphism `f` from `X` to `Y` is a topological open embedding, it will be an open immersion if and only if every stalk map induced by `f` is an isomorphism. Stalk maps are maps between the stalks of the sheaves at corresponding points, and an isomorphism of stalk maps implies that the morphism `f` is locally an isomorphism in the category `C`. Being an open immersion means that `f` is a monomorphism in the category of sheafed spaces and the underlying continuous map is an open embedding.
More concisely: A topological open embedding between sheafed spaces in a category with preserving and reflecting isomorphisms for limits and colimits is an open immersion if and only if all induced stalk maps are isomorphisms.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
{f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f) (U : TopologicalSpace.Opens ↑↑Y)
(hU : ↑U ⊆ Set.range ⇑f.base),
CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
(H.invApp ((TopologicalSpace.Opens.map f.base).obj U)) =
Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
The theorem `AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'` states that for any category `C`, presheafed spaces `X` and `Y` in `C`, a morphism `f` from `X` to `Y` that is an open immersion, and an open set `U` of the underlying topological space of `Y` such that `U` is a subset of the range of the base of `f`, the composition of the application of the structure morphism of `f` to the opposite of `U` and the inverse application of `H` to the object in the functor from open sets in `Y` to open sets in `X` (given by taking preimages under the base of `f`) that corresponds to `U`, is equal to the application of the presheaf of `Y` to the morphism from `X` to `Y` given by an equality, where the equality is suppressed for brevity.
More concisely: For any presheafed spaces $X$ and $Y$ in a category $C$, an open immersion $f : X \to Y$, and an open set $U \subseteq Y$, the composition of $f$ with the inverse image functor and the restriction of the structure morphism of $f$ to the complement of $U$ equals the restriction of the presheaf of $Y$ to $f$.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp.proof_1
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
{f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f) (U : TopologicalSpace.Opens ↑↑X),
Opposite.op U = Opposite.op ((TopologicalSpace.Opens.map f.base).obj (Opposite.op (H.openFunctor.obj U)).unop)
This theorem states that for any category 'C', presheaved spaces 'X' and 'Y' over 'C', and morphism 'f' from 'X' to 'Y' which is an open immersion, and for any open set 'U' in the topological space underlying 'X', the opposite of 'U' is equal to the opposite of the object obtained by first applying the functor associated with the open immersion to 'U', then applying the preimage functor associated with 'f' to the result, and finally taking the underlying set of the result. This essentially asserts a certain commutativity property for the process of taking preimages of open sets under open immersions in the category of presheaved spaces.
More concisely: For any open immersion $f : X \to Y$ between presheaves over a category $C$, and any open set $U$ in the underlying topological space of $X$, we have $U^op = (f(U))^op \cap X^op$, where $A^op$ denotes the opposite of an object $A$.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
{f : X ⟶ Y} (H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f),
CategoryTheory.CategoryStruct.comp H.isoRestrict.hom (Y.ofRestrict ⋯) = f
This theorem states that for any two presheafed spaces `X` and `Y` in a category `C` with a morphism `f : X ⟶ Y` which is an open immersion, the composition of the homomorphism of the isoRestrict of `f` and the map from the restriction of the presheafed space `Y` is equal to `f`. In other words, we can recover the original morphism `f` by applying the isoRestrict operation to `f`, then composing with the restriction of `Y`. This reflects the notion that the process of restriction and then composing with the isoRestrict homomorphism is essentially an identity operation for open immersions in algebraic geometry.
More concisely: For any open immersion of presheafed spaces $f : X \to Y$ in a category $C$, the composition of $f$ with the restriction map of $Y$ is equal to the isoRestrict homomorphism of $f$.
|
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso
theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
(f : X ⟶ Y) [h : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] [h' : CategoryTheory.Epi f.base],
CategoryTheory.IsIso f
This theorem states that in the context of algebraic geometry, for a given category `C` and for two pre-sheafed spaces `X` and `Y` in that category, if we have a morphism `f` from `X` to `Y` that is an open immersion, and if the underlying continuous map of the morphism `f` is an epimorphism (surjection), then `f` is an isomorphism. This theorem essentially relates the concepts of open immersion, epimorphism, and isomorphism in the domain of algebraic geometry.
More concisely: In algebraic geometry, if a morphism between pre-sheafed spaces is both an open immersion and an epimorphism, then it is an isomorphism.
|