refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446)

This PR refactors the definition of morphisms in full subcategories (and induced categories), by making them a 1-field structure. This prevents certain defeq abuse, and improves automation. (The only issue is that this adds an extra layer: `f` sometimes becomes `f.hom`, etc.)

(It would make sense to redefine `CommGrp/Grp/CommMon` as full subcategories of `Mon`, rather than defining `CommGrp` by applying `InducedCategory` twice, which adds one unnecessary layer of `.hom`, but no attempt was made to change this in this PR.)

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: joelriou

Mathlib/Algebra/Category/CommAlgCat/FiniteType.lean

@@ -50,13 +50,14 @@ lemma Algebra.FiniteType.exists_fgAlgCatSkeleton (A : Type v) [CommRing A] [Alge
 /-- Universe lift functor for finitely generated algebras. -/
 def FGAlgCat.uliftFunctor : FGAlgCat.{v} R ⥤ FGAlgCat.{max v w} R where
   obj A := ⟨.of R <| ULift A.1, .equiv inferInstance ULift.algEquiv.symm⟩
-  map {A B} f := CommAlgCat.ofHom <|
-    ULift.algEquiv.symm.toAlgHom.comp <| f.hom.comp ULift.algEquiv.toAlgHom
+  map {A B} f := ConcreteCategory.ofHom <|
+    ULift.algEquiv.symm.toAlgHom.comp <| f.hom.hom.comp ULift.algEquiv.toAlgHom
 
 /-- The universe lift functor for finitely generated algebras is fully faithful. -/
 def FGAlgCat.fullyFaithfulUliftFunctor : (FGAlgCat.uliftFunctor R).FullyFaithful where
   preimage {A B} f :=
-    CommAlgCat.ofHom <| ULift.algEquiv.toAlgHom.comp <| f.hom.comp ULift.algEquiv.symm.toAlgHom
+    ConcreteCategory.ofHom <| ULift.algEquiv.toAlgHom.comp <|
+      f.hom.hom.comp ULift.algEquiv.symm.toAlgHom
 
 instance : (FGAlgCat.uliftFunctor R).Full :=
   (FGAlgCat.fullyFaithfulUliftFunctor R).full
@@ -95,9 +96,9 @@ def FGAlgCat.equivUnder (R : CommRingCat.{u}) :
     FGAlgCat R ≌ MorphismProperty.Under (toMorphismProperty FiniteType) ⊤ R where
   functor.obj A := ⟨(commAlgCatEquivUnder R).functor.obj A.obj,
     (RingHom.finiteType_algebraMap (A := R) (B := A.obj)).mpr A.2⟩
-  functor.map {A B} f := ⟨(commAlgCatEquivUnder R).functor.map f, trivial, trivial⟩
+  functor.map {A B} f := ⟨(commAlgCatEquivUnder R).functor.map f.hom, trivial, trivial⟩
   inverse.obj A := ⟨(commAlgCatEquivUnder R).inverse.obj A.1, A.2⟩
-  inverse.map {A B} f := (commAlgCatEquivUnder R).inverse.map f.hom
+  inverse.map {A B} f := ObjectProperty.homMk ((commAlgCatEquivUnder R).inverse.map f.hom)
   unitIso := NatIso.ofComponents fun A ↦
     ObjectProperty.isoMk _ (CommAlgCat.isoMk { toRingEquiv := .refl A.1, commutes' _ := rfl })
   counitIso := .refl _

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -90,10 +90,13 @@ section Ring
 
 variable (R : Type u) [Ring R]
 
-@[simp] lemma hom_comp (A B C : FGModuleCat.{v} R) (f : A ⟶ B) (g : B ⟶ C) :
-    (f ≫ g).hom = g.hom.comp f.hom := rfl
+@[simp] lemma hom_hom_comp {A B C : FGModuleCat.{v} R} (f : A ⟶ B) (g : B ⟶ C) :
+  (f ≫ g).hom.hom = g.hom.hom.comp f.hom.hom := rfl
 
-@[simp] lemma hom_id (A : FGModuleCat.{v} R) : (𝟙 A : A ⟶ A).hom = LinearMap.id := rfl
+@[simp] lemma hom_hom_id (A : FGModuleCat.{v} R) : (𝟙 A : A ⟶ A).hom.hom = LinearMap.id := rfl
+
+@[deprecated (since := "2025-12-18")] alias hom_comp := hom_hom_comp
+@[deprecated (since := "2025-12-18")] alias hom_id := hom_hom_id
 
 instance : Inhabited (FGModuleCat.{v} R) :=
   ⟨⟨ModuleCat.of R PUnit, by unfold ModuleCat.isFG; infer_instance⟩⟩
@@ -111,17 +114,17 @@ variable {R} in
 abbrev ofHom {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V]
     [AddCommGroup W] [Module R W] [Module.Finite R W]
     (f : V →ₗ[R] W) : of R V ⟶ of R W :=
-  ModuleCat.ofHom f
+  ConcreteCategory.ofHom f
 
 variable {R} in
-@[ext] lemma hom_ext {V W : FGModuleCat.{v} R} {f g : V ⟶ W} (h : f.hom = g.hom) : f = g :=
-  ModuleCat.hom_ext h
+@[ext] lemma hom_ext {V W : FGModuleCat.{v} R} {f g : V ⟶ W} (h : f.hom.hom = g.hom.hom) : f = g :=
+  ObjectProperty.hom_ext _ (ModuleCat.hom_ext h)
 
 instance (V : FGModuleCat.{v} R) : Module.Finite R V :=
   V.property
 
 instance : (forget₂ (FGModuleCat.{v} R) (ModuleCat.{v} R)).Full where
-  map_surjective f := ⟨f, rfl⟩
+  map_surjective f := ⟨ofHom f.hom, rfl⟩
 
 variable {R} in
 /-- Converts an isomorphism in the category `FGModuleCat R` to
@@ -136,19 +139,19 @@ def _root_.LinearEquiv.toFGModuleCatIso
     {V W : Type v} [AddCommGroup V] [Module R V] [Module.Finite R V]
     [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) :
     FGModuleCat.of R V ≅ FGModuleCat.of R W where
-  hom := ModuleCat.ofHom e.toLinearMap
-  inv := ModuleCat.ofHom e.symm.toLinearMap
+  hom := ConcreteCategory.ofHom e.toLinearMap
+  inv := ConcreteCategory.ofHom e.symm.toLinearMap
   hom_inv_id := by ext x; exact e.left_inv x
   inv_hom_id := by ext x; exact e.right_inv x
 
 /-- Universe lifting as a functor on `FGModuleCat`. -/
 def ulift : FGModuleCat.{v} R ⥤ FGModuleCat.{max v w} R where
   obj M := .of R <| ULift M
-  map f := ofHom <| ULift.moduleEquiv.symm.toLinearMap ∘ₗ f.hom ∘ₗ ULift.moduleEquiv.toLinearMap
+  map f := ofHom <| ULift.moduleEquiv.symm.toLinearMap ∘ₗ f.hom.hom ∘ₗ ULift.moduleEquiv.toLinearMap
 
 /-- Universe lifting is fully faithful. -/
 def fullyFaithfulULift : (ulift R).FullyFaithful where
-  preimage f := ofHom <| ULift.moduleEquiv.toLinearMap ∘ₗ f.hom ∘ₗ
+  preimage f := ofHom <| ULift.moduleEquiv.toLinearMap ∘ₗ f.hom.hom ∘ₗ
     ULift.moduleEquiv.symm.toLinearMap
 
 instance : (ulift R).Faithful :=
@@ -177,11 +180,11 @@ instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Additive where
 instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Linear R where
 
 theorem Iso.conj_eq_conj {V W : FGModuleCat R} (i : V ≅ W) (f : End V) :
-    Iso.conj i f = FGModuleCat.ofHom (LinearEquiv.conj (isoToLinearEquiv i) f.hom) :=
+    Iso.conj i f = FGModuleCat.ofHom (LinearEquiv.conj (isoToLinearEquiv i) f.hom.hom) :=
   rfl
 
 theorem Iso.conj_hom_eq_conj {V W : FGModuleCat R} (i : V ≅ W) (f : End V) :
-    (Iso.conj i f).hom = (LinearEquiv.conj (isoToLinearEquiv i) f.hom) :=
+    (Iso.conj i f).hom.hom = (LinearEquiv.conj (isoToLinearEquiv i) f.hom.hom) :=
   rfl
 
 end CommRing
@@ -190,17 +193,21 @@ section Field
 
 variable (K : Type u) [Field K]
 
-instance (V W : FGModuleCat.{v} K) : Module.Finite K (V ⟶ W) :=
+instance (V W : FGModuleCat.{v} K) : Module.Finite K (V.obj ⟶ W.obj) :=
   (inferInstanceAs <| Module.Finite K (V →ₗ[K] W)).equiv ModuleCat.homLinearEquiv.symm
 
+instance (V W : FGModuleCat.{v} K) : Module.Finite K (V ⟶ W) :=
+  (inferInstanceAs (Module.Finite K (V.obj ⟶ W.obj))).equiv
+    InducedCategory.homLinearEquiv.symm
+
 instance : (ModuleCat.isFG K).IsMonoidalClosed where
   prop_ihom {X Y} (_ : Module.Finite _ _) (_ : Module.Finite _ _) :=
     (inferInstanceAs <| Module.Finite K (X →ₗ[K] Y)).equiv ModuleCat.homLinearEquiv.symm
 
 variable (V W : FGModuleCat K)
 
 @[simp]
-theorem ihom_obj : (ihom V).obj W = FGModuleCat.of K (V ⟶ W) :=
+theorem ihom_obj : (ihom V).obj W = FGModuleCat.of K (V.obj ⟶ W.obj) :=
   rfl
 
 /-- The dual module is the dual in the rigid monoidal category `FGModuleCat K`. -/
@@ -215,7 +222,7 @@ open CategoryTheory.MonoidalCategory
 
 /-- The coevaluation map is defined in `LinearAlgebra.coevaluation`. -/
 def FGModuleCatCoevaluation : 𝟙_ (FGModuleCat K) ⟶ V ⊗ FGModuleCatDual K V :=
-  ModuleCat.ofHom <| coevaluation K V
+  ConcreteCategory.ofHom <| coevaluation K V
 
 theorem FGModuleCatCoevaluation_apply_one :
     (FGModuleCatCoevaluation K V).hom (1 : K) =
@@ -225,7 +232,7 @@ theorem FGModuleCatCoevaluation_apply_one :
 
 /-- The evaluation morphism is given by the contraction map. -/
 def FGModuleCatEvaluation : FGModuleCatDual K V ⊗ V ⟶ 𝟙_ (FGModuleCat K) :=
-  ModuleCat.ofHom <| contractLeft K V
+  ConcreteCategory.ofHom <| contractLeft K V
 
 theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
     (FGModuleCatEvaluation K V).hom (f ⊗ₜ x) = f.toFun x :=
@@ -237,7 +244,7 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
 theorem FGModuleCatEvaluation_apply' (f : FGModuleCatDual K V) (x : V) :
     DFunLike.coe
       (F := ((ModuleCat.of K (Module.Dual K V) ⊗ V.obj).carrier →ₗ[K] (𝟙_ (ModuleCat K))))
-      (FGModuleCatEvaluation K V).hom (f ⊗ₜ x) = f.toFun x :=
+      (FGModuleCatEvaluation K V).hom.hom (f ⊗ₜ x) = f.toFun x :=
   contractLeft_apply f x
 
 private theorem coevaluation_evaluation :
@@ -275,10 +282,10 @@ end FGModuleCat
 
 @[simp] theorem LinearMap.comp_id_fgModuleCat
     {R} [Ring R] {G : FGModuleCat.{v} R} {H : Type v} [AddCommGroup H] [Module R H]
-    (f : G →ₗ[R] H) : f.comp (ModuleCat.Hom.hom (𝟙 G)) = f :=
+    (f : G →ₗ[R] H) : f.comp (ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 G))) = f :=
   ModuleCat.hom_ext_iff.mp <| Category.id_comp (ModuleCat.ofHom f)
 
 @[simp] theorem LinearMap.id_fgModuleCat_comp
     {R} [Ring R] {G : Type v} [AddCommGroup G] [Module R G] {H : FGModuleCat.{v} R}
-    (f : G →ₗ[R] H) : LinearMap.comp (ModuleCat.Hom.hom (𝟙 H)) f = f :=
+    (f : G →ₗ[R] H) : LinearMap.comp (ModuleCat.Hom.hom (InducedCategory.Hom.hom (𝟙 H))) f = f :=
   ModuleCat.hom_ext_iff.mp <| Category.comp_id (ModuleCat.ofHom f)

Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean

@@ -67,7 +67,8 @@ noncomputable def ofFiniteEquiv : ofFinite R M ≃ₗ[R] M :=
   Classical.choice (Module.Finite.exists_fin_quot_equiv R M).choose_spec.choose_spec
 
 instance : Category (FGModuleRepr R) :=
-  InducedCategory.category fun x : FGModuleRepr R ↦ FGModuleCat.of R x
+  inferInstanceAs (Category (InducedCategory _
+    (fun x : FGModuleRepr R ↦ FGModuleCat.of R x)))
 
 instance : SmallCategory (FGModuleRepr R) where
 

Mathlib/Algebra/Category/Grp/FiniteGrp.lean

@@ -45,7 +45,8 @@ instance : CoeSort FiniteGrp.{u} (Type u) where
   coe G := G.toGrp
 
 @[to_additive]
-instance : Category FiniteGrp := InducedCategory.category FiniteGrp.toGrp
+instance : Category FiniteGrp :=
+  inferInstanceAs (Category (InducedCategory _ FiniteGrp.toGrp))
 
 @[to_additive]
 instance : ConcreteCategory FiniteGrp (· →* ·) := InducedCategory.concreteCategory FiniteGrp.toGrp
@@ -67,7 +68,7 @@ def of (G : Type u) [Group G] [Finite G] : FiniteGrp where
 @[to_additive
 /-- The morphism in `FiniteAddGrp`, induced from a morphism of the category `AddGrpCat` -/]
 def ofHom {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) : of X ⟶ of Y :=
-  GrpCat.ofHom f
+  InducedCategory.homMk (GrpCat.ofHom f)
 
 @[to_additive]
 lemma ofHom_apply {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) (x : X) :

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -65,7 +65,7 @@ instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
 
 /-- Implementation, see `leftExactFunctorForgetEquivalence`. -/
 noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrpCat.{v}) :=
