From a884fb60c619a787b75aa17e6ca85d1f9a1ee469 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Fri, 15 May 2026 23:30:19 +0100 Subject: [PATCH 1/6] restriction lemmas --- Mathlib/AlgebraicGeometry/Restrict.lean | 55 +++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean index 4af3250749b579..baa36f5fc1e18d 100644 --- a/Mathlib/AlgebraicGeometry/Restrict.lean +++ b/Mathlib/AlgebraicGeometry/Restrict.lean @@ -380,6 +380,23 @@ lemma Scheme.Hom.isoImage_inv_ι (f.isoImage U).inv ≫ U.ι ≫ f = (f ''ᵁ U).ι := IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _ +@[reassoc] +lemma Scheme.Hom.isoImage_hom_homOfLE + {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U V : Opens X) (e : U ≤ V) : + (f.isoImage U).hom ≫ Y.homOfLE (f.image_mono e) = X.homOfLE e ≫ (f.isoImage V).hom := by + simp [← cancel_mono (f ''ᵁ V).ι] + +@[reassoc] +lemma Scheme.Hom.isoImage_inv_homOfLE + {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U V : Opens X) (e : U ≤ V) : + (f.isoImage U).inv ≫ X.homOfLE e = Y.homOfLE (f.image_mono e) ≫ (f.isoImage V).inv := by + simp [← cancel_mono (f.isoImage V).hom, ← f.isoImage_hom_homOfLE] + +@[reassoc (attr := simp)] +lemma Scheme.Opens.ι_isoImage_inv_ι {X : Scheme.{u}} (U : Opens X) (V : Opens U) : + (U.ι.isoImage V).inv ≫ V.ι = X.homOfLE (U.ι_image_le V) := by + simp [← cancel_mono U.ι] + /-- If `f : X ⟶ Y` is an open immersion, then `X` is isomorphic to its image in `Y`. -/ def Scheme.Hom.isoOpensRange {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] : X ≅ f.opensRange := @@ -577,6 +594,16 @@ theorem morphismRestrict_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) ( pullbackRestrictIsoRestrict_inv_fst_assoc] rfl +@[reassoc] +theorem morphismRestrict_homOfLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U V : Y.Opens) (e : U ≤ V) : + (f ∣_ U) ≫ Y.homOfLE e = X.homOfLE (f.preimage_mono e) ≫ (f ∣_ V) := by + simp [← cancel_mono V.ι] + +lemma morphismRestrict_eq_isoImage_hom_homOfLE {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] + (U : Y.Opens) : + f ∣_ U = (f.isoImage (f ⁻¹ᵁ U)).hom ≫ Y.homOfLE (f.image_preimage_le U) := by + simp [← cancel_mono U.ι] + instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] (U : Y.Opens) : IsIso (f ∣_ U) := by delta morphismRestrict; infer_instance @@ -622,6 +649,20 @@ theorem morphismRestrict_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map, Scheme.Hom.appLE_map] +@[reassoc] +theorem morphismRestrict_homOfLE_ι_isoImage_hom + {X : Scheme.{u}} {U V : X.Opens} (e : U ≤ V) (W : Opens V) : + X.homOfLE e ∣_ W ≫ (V.ι.isoImage W).hom = + (U.ι.isoImage (X.homOfLE e ⁻¹ᵁ W)).hom ≫ X.homOfLE (X.ι_image_homOfLE_le_ι_image e W) := by + simp [← cancel_mono (V.ι ''ᵁ W).ι] + +@[reassoc] +theorem ι_isoImage_inv_morphismRestrict_homOfLE {X : Scheme.{u}} {U V : X.Opens} + (e : U ≤ V) (W : Opens V) : + (U.ι.isoImage (X.homOfLE e ⁻¹ᵁ W)).inv ≫ X.homOfLE e ∣_ W = + X.homOfLE (X.ι_image_homOfLE_le_ι_image e W) ≫ (V.ι.isoImage W).inv := by + simp [← cancel_mono (V.ι.isoImage W).hom, morphismRestrict_homOfLE_ι_isoImage_hom] + set_option backward.isDefEq.respectTransparency false in /-- Restricting a morphism onto the image of an open immersion is isomorphic to the base change along the immersion. -/ @@ -659,6 +700,20 @@ def morphismRestrictRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : Scheme.Hom.isoImage_hom_ι, morphismRestrict_ι_assoc, morphismRestrict_ι] +@[reassoc] +lemma morphismRestrict_ι_image_ι_isoImage_inv + {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : + f ∣_ U.ι ''ᵁ V ≫ (U.ι.isoImage V).inv = (X.homOfLE (image_morphismRestrict_preimage f U V).ge ≫ + ((f ⁻¹ᵁ U).ι.isoImage ((f ∣_ U) ⁻¹ᵁ V)).inv) ≫ f ∣_ U ∣_ V := + (morphismRestrictRestrict f U V).inv.w' + +@[reassoc] +lemma morphismRestrict_morphismRestrict_ι_isoImage_hom + {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : + f ∣_ U ∣_ V ≫ (U.ι.isoImage V).hom = (((f ⁻¹ᵁ U).ι.isoImage ((f ∣_ U) ⁻¹ᵁ V)).hom ≫ + X.homOfLE (image_morphismRestrict_preimage f U V).le) ≫ f ∣_ U.ι ''ᵁ V := + (morphismRestrictRestrict f U V).hom.w' + set_option backward.isDefEq.respectTransparency false in /-- Restricting a morphism twice onto a basic open set is isomorphic to one restriction. -/ def morphismRestrictRestrictBasicOpen {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (r : Γ(Y, U)) : From 3343cbb836624783a2da24b3670feebd7f08528f Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Tue, 26 May 2026 11:48:32 +0100 Subject: [PATCH 2/6] Apply suggestion from @chrisflav Co-authored-by: Christian Merten --- Mathlib/AlgebraicGeometry/Restrict.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean index baa36f5fc1e18d..c61c396f3778b5 100644 --- a/Mathlib/AlgebraicGeometry/Restrict.lean +++ b/Mathlib/AlgebraicGeometry/Restrict.lean @@ -650,7 +650,7 @@ theorem morphismRestrict_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V Scheme.Hom.appLE_map] @[reassoc] -theorem morphismRestrict_homOfLE_ι_isoImage_hom +theorem morphismRestrict_homOfLE_isoImage_ι_hom {X : Scheme.{u}} {U V : X.Opens} (e : U ≤ V) (W : Opens V) : X.homOfLE e ∣_ W ≫ (V.ι.isoImage W).hom = (U.ι.isoImage (X.homOfLE e ⁻¹ᵁ W)).hom ≫ X.homOfLE (X.ι_image_homOfLE_le_ι_image e W) := by From a7b8053a59eab6c12154d01befb1f40e809a0c1f Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Tue, 26 May 2026 11:49:22 +0100 Subject: [PATCH 3/6] Apply suggestion from @chrisflav Co-authored-by: Christian Merten --- Mathlib/AlgebraicGeometry/Restrict.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean index c61c396f3778b5..f5873c87781df3 100644 --- a/Mathlib/AlgebraicGeometry/Restrict.lean +++ b/Mathlib/AlgebraicGeometry/Restrict.lean @@ -393,7 +393,7 @@ lemma Scheme.Hom.isoImage_inv_homOfLE simp [← cancel_mono (f.isoImage V).hom, ← f.isoImage_hom_homOfLE] @[reassoc (attr := simp)] -lemma Scheme.Opens.ι_isoImage_inv_ι {X : Scheme.{u}} (U : Opens X) (V : Opens U) : +lemma Scheme.Opens.isoImage_ι_inv_ι {X : Scheme.{u}} (U : Opens X) (V : Opens U) : (U.ι.isoImage V).inv ≫ V.ι = X.homOfLE (U.ι_image_le V) := by simp [← cancel_mono U.ι] From 700394a91f79ae435c03b5b6f11489bf3ea4825d Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Tue, 26 May 2026 11:55:56 +0100 Subject: [PATCH 4/6] Apply suggestion from @chrisflav Co-authored-by: Christian Merten --- Mathlib/AlgebraicGeometry/Restrict.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean index f5873c87781df3..2821109240be07 100644 --- a/Mathlib/AlgebraicGeometry/Restrict.lean +++ b/Mathlib/AlgebraicGeometry/Restrict.lean @@ -704,8 +704,8 @@ def morphismRestrictRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : lemma morphismRestrict_ι_image_ι_isoImage_inv {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : f ∣_ U.ι ''ᵁ V ≫ (U.ι.isoImage V).inv = (X.homOfLE (image_morphismRestrict_preimage f U V).ge ≫ - ((f ⁻¹ᵁ U).ι.isoImage ((f ∣_ U) ⁻¹ᵁ V)).inv) ≫ f ∣_ U ∣_ V := - (morphismRestrictRestrict f U V).inv.w' + ((f ⁻¹ᵁ U).ι.isoImage ((f ∣_ U) ⁻¹ᵁ V)).inv) ≫ f ∣_ U ∣_ V := by + simp [← cancel_mono (Scheme.Opens.ι _)] @[reassoc] lemma morphismRestrict_morphismRestrict_ι_isoImage_hom From 865d904260887078d4ecff1f8bba79b7db1921ce Mon Sep 17 00:00:00 2001 From: Justus Springer <50165510+justus-springer@users.noreply.github.com> Date: Tue, 26 May 2026 11:56:05 +0100 Subject: [PATCH 5/6] Apply suggestion from @chrisflav Co-authored-by: Christian Merten --- Mathlib/AlgebraicGeometry/Restrict.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean index 2821109240be07..db4f1eeaef7fdc 100644 --- a/Mathlib/AlgebraicGeometry/Restrict.lean +++ b/Mathlib/AlgebraicGeometry/Restrict.lean @@ -712,7 +712,7 @@ lemma morphismRestrict_morphismRestrict_ι_isoImage_hom {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : f ∣_ U ∣_ V ≫ (U.ι.isoImage V).hom = (((f ⁻¹ᵁ U).ι.isoImage ((f ∣_ U) ⁻¹ᵁ V)).hom ≫ X.homOfLE (image_morphismRestrict_preimage f U V).le) ≫ f ∣_ U.ι ''ᵁ V := - (morphismRestrictRestrict f U V).hom.w' + simp [← cancel_mono (Scheme.Opens.ι _)] set_option backward.isDefEq.respectTransparency false in /-- Restricting a morphism twice onto a basic open set is isomorphic to one restriction. -/ From 0cee355f5869a2e8482baa510501080cffcfa766 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Tue, 26 May 2026 12:10:47 +0100 Subject: [PATCH 6/6] review --- Mathlib/AlgebraicGeometry/Restrict.lean | 31 +++++++++++-------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean index db4f1eeaef7fdc..3bc18e27ad87b5 100644 --- a/Mathlib/AlgebraicGeometry/Restrict.lean +++ b/Mathlib/AlgebraicGeometry/Restrict.lean @@ -599,9 +599,10 @@ theorem morphismRestrict_homOfLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U V : Y.Opens (f ∣_ U) ≫ Y.homOfLE e = X.homOfLE (f.preimage_mono e) ≫ (f ∣_ V) := by simp [← cancel_mono V.ι] -lemma morphismRestrict_eq_isoImage_hom_homOfLE {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] +@[reassoc (attr := simp)] +lemma Scheme.Hom.isoImage_preimage_hom_homOfLE {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) : - f ∣_ U = (f.isoImage (f ⁻¹ᵁ U)).hom ≫ Y.homOfLE (f.image_preimage_le U) := by + (f.isoImage (f ⁻¹ᵁ U)).hom ≫ Y.homOfLE (f.image_preimage_le U) = f ∣_ U := by simp [← cancel_mono U.ι] instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f] (U : Y.Opens) : IsIso (f ∣_ U) := by @@ -657,11 +658,11 @@ theorem morphismRestrict_homOfLE_isoImage_ι_hom simp [← cancel_mono (V.ι ''ᵁ W).ι] @[reassoc] -theorem ι_isoImage_inv_morphismRestrict_homOfLE {X : Scheme.{u}} {U V : X.Opens} +theorem isoImage_ι_inv_morphismRestrict_homOfLE {X : Scheme.{u}} {U V : X.Opens} (e : U ≤ V) (W : Opens V) : (U.ι.isoImage (X.homOfLE e ⁻¹ᵁ W)).inv ≫ X.homOfLE e ∣_ W = X.homOfLE (X.ι_image_homOfLE_le_ι_image e W) ≫ (V.ι.isoImage W).inv := by - simp [← cancel_mono (V.ι.isoImage W).hom, morphismRestrict_homOfLE_ι_isoImage_hom] + simp [← cancel_mono (V.ι.isoImage W).hom, morphismRestrict_homOfLE_isoImage_ι_hom] set_option backward.isDefEq.respectTransparency false in /-- Restricting a morphism onto the image of an open immersion is isomorphic to the base change @@ -688,18 +689,6 @@ def morphismRestrictEq {X Y : Scheme.{u}} (f : X ⟶ Y) {U V : Y.Opens} (e : U = Arrow.mk (f ∣_ U) ≅ Arrow.mk (f ∣_ V) := eqToIso (by subst e; rfl) -/-- Restricting a morphism twice is isomorphic to one restriction. -/ -def morphismRestrictRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : - Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (f ∣_ U.ι ''ᵁ V) := by - refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_) - ((Scheme.Opens.ι _).isoImage _) ?_ - · exact image_morphismRestrict_preimage f U V - · rw [← cancel_mono (Scheme.Opens.ι _), Iso.trans_hom, Category.assoc, Category.assoc, - Category.assoc, morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc, - Scheme.Hom.isoImage_hom_ι_assoc, - Scheme.Hom.isoImage_hom_ι, - morphismRestrict_ι_assoc, morphismRestrict_ι] - @[reassoc] lemma morphismRestrict_ι_image_ι_isoImage_inv {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : @@ -711,9 +700,17 @@ lemma morphismRestrict_ι_image_ι_isoImage_inv lemma morphismRestrict_morphismRestrict_ι_isoImage_hom {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : f ∣_ U ∣_ V ≫ (U.ι.isoImage V).hom = (((f ⁻¹ᵁ U).ι.isoImage ((f ∣_ U) ⁻¹ᵁ V)).hom ≫ - X.homOfLE (image_morphismRestrict_preimage f U V).le) ≫ f ∣_ U.ι ''ᵁ V := + X.homOfLE (image_morphismRestrict_preimage f U V).le) ≫ f ∣_ U.ι ''ᵁ V := by simp [← cancel_mono (Scheme.Opens.ι _)] +/-- Restricting a morphism twice is isomorphic to one restriction. -/ +def morphismRestrictRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : + Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (f ∣_ U.ι ''ᵁ V) := by + refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_) + ((Scheme.Opens.ι _).isoImage _) ?_ + · exact image_morphismRestrict_preimage f U V + · simp [← cancel_mono (Scheme.Opens.ι _)] + set_option backward.isDefEq.respectTransparency false in /-- Restricting a morphism twice onto a basic open set is isomorphic to one restriction. -/ def morphismRestrictRestrictBasicOpen {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (r : Γ(Y, U)) :