feat(Geometry/RingedSpace/OpenImmersion): make IsOpenImmersion inst…

…ance (#14050)

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -407,8 +407,8 @@ theorem exists_basicOpen_le {V : Opens X} (x : V) (h : ↑x ∈ U) :
     refine (Scheme.image_basicOpen (X.ofRestrict U.openEmbedding) r).trans ?_
     rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.openEmbedding_obj_top).op,
       ← comp_apply, ← CategoryTheory.Functor.map_comp, ← op_comp, eqToHom_trans, eqToHom_refl,
-      op_id, CategoryTheory.Functor.map_id, Scheme.Hom.invApp,
-      PresheafedSpace.IsOpenImmersion.ofRestrict_invApp]
+      op_id, CategoryTheory.Functor.map_id, Scheme.Hom.invApp]
+    erw [PresheafedSpace.IsOpenImmersion.ofRestrict_invApp]
     congr
   use X.presheaf.map (eqToHom U.openEmbedding_obj_top.symm).op r
   rw [← this]

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -263,8 +263,7 @@ def OpenCover.inter {X : Scheme.{u}} (𝒰₁ : Scheme.OpenCover.{v₁} X)
   Covers x := by
     rw [IsOpenImmersion.range_pullback_to_base_of_left]
     exact ⟨𝒰₁.Covers x, 𝒰₂.Covers x⟩
-  -- Porting note: was automatic
-  IsOpen x := PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := (𝒰₁.IsOpen _))
+  IsOpen x := inferInstance
 #align algebraic_geometry.Scheme.open_cover.inter AlgebraicGeometry.Scheme.OpenCover.inter
 
 /-- If `U` is a family of open sets that covers `X`, then `X.restrict U` forms an `X.open_cover`. -/

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -216,9 +216,7 @@ end
 /-- The restriction of an isomorphism onto an open set. -/
 noncomputable abbrev Scheme.restrictMapIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIso f]
     (U : Opens Y) : X ∣_ᵤ f ⁻¹ᵁ U ≅ Y ∣_ᵤ U := by
-  apply IsOpenImmersion.isoOfRangeEq (f := X.ofRestrict _ ≫ f)
-    (H := PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := inferInstance))
-    (Y.ofRestrict _) _
+  apply IsOpenImmersion.isoOfRangeEq (f := X.ofRestrict _ ≫ f) (Y.ofRestrict _) _
   dsimp [restrict]
   rw [Set.range_comp, Subtype.range_val, Subtype.range_coe]
   refine @Set.image_preimage_eq _ _ f.1.base U.1 ?_

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -100,7 +100,7 @@ attribute [instance] IsOpenImmersion.c_iso
 
 section
 