-  ObjectProperty.lift _ inverseAux inferInstance
+  ObjectProperty.lift _ inverseAux (by simp only [leftExactFunctor_iff]; infer_instance)
 
 open scoped MonObj
 

Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

@@ -22,37 +22,24 @@ universe u
 
 open CategoryTheory
 
+attribute [local simp] add_smul mul_smul in
+attribute [local ext] End.ext in
 /-- An ingredient of Tannaka duality for rings:
 A ring `R` is equivalent to
 the endomorphisms of the additive forgetful functor `Module R ⥤ AddCommGroup`.
 -/
 def ringEquivEndForget₂ (R : Type u) [Ring R] :
     R ≃+* End (AdditiveFunctor.of (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u})) where
   toFun r :=
-    { app := fun M =>
-        @AddCommGrpCat.ofHom M.carrier M.carrier _ _ (DistribMulAction.toAddMonoidHom M r) }
-  invFun φ := φ.app (ModuleCat.of R R) (1 : R)
-  left_inv := by
-    intro r
-    simp
-  right_inv := by
-    intro φ
-    apply NatTrans.ext
+    ObjectProperty.homMk
+      { app M := @AddCommGrpCat.ofHom M.carrier M.carrier _ _
+          (DistribMulAction.toAddMonoidHom M r) }
+  invFun φ := φ.hom.app (ModuleCat.of R R) (1 : R)
+  left_inv _ := by simp
+  right_inv φ := by
     ext M (x : M)
     have w := CategoryTheory.congr_fun
