refactor(algebraic_geometry/*): Make LocallyRingedSpace.hom a custo…

…m structure. (#15973)

We also define `algebraic_geometry.Scheme.hom` as an type alias for morphisms between schemes to enable
dot notation.



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/algebraic_geometry/AffineScheme.lean

@@ -146,7 +146,7 @@ def Scheme.affine_opens (X : Scheme) : set (opens X.carrier) :=
 { U : opens X.carrier | is_affine_open U }
 
 lemma range_is_affine_open_of_open_immersion {X Y : Scheme} [is_affine X] (f : X ⟶ Y)
-  [H : is_open_immersion f] : is_affine_open ⟨set.range f.1.base, H.base_open.open_range⟩ :=
+  [H : is_open_immersion f] : is_affine_open f.opens_range :=
 begin
   refine is_affine_of_iso (is_open_immersion.iso_of_range_eq f (Y.of_restrict _) _).inv,
   exact subtype.range_coe.symm,
@@ -222,7 +222,7 @@ end
 
 lemma is_affine_open.image_is_open_immersion {X Y : Scheme} {U : opens X.carrier}
   (hU : is_affine_open U)
-  (f : X ⟶ Y) [H : is_open_immersion f] : is_affine_open (H.open_functor.obj U) :=
+  (f : X ⟶ Y) [H : is_open_immersion f] : is_affine_open (f.opens_functor.obj U) :=
 begin
   haveI : is_affine _ := hU,
   convert range_is_affine_open_of_open_immersion (X.of_restrict U.open_embedding ≫ f),
@@ -317,7 +317,7 @@ begin
     (X.basic_open f : set X.carrier),
   { rw [set.image_preimage_eq_inter_range, set.inter_eq_left_iff_subset, hU.from_Spec_range],
     exact Scheme.basic_open_subset _ _ },
-  rw [subtype.coe_mk, Scheme.comp_val_base, ← this, coe_comp, set.range_comp],
+  rw [Scheme.hom.opens_range_coe, Scheme.comp_val_base, ← this, coe_comp, set.range_comp],
   congr' 1,
   refine (congr_arg coe $ Scheme.preimage_basic_open hU.from_Spec f).trans _,
   refine eq.trans _ (prime_spectrum.localization_away_comap_range (localization.away f) f).symm,
@@ -396,7 +396,7 @@ begin
   swap, exact ⟨x, h⟩,
   have : U.open_embedding.is_open_map.functor.obj ((X.restrict U.open_embedding).basic_open r)
     = X.basic_open (X.presheaf.map (eq_to_hom U.open_embedding_obj_top.symm).op r),
-  { refine (is_open_immersion.image_basic_open (X.of_restrict U.open_embedding) r).trans _,
+  { refine (Scheme.image_basic_open (X.of_restrict U.open_embedding) r).trans _,
     erw ← Scheme.basic_open_res_eq _ _ (eq_to_hom U.open_embedding_obj_top).op,
     rw [← comp_apply, ← category_theory.functor.map_comp, ← op_comp, eq_to_hom_trans,
       eq_to_hom_refl, op_id, category_theory.functor.map_id],

src/algebraic_geometry/Gamma_Spec_adjunction.lean

@@ -183,10 +183,10 @@ begin
 end
 
 /-- The canonical morphism from `X` to the spectrum of its global sections. -/
-@[simps coe_base]
+@[simps val_base]
 def to_Γ_Spec : X ⟶ Spec.LocallyRingedSpace_obj (Γ.obj (op X)) :=
 { val := X.to_Γ_Spec_SheafedSpace,
-  property :=
+  prop :=
   begin
     intro x,
     let p : prime_spectrum (Γ.obj (op X)) := X.to_Γ_Spec_fun x,
@@ -246,7 +246,7 @@ def identity_to_Γ_Spec : 𝟭 LocallyRingedSpace.{u} ⟶ Γ.right_op ⋙ Spec.t
     apply LocallyRingedSpace.comp_ring_hom_ext,
     { ext1 x,
       dsimp [Spec.Top_map, LocallyRingedSpace.to_Γ_Spec_fun],
-      rw [← subtype.val_eq_coe, ← local_ring.comap_closed_point (PresheafedSpace.stalk_map _ x),
+      rw [← local_ring.comap_closed_point (PresheafedSpace.stalk_map _ x),
         ← prime_spectrum.comap_comp_apply, ← prime_spectrum.comap_comp_apply],
       congr' 2,
       exact (PresheafedSpace.stalk_map_germ f.1 ⊤ ⟨x,trivial⟩).symm,

src/algebraic_geometry/Scheme.lean

@@ -39,11 +39,16 @@ structure Scheme extends to_LocallyRingedSpace : LocallyRingedSpace :=
 
 namespace Scheme
 
+/-- A morphism between schemes is a morphism between the underlying locally ringed spaces. -/
+@[nolint has_nonempty_instance] -- There isn't nessecarily a morphism between two schemes.
+def hom (X Y : Scheme) : Type* :=
+X.to_LocallyRingedSpace ⟶ Y.to_LocallyRingedSpace
+
 /--
 Schemes are a full subcategory of locally ringed spaces.
 -/
 instance : category Scheme :=
-induced_category.category Scheme.to_LocallyRingedSpace
+{ hom := hom, ..(induced_category.category Scheme.to_LocallyRingedSpace) }
 
 /-- The structure sheaf of a Scheme. -/
 protected abbreviation sheaf (X : Scheme) := X.to_SheafedSpace.sheaf
@@ -61,16 +66,11 @@ def forget_to_LocallyRingedSpace : Scheme ⥤ LocallyRingedSpace :=
 def forget_to_Top : Scheme ⥤ Top :=
   Scheme.forget_to_LocallyRingedSpace ⋙ LocallyRingedSpace.forget_to_Top
 
-instance {X Y : Scheme} : has_lift_t (X ⟶ Y)
-  (X.to_SheafedSpace ⟶ Y.to_SheafedSpace) := (@@coe_to_lift $ @@coe_base coe_subtype)
-
-lemma id_val_base (X : Scheme) : (subtype.val (𝟙 X)).base = 𝟙 _ := rfl
-
-@[simp] lemma id_coe_base (X : Scheme) :
-  (↑(𝟙 X) : X.to_SheafedSpace ⟶ X.to_SheafedSpace).base = 𝟙 _ := rfl
+@[simp]
+lemma id_val_base (X : Scheme) : (𝟙 X : _).1.base = 𝟙 _ := rfl
 
 @[simp] lemma id_app {X : Scheme} (U : (opens X.carrier)ᵒᵖ) :
-  (subtype.val (𝟙 X)).c.app U = X.presheaf.map
+  (𝟙 X : _).val.c.app U = X.presheaf.map
     (eq_to_hom (by { induction U using opposite.rec, cases U, refl })) :=
 PresheafedSpace.id_c_app X.to_PresheafedSpace U
 
@@ -80,7 +80,7 @@ lemma comp_val {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
 
 @[reassoc, simp]
 lemma comp_coe_base {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
-  (↑(f ≫ g) : X.to_SheafedSpace ⟶ Z.to_SheafedSpace).base = f.val.base ≫ g.val.base := rfl
+  (f ≫ g).val.base = f.val.base ≫ g.val.base := rfl
 
 @[reassoc, elementwise]
 lemma comp_val_base {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
@@ -211,19 +211,13 @@ RingedSpace.basic_open_res_eq _ i f
 lemma basic_open_subset : X.basic_open f ⊆ U :=
 RingedSpace.basic_open_subset _ _
 
+@[simp]
 lemma preimage_basic_open {X Y : Scheme} (f : X ⟶ Y) {U : opens Y.carrier}
   (r : Y.presheaf.obj $ op U) :
   (opens.map f.1.base).obj (Y.basic_open r) =
     @Scheme.basic_open X ((opens.map f.1.base).obj U) (f.1.c.app _ r) :=
 LocallyRingedSpace.preimage_basic_open f r
 
-@[simp]
-lemma preimage_basic_open' {X Y : Scheme} (f : X ⟶ Y) {U : opens Y.carrier}
-  (r : Y.presheaf.obj $ op U) :
-  (opens.map (↑f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace).base).obj (Y.basic_open r) =
-    @Scheme.basic_open X ((opens.map f.1.base).obj U) (f.1.c.app _ r) :=
-LocallyRingedSpace.preimage_basic_open f r
-
 @[simp]
 lemma basic_open_zero (U : opens X.carrier) : X.basic_open (0 : X.presheaf.obj $ op U) = ∅ :=
 LocallyRingedSpace.basic_open_zero _ U
@@ -232,7 +226,6 @@ LocallyRingedSpace.basic_open_zero _ U
 lemma basic_open_mul : X.basic_open (f * g) = X.basic_open f ⊓ X.basic_open g :=
 RingedSpace.basic_open_mul _ _ _
 
-@[simp]
 lemma basic_open_of_is_unit {f : X.presheaf.obj (op U)} (hf : is_unit f) : X.basic_open f = U :=
 RingedSpace.basic_open_of_is_unit _ hf
 

src/algebraic_geometry/Spec.lean

@@ -188,7 +188,7 @@ The induced map of a ring homomorphism on the prime spectra, as a morphism of lo
 -/
 @[simps] def Spec.LocallyRingedSpace_map {R S : CommRing} (f : R ⟶ S) :
   Spec.LocallyRingedSpace_obj S ⟶ Spec.LocallyRingedSpace_obj R :=
-subtype.mk (Spec.SheafedSpace_map f) $ λ p, is_local_ring_hom.mk $ λ a ha,
+LocallyRingedSpace.hom.mk (Spec.SheafedSpace_map f) $ λ p, is_local_ring_hom.mk $ λ a ha,
 begin
   -- Here, we are showing that the map on prime spectra induced by `f` is really a morphism of
   -- *locally* ringed spaces, i.e. that the induced map on the stalks is a local ring homomorphism.
@@ -197,17 +197,19 @@ begin
   rw iso.inv_hom_id_apply at ha,
   replace ha := is_local_ring_hom.map_nonunit _ ha,
   convert ring_hom.is_unit_map (stalk_iso R (prime_spectrum.comap f p)).inv ha,
-  rw iso.hom_inv_id_apply,
+  rw iso.hom_inv_id_apply
 end
 
 @[simp] lemma Spec.LocallyRingedSpace_map_id (R : CommRing) :
   Spec.LocallyRingedSpace_map (𝟙 R) = 𝟙 (Spec.LocallyRingedSpace_obj R) :=
-subtype.ext $ by { rw [Spec.LocallyRingedSpace_map_coe, Spec.SheafedSpace_map_id], refl }
+LocallyRingedSpace.hom.ext _ _ $
+  by { rw [Spec.LocallyRingedSpace_map_val, Spec.SheafedSpace_map_id], refl }
 
 lemma Spec.LocallyRingedSpace_map_comp {R S T : CommRing} (f : R ⟶ S) (g : S ⟶ T) :
   Spec.LocallyRingedSpace_map (f ≫ g) =
   Spec.LocallyRingedSpace_map g ≫ Spec.LocallyRingedSpace_map f :=
-subtype.ext $ by { rw [Spec.LocallyRingedSpace_map_coe, Spec.SheafedSpace_map_comp], refl }
+LocallyRingedSpace.hom.ext _ _ $
+  by { rw [Spec.LocallyRingedSpace_map_val, Spec.SheafedSpace_map_comp], refl }
 
 /--
 Spec, as a contravariant functor from commutative rings to locally ringed spaces.

src/algebraic_geometry/gluing.lean

@@ -351,7 +351,8 @@ instance from_glued_stalk_iso (x : 𝒰.glued_cover.glued.carrier) :
   is_iso (PresheafedSpace.stalk_map 𝒰.from_glued.val x) :=
 begin
   obtain ⟨i, x, rfl⟩ := 𝒰.glued_cover.ι_jointly_surjective x,
-  have := PresheafedSpace.stalk_map.congr_hom _ _ (congr_arg subtype.val $ 𝒰.ι_from_glued i) x,
+  have := PresheafedSpace.stalk_map.congr_hom _ _
+    (congr_arg LocallyRingedSpace.hom.val $ 𝒰.ι_from_glued i) x,
   erw PresheafedSpace.stalk_map.comp at this,
   rw ← is_iso.eq_comp_inv at this,
   rw this,

src/algebraic_geometry/locally_ringed_space.lean

@@ -63,15 +63,13 @@ def 𝒪 : sheaf CommRing X.to_Top := X.to_SheafedSpace.sheaf
 
 /-- A morphism of locally ringed spaces is a morphism of ringed spaces
  such that the morphims induced on stalks are local ring homomorphisms. -/
-def hom (X Y : LocallyRingedSpace) : Type* :=
-{ f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace //
-    ∀ x, is_local_ring_hom (PresheafedSpace.stalk_map f x) }
+@[ext]
+structure hom (X Y : LocallyRingedSpace.{u}) : Type u :=
+(val : X.to_SheafedSpace ⟶ Y.to_SheafedSpace)
+(prop : ∀ x, is_local_ring_hom (PresheafedSpace.stalk_map val x))
 
 instance : quiver LocallyRingedSpace := ⟨hom⟩
 
-@[ext] lemma hom_ext {X Y : LocallyRingedSpace} (f g : hom X Y) (w : f.1 = g.1) : f = g :=
-subtype.eq w
-
 /--
 The stalk of a locally ringed space, just as a `CommRing`.
 -/
@@ -103,7 +101,6 @@ def id (X : LocallyRingedSpace) : hom X X :=
 instance (X : LocallyRingedSpace) : inhabited (hom X X) := ⟨id X⟩
 
 /-- Composition of morphisms of locally ringed spaces. -/
-@[simps]
 def comp {X Y Z : LocallyRingedSpace} (f : hom X Y) (g : hom Y Z) : hom X Z :=
 ⟨f.val ≫ g.val, λ x,
 begin
@@ -116,9 +113,9 @@ instance : category LocallyRingedSpace :=
 { hom := hom,
   id := id,
   comp := λ X Y Z f g, comp f g,
-  comp_id' := by { intros, ext1, simp, },
-  id_comp' := by { intros, ext1, simp, },
-  assoc' := by { intros, ext1, simp, }, }.
+  comp_id' := by { intros, ext1, simp [comp], },
+  id_comp' := by { intros, ext1, simp [comp], },
+  assoc' := by { intros, ext1, simp [comp], }, }.
 
 /-- The forgetful functor from `LocallyRingedSpace` to `SheafedSpace CommRing`. -/
 @[simps] def forget_to_SheafedSpace : LocallyRingedSpace ⥤ SheafedSpace CommRing :=
@@ -151,7 +148,7 @@ See also `iso_of_SheafedSpace_iso`.
 @[simps]
 def hom_of_SheafedSpace_hom_of_is_iso {X Y : LocallyRingedSpace}
   (f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace) [is_iso f] : X ⟶ Y :=
-subtype.mk f $ λ x,
+hom.mk f $ λ x,
 -- Here we need to see that the stalk maps are really local ring homomorphisms.
 -- This can be solved by type class inference, because stalk maps of isomorphisms are isomorphisms
 -- and isomorphisms are local ring homomorphisms.
@@ -171,14 +168,14 @@ def iso_of_SheafedSpace_iso {X Y : LocallyRingedSpace}
   (f : X.to_SheafedSpace ≅ Y.to_SheafedSpace) : X ≅ Y :=
 { hom := hom_of_SheafedSpace_hom_of_is_iso f.hom,
   inv := hom_of_SheafedSpace_hom_of_is_iso f.inv,
-  hom_inv_id' := hom_ext _ _ f.hom_inv_id,
-  inv_hom_id' := hom_ext _ _ f.inv_hom_id }
+  hom_inv_id' := hom.ext _ _ f.hom_inv_id,
+  inv_hom_id' := hom.ext _ _ f.inv_hom_id }
 
 instance : reflects_isomorphisms forget_to_SheafedSpace :=
 { reflects := λ X Y f i,
   { out := by exactI
     ⟨hom_of_SheafedSpace_hom_of_is_iso (category_theory.inv (forget_to_SheafedSpace.map f)),
-      hom_ext _ _ (is_iso.hom_inv_id _), hom_ext _ _ (is_iso.inv_hom_id _)⟩ } }
+      hom.ext _ _ (is_iso.hom_inv_id _), hom.ext _ _ (is_iso.inv_hom_id _)⟩ } }
 
 instance is_SheafedSpace_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) [is_iso f] :
   is_iso f.1 :=

src/algebraic_geometry/locally_ringed_space/has_colimits.lean

@@ -90,9 +90,10 @@ def coproduct_cofan_is_colimit : is_colimit (coproduct_cofan F) :=
       ((forget_to_SheafedSpace.map_cocone s).ι.app i) y) := (s.ι.app i).2 y,
     apply_instance
   end⟩,
-  fac' := λ s j, subtype.eq (colimit.ι_desc _ _),
-  uniq' := λ s f h, subtype.eq (is_colimit.uniq _ (forget_to_SheafedSpace.map_cocone s) f.1
-    (λ j, congr_arg subtype.val (h j))) }
+  fac' := λ s j, LocallyRingedSpace.hom.ext _ _ (colimit.ι_desc _ _),
+  uniq' := λ s f h, LocallyRingedSpace.hom.ext _ _
+    (is_colimit.uniq _ (forget_to_SheafedSpace.map_cocone s) f.1
+    (λ j, congr_arg LocallyRingedSpace.hom.val (h j))) }
 
 instance : has_coproducts.{u} LocallyRingedSpace.{u} :=
 λ ι, ⟨λ F, ⟨⟨⟨_, coproduct_cofan_is_colimit F⟩⟩⟩⟩
@@ -235,7 +236,7 @@ def coequalizer : LocallyRingedSpace :=
 noncomputable
 def coequalizer_cofork : cofork f g :=
 @cofork.of_π _ _ _ _ f g (coequalizer f g) ⟨coequalizer.π f.1 g.1, infer_instance⟩
-  (subtype.eq (coequalizer.condition f.1 g.1))
+  (LocallyRingedSpace.hom.ext _ _ (coequalizer.condition f.1 g.1))
 
 lemma is_local_ring_hom_stalk_map_congr {X Y : RingedSpace} (f g : X ⟶ Y) (H : f = g)
   (x) (h : is_local_ring_hom (PresheafedSpace.stalk_map f x)) :
@@ -259,10 +260,10 @@ begin
     apply is_local_ring_hom_stalk_map_congr _ _ (coequalizer.π_desc s.π.1 e).symm y,
     apply_instance },
   split,
-  exact subtype.eq (coequalizer.π_desc _ _),
+  { exact LocallyRingedSpace.hom.ext _ _ (coequalizer.π_desc _ _) },
   intros m h,
   replace h : (coequalizer_cofork f g).π.1 ≫ m.1 = s.π.1 := by { rw ← h, refl },
-  apply subtype.eq,
+  apply LocallyRingedSpace.hom.ext,
   apply (colimit.is_colimit (parallel_pair f.1 g.1)).uniq (cofork.of_π s.π.1 e) m.1,
   rintro ⟨⟩,
   { rw [← (colimit.cocone (parallel_pair f.val g.val)).w walking_parallel_pair_hom.left,

src/algebraic_geometry/morphisms/basic.lean

@@ -232,7 +232,7 @@ begin
     all_goals { ext1, exact subtype.range_coe } },
   tfae_have : 1 → 5,
   { intro H,
-    refine ⟨Y.carrier, λ x, is_open_immersion.opens_range (Y.affine_cover.map x), _,
+    refine ⟨Y.carrier, λ x, (Y.affine_cover.map x).opens_range, _,
       λ i, range_is_affine_open_of_open_immersion _, _⟩,
     { rw eq_top_iff, intros x _, erw opens.mem_supr, exact⟨x, Y.affine_cover.covers x⟩ },
     { intro i, exact H ⟨_, range_is_affine_open_of_open_immersion _⟩ } },
@@ -357,7 +357,7 @@ begin
   tfae_have : 4 → 3,
   { intros H 𝒰 i,
     rw ← hP.1.arrow_mk_iso_iff (morphism_restrict_opens_range f _),
-    exact H (is_open_immersion.opens_range $ 𝒰.map i) },
+    exact H (𝒰.map i).opens_range },
   tfae_have : 3 → 2,
   { exact λ H, ⟨Y.affine_cover, H Y.affine_cover⟩ },
   tfae_have : 4 → 5,

src/algebraic_geometry/morphisms/ring_hom_properties.lean

@@ -286,7 +286,7 @@ begin
   { dsimp [functor.op],
     conv_lhs { rw opens.open_embedding_obj_top },
     conv_rhs { rw opens.open_embedding_obj_top },
-    erw is_open_immersion.image_basic_open (X.of_restrict U.1.open_embedding),
+    erw Scheme.image_basic_open (X.of_restrict U.1.open_embedding),
     erw PresheafedSpace.is_open_immersion.of_restrict_inv_app_apply,
     rw Scheme.basic_open_res_eq },
   { apply_instance }