Comparing open-immersion restriction with slice-site restriction

For an open immersion f : X ⟶ Y, the open-set site of X is equivalent to the slice of the open-set site of Y over the range of f. This file constructs that equivalence and lifts it to an equivalence of the corresponding categories of sheaves of modules.

def AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.Over (opensRange f) ≌ X.Opens

The open-set site of the source of an open immersion is equivalent to the slice of the open-set site of the target over the range of the immersion.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.coe_opensRangeEquivalence_functor_obj {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (X✝ : CategoryTheory.Over (opensRange f)) : ↑((opensRangeEquivalence f).functor.obj X✝) = ⇑f ⁻¹' ↑X✝.left

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_inverse_obj_right_as {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) : ((opensRangeEquivalence f).inverse.obj U).right.as = PUnit.unit

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_unitIso_hom_app_left {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (X✝ : CategoryTheory.Over (opensRange f)) : ((opensRangeEquivalence f).unitIso.hom.app X✝).left = CategoryTheory.eqToHom ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.coe_opensRangeEquivalence_inverse_obj_left {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) : ↑((opensRangeEquivalence f).inverse.obj U).left = ⇑(CategoryTheory.ConcreteCategory.hom (toLRSHom f).base) '' ↑U

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_counitIso_inv_app {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (X✝ : X.Opens) : (opensRangeEquivalence f).counitIso.inv.app X✝ = CategoryTheory.eqToHom ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_counitIso_hom_app {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (X✝ : X.Opens) : (opensRangeEquivalence f).counitIso.hom.app X✝ = CategoryTheory.eqToHom ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_unitIso_inv_app_left {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (X✝ : CategoryTheory.Over (opensRange f)) : ((opensRangeEquivalence f).unitIso.inv.app X✝).left = CategoryTheory.eqToHom ⋯

instance AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_functor_isContinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (opensRangeEquivalence f).functor.IsContinuous ((Opens.grothendieckTopology ↥Y).over (opensRange f)) (Opens.grothendieckTopology ↥X)

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_functor_coverPreserving {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.CoverPreserving ((Opens.grothendieckTopology ↥Y).over (opensRange f)) (Opens.grothendieckTopology ↥X) (opensRangeEquivalence f).functor

theorem AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_inverse_coverPreserving {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.CoverPreserving (Opens.grothendieckTopology ↥X) ((Opens.grothendieckTopology ↥Y).over (opensRange f)) (opensRangeEquivalence f).inverse

instance AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_functor_isCocontinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (opensRangeEquivalence f).functor.IsCocontinuous ((Opens.grothendieckTopology ↥Y).over (opensRange f)) (Opens.grothendieckTopology ↥X)

instance AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_inverse_isCocontinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (opensRangeEquivalence f).inverse.IsCocontinuous (Opens.grothendieckTopology ↥X) ((Opens.grothendieckTopology ↥Y).over (opensRange f))

instance AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence_inverse_isContinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (opensRangeEquivalence f).inverse.IsContinuous (Opens.grothendieckTopology ↥X) ((Opens.grothendieckTopology ↥Y).over (opensRange f))

def AlgebraicGeometry.Scheme.Hom.opensRangeOverEquivalence {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : CategoryTheory.Over W ≌ CategoryTheory.Over ((opensRangeEquivalence f).functor.obj W)

The equivalence on slice categories induced by opensRangeEquivalence.

Equations

• AlgebraicGeometry.Scheme.Hom.opensRangeOverEquivalence f W = CategoryTheory.Over.postEquiv W (AlgebraicGeometry.Scheme.Hom.opensRangeEquivalence f)

instance AlgebraicGeometry.Scheme.Hom.opensRangeOverEquivalence_functor_isCocontinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverEquivalence f W).functor.IsCocontinuous (((Opens.grothendieckTopology ↥Y).over (opensRange f)).over W) ((Opens.grothendieckTopology ↥X).over ((opensRangeEquivalence f).functor.obj W))

instance AlgebraicGeometry.Scheme.Hom.opensRangeOverEquivalence_inverse_isCocontinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverEquivalence f W).inverse.IsCocontinuous ((Opens.grothendieckTopology ↥X).over ((opensRangeEquivalence f).functor.obj W)) (((Opens.grothendieckTopology ↥Y).over (opensRange f)).over W)

instance AlgebraicGeometry.Scheme.Hom.opensRangeOverEquivalence_functor_isContinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverEquivalence f W).functor.IsContinuous (((Opens.grothendieckTopology ↥Y).over (opensRange f)).over W) ((Opens.grothendieckTopology ↥X).over ((opensRangeEquivalence f).functor.obj W))

instance AlgebraicGeometry.Scheme.Hom.opensRangeOverEquivalence_inverse_isContinuous {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverEquivalence f W).inverse.IsContinuous ((Opens.grothendieckTopology ↥X).over ((opensRangeEquivalence f).functor.obj W)) (((Opens.grothendieckTopology ↥Y).over (opensRange f)).over W)

def AlgebraicGeometry.Scheme.Hom.overOverRingCatSheafHom {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f)).over W ⟶ ((opensRangeOverEquivalence f W).functor.sheafPushforwardContinuous RingCat (((Opens.grothendieckTopology ↥Y).over (opensRange f)).over W) ((Opens.grothendieckTopology ↥X).over ((opensRangeEquivalence f).functor.obj W))).obj (CategoryTheory.Sheaf.over X.ringCatSheaf ((opensRangeEquivalence f).functor.obj W))

The structure-sheaf morphism on the slice over W induced by an open immersion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.ringCatSheafOverToPushforwardOverOver {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : CategoryTheory.Sheaf.over X.ringCatSheaf ((opensRangeEquivalence f).functor.obj W) ⟶ ((opensRangeOverEquivalence f W).inverse.sheafPushforwardContinuous RingCat ((Opens.grothendieckTopology ↥X).over ((opensRangeEquivalence f).functor.obj W)) (((Opens.grothendieckTopology ↥Y).over (opensRange f)).over W)).obj ((CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f)).over W)

The inverse structure-sheaf morphism on the slice over W.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.opensRangeOverModulesEquivalence {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf ((opensRangeEquivalence f).functor.obj W)) ≌ SheafOfModules ((CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f)).over W)

The module equivalence induced on the slice over W.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.opensRangeOverModulesEquivalenceInverseUnitIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverModulesEquivalence f W).inverse.obj (SheafOfModules.unit ((CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f)).over W)) ≅ SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf ((opensRangeEquivalence f).functor.obj W))