-      (φ.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)
-    exact w.symm.trans (congr_arg (φ.app M) (one_smul R x))
-  map_add' := by
-    intros
-    apply NatTrans.ext
-    ext
-    simp only [AdditiveFunctor.of_fst, ModuleCat.forget₂_obj, DistribMulAction.toAddMonoidHom_apply,
-      add_smul, AddCommGrpCat.hom_ofHom]
-    rfl
-  map_mul' := by
-    intros
-    apply NatTrans.ext
-    ext
-    simp only [AdditiveFunctor.of_fst, ModuleCat.forget₂_obj, DistribMulAction.toAddMonoidHom_apply,
-      mul_smul, AddCommGrpCat.hom_ofHom]
-    rfl
+      (φ.hom.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)
+    exact w.symm.trans (congr_arg (φ.hom.app M) (one_smul R x))
+  map_add' := by cat_disch
+  map_mul' := by cat_disch

Mathlib/Algebra/Homology/LocalCohomology.lean

@@ -206,7 +206,7 @@ instance ideal_powers_initial [hR : IsNoetherian R R] :
   out J' := by
     apply (config := { allowSynthFailures := true }) zigzag_isConnected
     · obtain ⟨k, hk⟩ := Ideal.exists_pow_le_of_le_radical_of_fg J'.2 (isNoetherian_def.mp hR _)
