[Merged by Bors] - refactor(AlgebraicGeometry): Rework Morphisms/Basic to phase away from TFAEs

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -501,6 +501,9 @@ lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl
 
 lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
+/-- Specialization of `ConcreteCategory.id_apply` because `simp` can't see through the defeq. -/
+@[simp] lemma id_apply (R : CommRingCat) (x : R) : 𝟙 R x = x := rfl
+
 @[simp] lemma forget_map {X Y : CommRingCat} (f : X ⟶ Y) :
     (forget CommRingCat).map f = (f : X → Y) := rfl
 

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -225,10 +225,13 @@ instance Scheme.isAffine_affineBasisCover (X : Scheme) (i : X.affineBasisCover.J
   isAffine_Spec _
 #align algebraic_geometry.Scheme.affine_basis_cover_is_affine AlgebraicGeometry.Scheme.isAffine_affineBasisCover
 
-instance Scheme.isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i: 𝒰.J) :
+instance Scheme.isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.J) :
     IsAffine (𝒰.openCover.obj i) :=
   inferInstanceAs (IsAffine (Spec (𝒰.obj i)))
 
+instance {X} [IsAffine X] (i) : IsAffine ((Scheme.openCoverOfIsIso (𝟙 X)).obj i) := by
+  dsimp; infer_instance
+
 theorem isBasis_affine_open (X : Scheme) : Opens.IsBasis X.affineOpens := by
   rw [Opens.isBasis_iff_nbhd]
   rintro U x (hU : x ∈ (U : Set X))
@@ -325,6 +328,12 @@ theorem image_of_isOpenImmersion (f : X ⟶ Y) [H : IsOpenImmersion f] :
   exact Set.image_eq_range _ _
 #align algebraic_geometry.is_affine_open.image_is_open_immersion AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion
 
+theorem preimage_of_isIso {U : Opens Y.carrier} (hU : IsAffineOpen U) (f : X ⟶ Y) [IsIso f] :
+    IsAffineOpen (f ⁻¹ᵁ U) :=
+  haveI : IsAffine _ := hU
+  isAffine_of_isIso (f ∣_ U)
+#align algebraic_geometry.is_affine_open.map_is_iso AlgebraicGeometry.IsAffineOpen.preimage_of_isIso
+
 theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
     (f : AlgebraicGeometry.Scheme.Hom X Y) [H : IsOpenImmersion f] {U : Opens X} :
     IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U := by