-variable {X Y : PresheafedSpace C} {f : X ⟶ Y} (H : IsOpenImmersion f)
+variable {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : IsOpenImmersion f]
 
 /-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`. -/
 abbrev openFunctor :=
@@ -114,7 +114,7 @@ noncomputable def isoRestrict : X ≅ Y.restrict H.base_open :=
     symm
     fapply NatIso.ofComponents
     · intro U
-      refine asIso (f.c.app (op (H.openFunctor.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)
+      refine asIso (f.c.app (op (openFunctor f |>.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)
       induction U using Opposite.rec' with | h U => ?_
       cases U
       dsimp only [IsOpenMap.functor, Functor.op, Opens.map]
@@ -129,7 +129,7 @@ noncomputable def isoRestrict : X ≅ Y.restrict H.base_open :=
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict
 
 @[simp]
-theorem isoRestrict_hom_ofRestrict : H.isoRestrict.hom ≫ Y.ofRestrict _ = f := by
+theorem isoRestrict_hom_ofRestrict : (isoRestrict f).hom ≫ Y.ofRestrict _ = f := by
   -- Porting note: `ext` did not pick up `NatTrans.ext`
   refine PresheafedSpace.Hom.ext _ _ rfl <| NatTrans.ext _ _ <| funext fun x => ?_
   simp only [isoRestrict_hom_c_app, NatTrans.comp_app, eqToHom_refl,
@@ -141,32 +141,26 @@ theorem isoRestrict_hom_ofRestrict : H.isoRestrict.hom ≫ Y.ofRestrict _ = f :=
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_hom_of_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
 
 @[simp]
-theorem isoRestrict_inv_ofRestrict : H.isoRestrict.inv ≫ f = Y.ofRestrict _ := by
+theorem isoRestrict_inv_ofRestrict : (isoRestrict f).inv ≫ f = Y.ofRestrict _ := by
   rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_inv_of_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict
 
-instance mono [H : IsOpenImmersion f] : Mono f := by
+instance mono : Mono f := by
   rw [← H.isoRestrict_hom_ofRestrict]; apply mono_comp
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.mono AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mono
 
 /-- The composition of two open immersions is an open immersion. -/
-instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : IsOpenImmersion f] (g : Y ⟶ Z)
-    [hg : IsOpenImmersion g] : IsOpenImmersion (f ≫ g) where
-  base_open := hg.base_open.comp hf.base_open
+instance comp {Z : PresheafedSpace C} (g : Y ⟶ Z) [hg : IsOpenImmersion g] :
+    IsOpenImmersion (f ≫ g) where
+  base_open := hg.base_open.comp H.base_open
   c_iso U := by
     generalize_proofs h
     dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base,
       TopCat.Presheaf.pushforwardObj_obj, Opens.map_comp_obj]
     apply (config := { allowSynthFailures := true }) IsIso.comp_isIso
-    · have : h.functor.obj U = hg.openFunctor.obj (hf.openFunctor.obj U) := by
-        ext1
-        dsimp only [IsOpenMap.functor_obj_coe]
-        -- Porting note: slightly more hand holding here: `g ∘ f` and `fun x => g (f x)`
-        erw [comp_base, coe_comp, show g.base ∘ f.base = fun x => g.base (f.base x) from rfl,
-          ← Set.image_image]  -- now `erw` after #13170
-      rw [this]
+    · rw [show h.functor.obj U = (openFunctor g).obj ((openFunctor f).obj U) by ext; simp]
       infer_instance
-    · have : (Opens.map g.base).obj (h.functor.obj U) = hf.openFunctor.obj U := by
+    · have : (Opens.map g.base).obj (h.functor.obj U) = (openFunctor f).obj U := by
         ext1
         dsimp only [Opens.map_coe, IsOpenMap.functor_obj_coe, comp_base]
         -- Porting note: slightly more hand holding here: `g ∘ f` and `fun x => g (f x)`
@@ -180,15 +174,15 @@ instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : IsOpenImmersion f] (g
 
 /-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`. -/
 noncomputable def invApp (U : Opens X) :
-    X.presheaf.obj (op U) ⟶ Y.presheaf.obj (op (H.openFunctor.obj U)) :=
+    X.presheaf.obj (op U) ⟶ Y.presheaf.obj (op (openFunctor f |>.obj U)) :=
   X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) ≫
-    inv (f.c.app (op (H.openFunctor.obj U)))
+    inv (f.c.app (op (openFunctor f |>.obj U)))
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
 
 @[simp, reassoc]
 theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) :
     X.presheaf.map i ≫ H.invApp (unop V) =
-      H.invApp (unop U) ≫ Y.presheaf.map (H.openFunctor.op.map i) := by
+      invApp f (unop U) ≫ Y.presheaf.map (openFunctor f |>.op.map i) := by
   simp only [invApp, ← Category.assoc]
   rw [IsIso.comp_inv_eq]
   simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
@@ -197,11 +191,11 @@ theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) :
   congr 1
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.inv_naturality AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality
 
-instance (U : Opens X) : IsIso (H.invApp U) := by delta invApp; infer_instance
+instance (U : Opens X) : IsIso (invApp f U) := by delta invApp; infer_instance
 
 theorem inv_invApp (U : Opens X) :
     inv (H.invApp U) =