-      exact ⟨CostructuredArrow.mk (⟨⟨hk⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩
+      exact ⟨CostructuredArrow.mk (⟨⟨⟨hk⟩⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩
     · intro j1 j2
       apply Relation.ReflTransGen.single
       -- The inclusions `J^n1 ≤ J'` and `J^n2 ≤ J'` always form a triangle, based on

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -103,7 +103,7 @@ def AffineScheme.of (X : Scheme) [h : IsAffine X] : AffineScheme :=
 /-- Type check a morphism of schemes as a morphism in `AffineScheme`. -/
 def AffineScheme.ofHom {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
     AffineScheme.of X ⟶ AffineScheme.of Y :=
-  f
+  InducedCategory.homMk f
 
 @[simp]
 theorem essImage_Spec {X : Scheme} : Scheme.Spec.essImage X ↔ IsAffine X :=

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -45,23 +45,18 @@ variable [∀ x, HasPullback (𝒰.f x ≫ f) g]
 instance (i : 𝒰.I₀) : IsOpenImmersion (𝒰.f i) := 𝒰.map_prop i
 
 /-- The affine cover of a scheme. -/
-def affineCover (X : Scheme.{u}) : OpenCover X where
-  I₀ := X
-  X x := Spec (X.local_affine x).choose_spec.choose
-  f x :=
-    ⟨(X.local_affine x).choose_spec.choose_spec.some.inv ≫ X.toLocallyRingedSpace.ofRestrict _⟩
-  mem₀ := by
-    rw [presieve₀_mem_precoverage_iff]
-    refine ⟨fun x ↦ ?_, inferInstance⟩
-    use x
-    simp only [LocallyRingedSpace.comp_toShHom, SheafedSpace.comp_base, TopCat.hom_comp,
-      ContinuousMap.coe_comp]
-    rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
-    · erw [Subtype.range_coe_subtype]
-      exact (X.local_affine x).choose.2
-    rw [← TopCat.epi_iff_surjective]
-    change Epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forgetToSheafedSpace.map _))
-    infer_instance
+def affineCover (X : Scheme.{u}) : OpenCover X := by
+  choose U R h using X.local_affine
+  let e (x) := (h x).some
+  exact
+  { I₀ := X
+    X x := Spec (R x)
+    f x := ⟨(e x).inv ≫ X.toLocallyRingedSpace.ofRestrict _⟩
+    mem₀ := by
+      rw [presieve₀_mem_precoverage_iff]
+      refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
+      change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x
+      cat_disch }
 
 instance : Inhabited X.OpenCover :=
   ⟨X.affineCover⟩

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -172,26 +172,27 @@ def toΓSpecCBasicOpens :
     apply X.presheaf.map_comp
 
 /-- The canonical morphism of sheafed spaces from `X` to the spectrum of its global sections. -/
-@[simps]
-def toΓSpecSheafedSpace : X.toSheafedSpace ⟶ Spec.toSheafedSpace.obj (op (Γ.obj (op X))) where
-  base := X.toΓSpecBase
-  c :=
-    TopCat.Sheaf.restrictHomEquivHom (structureSheaf (Γ.obj (op X))).1 _ isBasis_basic_opens
-      X.toΓSpecCBasicOpens
+@[simps! -isSimp]
+def toΓSpecSheafedSpace : X.toSheafedSpace ⟶ Spec.toSheafedSpace.obj (op (Γ.obj (op X))) :=
+  InducedCategory.homMk
+    { base := X.toΓSpecBase
+      c :=
+        TopCat.Sheaf.restrictHomEquivHom (structureSheaf (Γ.obj (op X))).1 _ isBasis_basic_opens
+          X.toΓSpecCBasicOpens }
 
 theorem toΓSpecSheafedSpace_app_eq :
-    X.toΓSpecSheafedSpace.c.app (op (basicOpen r)) = X.toΓSpecCApp r := by
+    X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen r)) = X.toΓSpecCApp r := by
   apply TopCat.Sheaf.extend_hom_app _ _ _
 
 @[reassoc] theorem toΓSpecSheafedSpace_app_spec (r : Γ.obj (op X)) :