@@ -435,6 +444,9 @@ theorem basicOpen :
   exact Opens.ext (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm
 #align algebraic_geometry.is_affine_open.basic_open_is_affine AlgebraicGeometry.IsAffineOpen.basicOpen
 
+instance [IsAffine X] (r : Γ(X, ⊤)) : IsAffine (X ∣_ᵤ X.basicOpen r) :=
+  (isAffineOpen_top X).basicOpen _
+
 theorem ιOpens_basicOpen_preimage (r : Γ(X, ⊤)) :
     IsAffineOpen (Scheme.ιOpens (X.basicOpen r) ⁻¹ᵁ U) := by
   apply (Scheme.ιOpens (X.basicOpen r)).isAffineOpen_iff_of_isOpenImmersion.mp

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -192,6 +192,15 @@ def OpenCover.pullbackCover {X W : Scheme.{u}} (𝒰 : X.OpenCover) (f : W ⟶ X
     · rw [← TopCat.epi_iff_surjective]; infer_instance
 #align algebraic_geometry.Scheme.open_cover.pullback_cover AlgebraicGeometry.Scheme.OpenCover.pullbackCover
 
+/-- The family of morphisms from the pullback cover to the original cover. -/
+def OpenCover.pullbackHom {X W : Scheme.{u}} (𝒰 : X.OpenCover) (f : W ⟶ X) (i) :
+    (𝒰.pullbackCover f).obj i ⟶ 𝒰.obj i :=
+  pullback.snd f (𝒰.map i)
+
+@[reassoc (attr := simp)]
+lemma OpenCover.pullbackHom_map {X W : Scheme.{u}} (𝒰 : X.OpenCover) (f : W ⟶ X) (i) :
+    𝒰.pullbackHom f i ≫ 𝒰.map i = (𝒰.pullbackCover f).map i ≫ f := pullback.condition.symm
+
 /-- Given an open cover on `X`, we may pull them back along a morphism `f : W ⟶ X` to obtain
 an open cover of `W`. This is similar to `Scheme.OpenCover.pullbackCover`, but here we
 take `pullback (𝒰.map x) f` instead of `pullback f (𝒰.map x)`. -/
@@ -337,6 +346,41 @@ def OpenCover.affineRefinement {X : Scheme.{u}} (𝓤 : X.OpenCover) : X.AffineO
   f := (𝓤.bind fun j => (𝓤.obj j).affineCover).f
   covers := (𝓤.bind fun j => (𝓤.obj j).affineCover).covers
 
+/-- The pullback of the affine refinement is the pullback of the affine cover. -/
+def OpenCover.pullbackCoverAffineRefinementObjIso (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i) :
+    (𝒰.affineRefinement.openCover.pullbackCover f).obj i ≅
+      ((𝒰.obj i.1).affineCover.pullbackCover (𝒰.pullbackHom f i.1)).obj i.2 :=
+  pullbackSymmetry _ _ ≪≫ (pullbackRightPullbackFstIso _ _ _).symm ≪≫
+    pullbackSymmetry _ _ ≪≫ asIso (pullback.map _ _ _ _ (pullbackSymmetry _ _).hom (𝟙 _) (𝟙 _)
+      (by simp [pullbackHom]) (by simp))
+
+@[reassoc]
+lemma OpenCover.pullbackCoverAffineRefinementObjIso_inv_map (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i) :
+    (𝒰.pullbackCoverAffineRefinementObjIso f i).inv ≫
+      (𝒰.affineRefinement.openCover.pullbackCover f).map i =
+      ((𝒰.obj i.1).affineCover.pullbackCover (𝒰.pullbackHom f i.1)).map i.2 ≫
+        (𝒰.pullbackCover f).map i.1 := by
+  simp only [pullbackCover_obj, AffineOpenCover.openCover_obj, AffineOpenCover.openCover_map,
+    pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv, Iso.symm_inv, Category.assoc,
+    pullbackCover_map, pullbackSymmetry_inv_comp_fst, IsIso.inv_comp_eq, limit.lift_π_assoc, id_eq,
+    PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app, pullbackSymmetry_hom_comp_fst]
+  convert pullbackSymmetry_inv_comp_snd_assoc
+    ((𝒰.obj i.1).affineCover.map i.2) (pullback.fst _ _) _ using 2
+  exact pullbackRightPullbackFstIso_hom_snd _ _ _
+
+@[reassoc]
+lemma OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom
+    (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i) :
+    (𝒰.pullbackCoverAffineRefinementObjIso f i).inv ≫
+      𝒰.affineRefinement.openCover.pullbackHom f i =
+      (𝒰.obj i.1).affineCover.pullbackHom (𝒰.pullbackHom f i.1) i.2 := by
+  simp only [pullbackCover_obj, pullbackHom, AffineOpenCover.openCover_obj,
+    AffineOpenCover.openCover_map, pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv,
+    Iso.symm_inv, Category.assoc, pullbackSymmetry_inv_comp_snd, IsIso.inv_comp_eq, limit.lift_π,
+    id_eq, PullbackCone.mk_pt, PullbackCone.mk_π_app, Category.comp_id]
+  convert pullbackSymmetry_inv_comp_fst ((𝒰.obj i.1).affineCover.map i.2) (pullback.fst _ _)
+  exact pullbackRightPullbackFstIso_hom_fst _ _ _
+
 section category
 
 /--