The inverse slice equivalence sends the unit module to the unit module.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.opensRangeOverModulesEquivalenceUnitIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverModulesEquivalence f W).functor.obj (SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf ((opensRangeEquivalence f).functor.obj W))) ≅ SheafOfModules.unit ((CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f)).over W)

The forward slice equivalence sends the unit module to the unit module.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.restrictOverIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverModulesEquivalence f W).inverse.obj ((SheafOfModules.over M (opensRange f)).over W) ≅ SheafOfModules.over (M.restrict f) ((opensRangeEquivalence f).functor.obj W)

Restricting twice and transporting across the slice equivalence agrees with restricting the scheme-level module and then restricting to an object of its open-set site.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.restrictOverIsoForward {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (W : CategoryTheory.Over (opensRange f)) : (opensRangeOverModulesEquivalence f W).functor.obj (SheafOfModules.over (M.restrict f) ((opensRangeEquivalence f).functor.obj W)) ≅ (SheafOfModules.over M (opensRange f)).over W

The forward slice equivalence carries a restriction of the scheme-level restriction back to the corresponding iterated slice restriction on the target.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.Hom.overRingCatSheafHom {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f) ⟶ ((opensRangeEquivalence f).functor.sheafPushforwardContinuous RingCat ((Opens.grothendieckTopology ↥Y).over (opensRange f)) (Opens.grothendieckTopology ↥X)).obj X.ringCatSheaf

The morphism from the restriction of the target's structure sheaf to the structure sheaf of the source, viewed on the equivalent slice site.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.ringCatSheafToPushforwardOver {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : X.ringCatSheaf ⟶ ((opensRangeEquivalence f).inverse.sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X) ((Opens.grothendieckTopology ↥Y).over (opensRange f))).obj (CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f))

The inverse structure-sheaf morphism, whose components are the inverse maps on sections induced by the open immersion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.opensRangeModulesEquivalence {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : X.Modules ≌ SheafOfModules (CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f))

The equivalence between modules on the source of an open immersion and modules on the slice site over its range.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.opensRangeModulesEquivalenceInverseUnitIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (opensRangeModulesEquivalence f).inverse.obj (SheafOfModules.unit (CategoryTheory.Sheaf.over Y.ringCatSheaf (opensRange f))) ≅ SheafOfModules.unit X.ringCatSheaf

The inverse open-immersion equivalence sends the unit module on the range slice to the unit module on the source.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.restrictPresentation {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (P : (SheafOfModules.over M (opensRange f)).Presentation) : SheafOfModules.Presentation (M.restrict f)

A presentation on the range slice of an open immersion transports to a presentation of the scheme-level restriction on its source.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.restrictFunctorIsoOver {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (SheafOfModules.overFunctor Y.ringCatSheaf (opensRange f)).comp (opensRangeModulesEquivalence f).inverse ≅ Modules.restrictFunctor f

Restriction to the slice over the range, transported back across opensRangeModulesEquivalence, agrees with scheme-level restriction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.restrictQuasicoherentData {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (q : (SheafOfModules.over M (opensRange f)).QuasicoherentData) : SheafOfModules.QuasicoherentData (M.restrict f)

Transport local presentation data on the slice over the range of an open immersion to local presentation data for the scheme-level restriction.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Hom.restrictQuasicoherentData_isFinitePresentation {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (q : (SheafOfModules.over M (opensRange f)).QuasicoherentData) [q.IsFinitePresentation] : (restrictQuasicoherentData f M q).IsFinitePresentation

Transporting finite local presentation data from the range slice to the source preserves finiteness.

theorem AlgebraicGeometry.Scheme.Hom.isFinitePresentation_restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (hM : (SheafOfModules.over M (opensRange f)).IsFinitePresentation) : SheafOfModules.IsFinitePresentation (M.restrict f)

Finite presentation on the range slice implies finite presentation after scheme-level restriction along the open immersion.

The reverse transport

Everything above carries finite presentation from the range slice to the scheme-level restriction. This section supplies the other direction, so that finite presentation is invariant under the equivalence rather than merely transported one way.

One asymmetry drives the shape of what follows. The forward direction never round-trips: restrictOverIso is stated at f.opensRangeEquivalence.functor.obj W for a W taken straight from the quasicoherent data, so the object is already in the form it is needed in. The reverse direction must round-trip, because the data now lives on X.Opens and its cover has to be pulled back to Over f.opensRange.

That round trip is an equality of opens rather than merely an isomorphism — opensRangeEquivalence's counit is eqToIso (f.preimage_image_eq _) — which is what makes it tractable. It is discharged once, by subst, in presentationOverOfEq, rather than by a dependent rewrite at each use site: the ambient category of (M.restrict f).over U depends on U, so rewriting U after the fact means transporting across a change of category.

noncomputable def AlgebraicGeometry.Scheme.Hom.presentationOverOfEq {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (W : CategoryTheory.Over (opensRange f)) (U : X.Opens) (h : (opensRangeEquivalence f).functor.obj W = U) (P : (SheafOfModules.over (M.restrict f) U).Presentation) : ((SheafOfModules.over M (opensRange f)).over W).Presentation

Transport a presentation of the scheme-level restriction over U to a presentation of the range-slice restriction over W, given that W maps to U under the site equivalence.

The equality hypothesis is what lets subst do the dependent work in one place.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Hom.presentationOverOfEq_isFinite {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (W : CategoryTheory.Over (opensRange f)) (U : X.Opens) (h : (opensRangeEquivalence f).functor.obj W = U) (P : (SheafOfModules.over (M.restrict f) U).Presentation) [P.IsFinite] : (presentationOverOfEq f M W U h P).IsFinite

The transported presentation is finite when the original is: neither Presentation.map nor Presentation.ofIsIso touches the generator and relation index types.

noncomputable def AlgebraicGeometry.Scheme.Hom.overQuasicoherentData {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (q : SheafOfModules.QuasicoherentData (M.restrict f)) : (SheafOfModules.over M (opensRange f)).QuasicoherentData

Transport local presentation data for the scheme-level restriction back to local presentation data on the slice over the range.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.Hom.overQuasicoherentData_isFinitePresentation {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (q : SheafOfModules.QuasicoherentData (M.restrict f)) [hq : q.IsFinitePresentation] : (overQuasicoherentData f M q).IsFinitePresentation

Transporting finite local presentation data back to the range slice preserves finiteness.

theorem AlgebraicGeometry.Scheme.Hom.isFinitePresentation_over_of_restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (hM : SheafOfModules.IsFinitePresentation (M.restrict f)) : (SheafOfModules.over M (opensRange f)).IsFinitePresentation

Finite presentation after scheme-level restriction along an open immersion implies finite presentation on the range slice — the converse of isFinitePresentation_restrict.

theorem AlgebraicGeometry.Scheme.Hom.isFinitePresentation_over_iff_restrict {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) : (SheafOfModules.over M (opensRange f)).IsFinitePresentation ↔ SheafOfModules.IsFinitePresentation (M.restrict f)

Finite presentation is invariant under the open-immersion/slice equivalence.

This is the statement downstream work should quote; the two one-directional theorems remain available for when only one implication is wanted.

theorem AlgebraicGeometry.Scheme.Modules.restrict_smul_eq {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (M : Y.Modules) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑((M.restrict f).presheaf.obj (Opposite.op U))) : r • x = (have this := (CommRingCat.Hom.hom (Hom.appIso f U).inv) r; this) • have this := x; this

The restricted sheaf's scalar action is the original one, transported along appIso.

Scheme.Modules.restrictAppIso is Iso.refl, so both sides live in the same type and the statement is purely about which action is used.

This is rfl. by rfl proves the statement verbatim; the proof term below just reads it off Mathlib's form. So it is not a defeq barrier, and reaching for it is never forced — do not read this lemma as evidence that a restricted scalar action cannot be closed definitionally, because it can.

What it is for is shape. Mathlib's smul_restrictAppIso_hom_apply states the same fact with two restrictAppIso.hom applications wrapped around it; this states it bare, so that instantiating it as a have hands back an equation whose sides match a goal written in the obvious way. Proj.chartUnitToTwist_eq uses it exactly so — to move an equation from the restricted action to the original one, where the pointwise lemma about the original applies.

A caveat on how to use it, learned the hard way: rw with it will fail on a goal carrying show-ascription residue, which Lean reports as the goal being "not type-correct under the instances transparency level". That is a property of the goal, not of this lemma. Instantiate it at explicit arguments as a have and combine with Eq.trans.