-    toOpen (Γ.obj (op X)) (basicOpen r) ≫ X.toΓSpecSheafedSpace.c.app (op (basicOpen r)) =
+    toOpen (Γ.obj (op X)) (basicOpen r) ≫ X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen r)) =
       X.toToΓSpecMapBasicOpen r :=
   (X.toΓSpecSheafedSpace_app_eq r).symm ▸ X.toΓSpecCApp_spec r
 
 /-- The map on stalks induced by the unit commutes with maps from `Γ(X)` to
 stalks (in `Spec Γ(X)` and in `X`). -/
 theorem toStalk_stalkMap_toΓSpec (x : X) :
-    toStalk _ _ ≫ X.toΓSpecSheafedSpace.stalkMap x = X.presheaf.Γgerm x := by
+    toStalk _ _ ≫ X.toΓSpecSheafedSpace.hom.stalkMap x = X.presheaf.Γgerm x := by
   rw [PresheafedSpace.Hom.stalkMap,
     ← toOpen_germ _ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
     ← Category.assoc, Category.assoc (toOpen _ _), stalkFunctor_map_germ, ← Category.assoc,
@@ -202,10 +203,8 @@ theorem toStalk_stalkMap_toΓSpec (x : X) :
 
 /-- The canonical morphism from `X` to the spectrum of its global sections. -/
 @[simps! base]
-def toΓSpec : X ⟶ Spec.locallyRingedSpaceObj (Γ.obj (op X)) where
-  __ := X.toΓSpecSheafedSpace
-  prop := by
-    intro x
+def toΓSpec : X ⟶ Spec.locallyRingedSpaceObj (Γ.obj (op X)) :=
+  LocallyRingedSpace.homMk (X.toΓSpecSheafedSpace) (fun x ↦ by
     let p : PrimeSpectrum (Γ.obj (op X)) := X.toΓSpecFun x
     constructor
     -- show stalk map is local hom ↓
@@ -222,7 +221,7 @@ def toΓSpec : X ⟶ Spec.locallyRingedSpaceObj (Γ.obj (op X)) where
     rw [← toStalk_stalkMap_toΓSpec, CommRingCat.comp_apply]
     erw [← he]
     rw [map_mul]
-    exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _
+    exact ht.mul <| (IsLocalization.map_units (R := Γ.obj (op X)) S s).map _)
 
 /-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
 of `Γ(X, ⊤)` under `toΓSpec` agrees with the associated zero locus on `X`. -/
@@ -250,11 +249,11 @@ theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f
         f ≫ X.presheaf.map (homOfLE le_top : (Opens.map β.base).obj (basicOpen r) ⟶ _).op =
           toOpen R (basicOpen r) ≫ β.c.app (op (basicOpen r))) :
     X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β := by
-  ext1
-  refine Spec.basicOpen_hom_ext w ?_
+  refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
+    (Spec.basicOpen_hom_ext w ?_)
   intro r U
-  rw [LocallyRingedSpace.comp_c_app]
-  erw [toOpen_comp_comap_assoc]
+  erw [SheafedSpace.comp_hom_c_app, toOpen_comp_comap_assoc]
+  dsimp
   rw [Category.assoc]
   erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]
   exact h r