Restricting local properties of scheme morphisms

For a morphism of schemes f : X ⟶ Y and an open U of Y, Mathlib's f ∣_ U is the restriction f ⁻¹ᵁ U ⟶ U. A property local on the target passes from this restriction to every smaller open. An open immersion restricts to an isomorphism over opens in its range. Restricting the source to an open equal to the full preimage gives a pullback square, which transfers properties stable under base change to Scheme.Hom.resLE. Between affine opens, a property attached to a ring-hom property holds for Scheme.Hom.resLE iff the ring-hom property holds for Scheme.Hom.appLE. Dually, in a pullback square of the inclusion of an open U along f, pullback of functions along the top morphism identifies the functions on f ⁻¹ᵁ U with the global functions of the base change.

Main results

• AlgebraicGeometry.IsZariskiLocalAtTarget.restrict_of_le: a property local on the target passes from f ∣_ U to f ∣_ V when V ≤ U.
• AlgebraicGeometry.Scheme.Hom.isIso_morphismRestrict_of_le_opensRange: an open immersion restricts to an isomorphism over every open contained in its range.
• AlgebraicGeometry.Scheme.Hom.isPullback_resLE_of_eq: the restriction of f to an open U of the target and an open V of the source equal to f ⁻¹ᵁ U is a pullback of f.
• AlgebraicGeometry.Scheme.Hom.isIso_morphismRestrict_of_isIso_comp: if an open immersion ι contains f ⁻¹ᵁ V in its range and (ι ≫ f) ∣_ V is an isomorphism, so is f ∣_ V.
• AlgebraicGeometry.HasRingHomProperty.resLE_iff: for affine opens V ⊆ f ⁻¹ᵁ U, a property attached to a ring-hom property Q holds for f.resLE U V iff Q holds for f.appLE U V.
• AlgebraicGeometry.Scheme.Hom.congr_appLE: equal morphisms induce the same maps Γ(Y, U) ⟶ Γ(X, V), whatever the proofs of V ≤ f ⁻¹ᵁ U.
• CategoryTheory.CommSq.appLE_app_topIso_hom: in a commutative square over the inclusion of an open U, the two ways of pulling a function on U back to the source of the square agree.
• CategoryTheory.IsPullback.isIso_appLE: in a pullback square of the inclusion of an open U along f, pullback along the top morphism identifies the functions on f ⁻¹ᵁ U with the global functions of the base change.

theorem AlgebraicGeometry.IsZariskiLocalAtTarget.restrict_of_le {X Y : Scheme} (P : CategoryTheory.MorphismProperty Scheme) [IsZariskiLocalAtTarget P] {f : X ⟶ Y} {U V : Y.Opens} (h : P (f ∣_ U)) (hVU : V ≤ U) : P (f ∣_ V)

A property local on the target passes from the restriction over U to the restriction over every open V ≤ U.

theorem AlgebraicGeometry.Scheme.Hom.isIso_morphismRestrict_of_le_opensRange {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] {V : Y.Opens} (hV : V ≤ opensRange f) : CategoryTheory.IsIso (f ∣_ V)

An open immersion f restricts to an isomorphism over every open V contained in its range.

theorem AlgebraicGeometry.Scheme.Hom.isPullback_resLE_of_eq {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) {V : X.Opens} (h : V = (TopologicalSpace.Opens.map f.base).obj U) : CategoryTheory.IsPullback (resLE f U V ⋯) V.ι U.ι f

Restricting f over an open U of the target, with source the open V = f ⁻¹ᵁ U (up to a propositional equality), gives a pullback of f along the inclusion of U.

theorem AlgebraicGeometry.Scheme.Hom.isIso_morphismRestrict_of_isIso_comp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (ι : Z ⟶ X) [IsOpenImmersion ι] {V : Y.Opens} (hV : (TopologicalSpace.Opens.map f.base).obj V ≤ opensRange ι) (h : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp ι f ∣_ V)) : CategoryTheory.IsIso (f ∣_ V)

If the range of an open immersion ι contains f ⁻¹ᵁ V and (ι ≫ f) ∣_ V is an isomorphism, then so is f ∣_ V: over V, the morphism f is ι ≫ f up to an isomorphism.

theorem AlgebraicGeometry.HasRingHomProperty.resLE_iff {X Y : Scheme} (P : CategoryTheory.MorphismProperty Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] => Q] {f : X ⟶ Y} {U : Y.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : P (Scheme.Hom.resLE f U V hVU) ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU))

Let V ⊆ f⁻¹ U with U and V affine, and let P be a morphism property attached to the ring-hom property Q. Then P holds for the restriction V ⟶ U of f iff Q holds for f.appLE U V : Γ(Y, U) ⟶ Γ(X, V).

theorem AlgebraicGeometry.Scheme.Hom.congr_appLE {X Y : Scheme} (f : X ⟶ Y) {g : X ⟶ Y} (e : f = g) (U : Y.Opens) (V : X.Opens) (hf : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hg : V ≤ (TopologicalSpace.Opens.map g.base).obj U) : appLE f U V hf = appLE g U V hg

Equal morphisms induce the same maps on sections Γ(Y, U) ⟶ Γ(X, V). Unlike rewriting along f = g, this applies when the proofs of V ≤ f ⁻¹ᵁ U and of V ≤ g ⁻¹ᵁ U are unrelated.

theorem CategoryTheory.CommSq.top_le_preimage_preimage {Z Y T : AlgebraicGeometry.Scheme} {U : T.Opens} {j : Z ⟶ Y} {g : Z ⟶ ↑U} {f : Y ⟶ T} (h : CommSq j g f U.ι) : ⊤ ≤ (TopologicalSpace.Opens.map j.base).obj ((TopologicalSpace.Opens.map f.base).obj U)

In a commutative square over the inclusion of an open U, the top morphism j maps all of its source into f ⁻¹ᵁ U.

theorem CategoryTheory.CommSq.appLE_app_topIso_hom {Z Y T : AlgebraicGeometry.Scheme} {U : T.Opens} {j : Z ⟶ Y} {g : Z ⟶ ↑U} {f : Y ⟶ T} (h : CommSq j g f U.ι) (r : ↑((↑U).presheaf.obj (Opposite.op ⊤))) : (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE j ((TopologicalSpace.Opens.map f.base).obj U) ⊤ ⋯)) ((ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) ((ConcreteCategory.hom U.topIso.hom) r)) = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop g)) r

In a commutative square over the inclusion of an open U, pulling a function on U back to the source along g is pulling it back along f to f ⁻¹ᵁ U and then along j.

theorem CategoryTheory.IsPullback.isIso_appLE {Z Y T : AlgebraicGeometry.Scheme} {U : T.Opens} {j : Z ⟶ Y} {g : Z ⟶ ↑U} {f : Y ⟶ T} (h : IsPullback j g f U.ι) : IsIso (AlgebraicGeometry.Scheme.Hom.appLE j ((TopologicalSpace.Opens.map f.base).obj U) ⊤ ⋯)

In a pullback square of the inclusion of an open U along f, pullback of functions along the top morphism j is an isomorphism Γ(Y, f ⁻¹ᵁ U) ≅ Γ(Z, ⊤).