Restriction of Schemes and Morphisms #
Main definition #
AlgebraicGeometry.Scheme.restrict
: The restriction of a scheme along an open embedding. The mapX.restrict f ⟶ X
isAlgebraicGeometry.Scheme.ofRestrict
.U : X.Opens
has a coercion toScheme
andU.ι
is a shorthand forX.restrict U.open_embedding : U ⟶ X
.AlgebraicGeometry.morphism_restrict
: The restriction ofX ⟶ Y
toX ∣_ᵤ f ⁻¹ᵁ U ⟶ Y ∣_ᵤ U
.
Open subset of a scheme as a scheme.
Equations
- ↑U = X.restrict ⋯
Instances For
Equations
- AlgebraicGeometry.Scheme.Opens.instCoeOut = { coe := AlgebraicGeometry.Scheme.Opens.toScheme }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The global sections of the restriction is isomorphic to the sections on the open set.
Equations
- U.topIso = CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).op
Instances For
The stalks of an open subscheme are isomorphic to the stalks of the original scheme.
Equations
- U.stalkIso x = X.restrictStalkIso ⋯ x
Instances For
If U
is a family of open sets that covers X
, then X.restrict U
forms an X.open_cover
.
Equations
- X.openCoverOfISupEqTop U hU = { J := s, obj := fun (i : s) => ↑(U i), map := fun (i : s) => (U i).ι, f := fun (x : ↑↑X.toPresheafedSpace) => ⋯.choose, covers := ⋯, IsOpen := ⋯ }
Instances For
Alias of AlgebraicGeometry.Scheme.openCoverOfISupEqTop
.
If U
is a family of open sets that covers X
, then X.restrict U
forms an X.open_cover
.
Equations
Instances For
The open sets of an open subscheme corresponds to the open sets containing in the subset.
Equations
Instances For
The functor taking open subsets of X
to open subschemes of X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is not a simp
lemma, as (X.restricFunctor.map i).left
is used as the simp
normal-form for the induced morphism U.toScheme ⟶ V.toScheme
.
The functor that restricts to open subschemes and then takes global section is isomorphic to the structure sheaf.
Equations
- AlgebraicGeometry.Scheme.restrictFunctorΓ = CategoryTheory.NatIso.ofComponents (fun (U : X.Opensᵒᵖ) => CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).symm.op) ⋯
Instances For
X ∣_ U ∣_ V
is isomorphic to X ∣_ V ∣_ U
Equations
- One or more equations did not get rendered due to their size.
Instances For
If V
is an open subset of U
, then X ∣_ U ∣_ V
is isomorphic to X ∣_ V
.
Equations
- X.restrictRestrict U V = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (CategoryTheory.CategoryStruct.comp V.ι U.ι) ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V).ι ⋯
Instances For
If U = V
, then X ∣_ U
is isomorphic to X ∣_ V
.
Equations
- X.restrictIsoOfEq e = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq U.ι V.ι ⋯
Instances For
The restriction of an isomorphism onto an open set.
Equations
- AlgebraicGeometry.Scheme.restrictMapIso f U = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.val.base).obj U).ι f) U.ι ⋯
Instances For
Given a morphism f : X ⟶ Y
and an open set U ⊆ Y
, we have X ×[Y] U ≅ X |_{f ⁻¹ U}
Equations
- AlgebraicGeometry.pullbackRestrictIsoRestrict f U = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq (CategoryTheory.Limits.pullback.fst f U.ι) ((TopologicalSpace.Opens.map f.val.base).obj U).ι ⋯
Instances For
The restriction of a morphism X ⟶ Y
onto X |_{f ⁻¹ U} ⟶ Y |_ U
.
Equations
Instances For
the notation for restricting a morphism of scheme to an open subset of the target scheme
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Restricting a morphism onto the image of an open immersion is isomorphic to the base change along the immersion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restrictions onto two equal open sets are isomorphic. This currently has bad defeqs when unfolded, but it should not matter for now. Replace this definition if better defeqs are needed.
Equations
Instances For
Restricting a morphism twice is isomorphic to one restriction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restricting a morphism twice onto a basic open set is isomorphic to one restriction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stalk map of a restriction of a morphism is isomorphic to the stalk map of the original map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The restriction of a morphism f : X ⟶ Y
to open sets on the source and target.
Equations
- f.resLE U V e = CategoryTheory.CategoryStruct.comp (X.restrictFunctor.map (CategoryTheory.homOfLE e)).left (f ∣_ U)
Instances For
f.resLE U V
induces f.appLE U V
on global sections.
Equations
- AlgebraicGeometry.arrowResLEAppIso f U V e = CategoryTheory.Arrow.isoMk U.topIso V.topIso ⋯
Instances For
The restriction of an open cover to an open subset.
Equations
- One or more equations did not get rendered due to their size.