-      f.c.app (op (H.openFunctor.obj U)) ≫
+      f.c.app (op (openFunctor f |>.obj U)) ≫
         X.presheaf.map
           (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := by
   rw [← cancel_epi (H.invApp U), IsIso.hom_inv_id]
@@ -211,7 +205,7 @@ theorem inv_invApp (U : Opens X) :
 
 @[simp, reassoc, elementwise]
 theorem invApp_app (U : Opens X) :
-    H.invApp U ≫ f.c.app (op (H.openFunctor.obj U)) =
+    invApp f U ≫ f.c.app (op (openFunctor f |>.obj U)) =
       X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := by
   rw [invApp, Category.assoc, IsIso.inv_hom_id, Category.comp_id]
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app
@@ -221,22 +215,19 @@ theorem app_invApp (U : Opens Y) :
     f.c.app (op U) ≫ H.invApp ((Opens.map f.base).obj U) =
       Y.presheaf.map
         ((homOfLE (Set.image_preimage_subset f.base U.1)).op :
-          op U ⟶ op (H.openFunctor.obj ((Opens.map f.base).obj U))) := by
+          op U ⟶ op (openFunctor f |>.obj ((Opens.map f.base).obj U))) := by
   erw [← Category.assoc]; rw [IsIso.comp_inv_eq, f.c.naturality]; congr
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp
 
 /-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`. -/
 @[reassoc]
 theorem app_inv_app' (U : Opens Y) (hU : (U : Set Y) ⊆ Set.range f.base) :
-    f.c.app (op U) ≫ H.invApp ((Opens.map f.base).obj U) =
+    f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) =
       Y.presheaf.map
         (eqToHom
-            (by
-              apply le_antisymm
-              · exact Set.image_preimage_subset f.base U.1
-              · rw [← SetLike.coe_subset_coe]
-                refine LE.le.trans_eq ?_ (@Set.image_preimage_eq_inter_range _ _ f.base U.1).symm
-                exact Set.subset_inter_iff.mpr ⟨fun _ h => h, hU⟩)).op := by
+            (le_antisymm (Set.image_preimage_subset f.base U.1) <|
+              (Set.image_preimage_eq_inter_range (f := f.base) (t := U.1)).symm ▸
+                Set.subset_inter_iff.mpr ⟨fun _ h => h, hU⟩)).op := by
   erw [← Category.assoc]; rw [IsIso.comp_inv_eq, f.c.naturality]; congr
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app' AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'
 
@@ -283,21 +274,21 @@ theorem ofRestrict_invApp {C : Type*} [Category C] (X : PresheafedSpace C) {Y :
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict_inv_app AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp
 
 /-- An open immersion is an iso if the underlying continuous map is epi. -/
-theorem to_iso (f : X ⟶ Y) [h : IsOpenImmersion f] [h' : Epi f.base] : IsIso f := by
+theorem to_iso [h' : Epi f.base] : IsIso f := by
   have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U) := by
     intro U
-    have : U = op (h.openFunctor.obj ((Opens.map f.base).obj (unop U))) := by
+    have : U = op (openFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
       induction U using Opposite.rec' with | h U => ?_
       cases U
       dsimp only [Functor.op, Opens.map]
       congr
       exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm
-    convert @IsOpenImmersion.c_iso _ _ _ _ _ h ((Opens.map f.base).obj (unop U))
+    convert H.c_iso (Opens.map f.base |>.obj <| unop U)
 
   have : IsIso f.c := NatIso.isIso_of_isIso_app _
 
   apply (config := { allowSynthFailures := true }) isIso_of_components
-  let t : X ≃ₜ Y := (Homeomorph.ofEmbedding _ h.base_open.toEmbedding).trans
+  let t : X ≃ₜ Y := (Homeomorph.ofEmbedding _ H.base_open.toEmbedding).trans
     { toFun := Subtype.val
       invFun := fun x =>
         ⟨x, by rw [Set.range_iff_surjective.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩
@@ -307,7 +298,7 @@ theorem to_iso (f : X ⟶ Y) [h : IsOpenImmersion f] [h' : Epi f.base] : IsIso f
 
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.to_iso AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso
 
-instance stalk_iso [HasColimits C] [H : IsOpenImmersion f] (x : X) : IsIso (stalkMap f x) := by
+instance stalk_iso [HasColimits C] (x : X) : IsIso (stalkMap f x) := by
   rw [← H.isoRestrict_hom_ofRestrict]
   rw [PresheafedSpace.stalkMap.comp]
   infer_instance
@@ -440,7 +431,7 @@ theorem pullbackConeOfLeftLift_fst :
     simp_rw [Category.assoc]
     erw [← s.pt.presheaf.map_comp]
     erw [s.snd.c.naturality_assoc]
-    have := congr_app s.condition (op (hf.openFunctor.obj x))
+    have := congr_app s.condition (op (openFunctor f |>.obj x))
     dsimp only [comp_c_app, unop_op] at this
     rw [← IsIso.comp_inv_eq] at this
     replace this := reassoc_of% this
@@ -579,7 +570,7 @@ variable (f : X ⟶ Y.toPresheafedSpace) [H : IsOpenImmersion f]
 /-- If `X ⟶ Y` is an open immersion, and `Y` is a SheafedSpace, then so is `X`. -/
 def toSheafedSpace : SheafedSpace C where
   IsSheaf := by
-    apply TopCat.Presheaf.isSheaf_of_iso (sheafIsoOfIso H.isoRestrict.symm).symm
+    apply TopCat.Presheaf.isSheaf_of_iso (sheafIsoOfIso (isoRestrict f).symm).symm
     apply TopCat.Sheaf.pushforward_sheaf_of_sheaf
     exact (Y.restrict H.base_open).IsSheaf
   toPresheafedSpace := X
@@ -1163,10 +1154,10 @@ end Pullback
 /-- An open immersion is isomorphic to the induced open subscheme on its image. -/
 noncomputable def isoRestrict {X Y : LocallyRingedSpace} {f : X ⟶ Y}
     (H : LocallyRingedSpace.IsOpenImmersion f) :
-    X ≅ Y.restrict H.base_open := by
-  apply LocallyRingedSpace.isoOfSheafedSpaceIso
-  refine SheafedSpace.forgetToPresheafedSpace.preimageIso ?_
-  exact PresheafedSpace.IsOpenImmersion.isoRestrict H
+    X ≅ Y.restrict H.base_open :=
+  LocallyRingedSpace.isoOfSheafedSpaceIso <|
+    SheafedSpace.forgetToPresheafedSpace.preimageIso <|
+      PresheafedSpace.IsOpenImmersion.isoRestrict f.1
 #align algebraic_geometry.LocallyRingedSpace.is_open_immersion.iso_restrict AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict
 
 end LocallyRingedSpace.IsOpenImmersion

Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

@@ -63,6 +63,8 @@ open TopologicalSpace CategoryTheory Opposite
 
 open CategoryTheory.Limits AlgebraicGeometry.PresheafedSpace
 
+open AlgebraicGeometry.PresheafedSpace.IsOpenImmersion
+
 open CategoryTheory.GlueData
 
 namespace AlgebraicGeometry
@@ -219,8 +221,7 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)
     simp_rw [Category.assoc]
     erw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc,
       IsOpenImmersion.app_inv_app'_assoc]
-    · simp_rw [← (𝖣.V (k, i)).presheaf.map_comp, eqToHom_map (Functor.op _), eqToHom_op,
-        eqToHom_trans]
+    · simp_rw [← (𝖣.V (k, i)).presheaf.map_comp]; rfl
     rintro x ⟨y, -, eq⟩
     replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
     change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq
@@ -250,7 +251,7 @@ variable [HasLimits C]
 
 theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
     (Opens.map (𝖣.ι j).base).obj ((D.ι_openEmbedding i).isOpenMap.functor.obj U) =
-      (D.f_open j i).openFunctor.obj
+      (openFunctor (D.f j i)).obj
         ((Opens.map (𝖣.t j i).base).obj ((Opens.map (𝖣.f i j).base).obj U)) := by
   ext1
   dsimp only [Opens.map_coe, IsOpenMap.functor_obj_coe]
@@ -618,9 +619,8 @@ theorem ι_isoPresheafedSpace_inv (i : D.J) :
 
 instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) := by
   rw [← D.ι_isoPresheafedSpace_inv]
-  -- Porting note: was `inferInstance`
-  refine PresheafedSpace.IsOpenImmersion.comp (hf := ?_) (hg := inferInstance)
-  apply PresheafedSpace.GlueData.ιIsOpenImmersion
+  have := D.toPresheafedSpaceGlueData.ιIsOpenImmersion i
+  infer_instance
 #align algebraic_geometry.SheafedSpace.glue_data.ι_IsOpenImmersion AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion
 
 theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x :=