feat(algebraic_geometry/morphisms/basic): Morphism properties on the diagonal morphism. (#16111)

Author: erdOne

src/algebraic_geometry/morphisms/basic.lean

@@ -436,4 +436,128 @@ end
 
 end affine_target_morphism_property
 
+/--
+The `affine_target_morphism_property` associated to `(target_affine_locally P).diagonal`.
+See `diagonal_target_affine_locally_eq_target_affine_locally`.
+-/
+def affine_target_morphism_property.diagonal (P : affine_target_morphism_property) :
+  affine_target_morphism_property :=
+λ X Y f hf, ∀ {U₁ U₂ : Scheme} (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [is_affine U₁] [is_affine U₂]
+  [is_open_immersion f₁] [is_open_immersion f₂],
+  by exactI P (pullback.map_desc f₁ f₂ f)
+
+lemma affine_target_morphism_property.diagonal_respects_iso (P : affine_target_morphism_property)
+  (hP : P.to_property.respects_iso) :
+  P.diagonal.to_property.respects_iso :=
+begin
+  delta affine_target_morphism_property.diagonal,
+  apply affine_target_morphism_property.respects_iso_mk,
+  { introv H _ _,
+    resetI,
+    rw [pullback.map_desc_comp, affine_cancel_left_is_iso hP, affine_cancel_right_is_iso hP],
+    apply H },
+  { introv H _ _,
+    resetI,
+    rw [pullback.map_desc_comp, affine_cancel_right_is_iso hP],
+    apply H }
+end
+
+lemma diagonal_target_affine_locally_of_open_cover (P : affine_target_morphism_property)
+  (hP : P.is_local)
+  {X Y : Scheme.{u}} (f : X ⟶ Y)
+  (𝒰 : Scheme.open_cover.{u} Y)
+  [∀ i, is_affine (𝒰.obj i)] (𝒰' : Π i, Scheme.open_cover.{u} (pullback f (𝒰.map i)))
+  [∀ i j, is_affine ((𝒰' i).obj j)]
+  (h𝒰' : ∀ i j k, P (pullback.map_desc ((𝒰' i).map j) ((𝒰' i).map k) pullback.snd)) :
+    (target_affine_locally P).diagonal f :=
+begin
+  refine (hP.affine_open_cover_iff _ _).mpr _,
+  { exact ((Scheme.pullback.open_cover_of_base 𝒰 f f).bind (λ i,
+      Scheme.pullback.open_cover_of_left_right.{u u} (𝒰' i) (𝒰' i) pullback.snd pullback.snd)) },
+  { intro i,
+    dsimp at *,
+    apply_instance },
+  { rintro ⟨i, j, k⟩,
+    dsimp,
+    convert (affine_cancel_left_is_iso hP.1
+    (pullback_diagonal_map_iso _ _ ((𝒰' i).map j) ((𝒰' i).map k)).inv pullback.snd).mp _,
+    swap 3,
+    { convert h𝒰' i j k, apply pullback.hom_ext; simp, },
+    all_goals
+    { apply pullback.hom_ext; simp only [category.assoc, pullback.lift_fst, pullback.lift_snd,
+      pullback.lift_fst_assoc, pullback.lift_snd_assoc] } }
+end
+
+lemma affine_target_morphism_property.diagonal_of_target_affine_locally
+  (P : affine_target_morphism_property)
+  (hP : P.is_local) {X Y U : Scheme.{u}} (f : X ⟶ Y) (g : U ⟶ Y)
+  [is_affine U] [is_open_immersion g] (H : (target_affine_locally P).diagonal f) :
+    P.diagonal (pullback.snd : pullback f g ⟶ _) :=
+begin
+  rintros U V f₁ f₂ _ _ _ _,
+  resetI,
+  replace H := ((hP.affine_open_cover_tfae (pullback.diagonal f)).out 0 3).mp H,
+  let g₁ := pullback.map (f₁ ≫ pullback.snd)
+    (f₂ ≫ pullback.snd) f f
+    (f₁ ≫ pullback.fst)
+    (f₂ ≫ pullback.fst) g
+    (by rw [category.assoc, category.assoc, pullback.condition])
+    (by rw [category.assoc, category.assoc, pullback.condition]),
+  let g₂ : pullback f₁ f₂ ⟶ pullback f g := pullback.fst ≫ f₁,
+  specialize H g₁,
+  rw ← affine_cancel_left_is_iso hP.1 (pullback_diagonal_map_iso f _ f₁ f₂).hom,
+  convert H,
+  { apply pullback.hom_ext; simp only [category.assoc, pullback.lift_fst, pullback.lift_snd,
+    pullback.lift_fst_assoc, pullback.lift_snd_assoc, category.comp_id,
+    pullback_diagonal_map_iso_hom_fst, pullback_diagonal_map_iso_hom_snd], }
+end
+
+lemma affine_target_morphism_property.is_local.diagonal_affine_open_cover_tfae
+  {P : affine_target_morphism_property}
+  (hP : P.is_local) {X Y : Scheme.{u}} (f : X ⟶ Y) :
+  tfae [(target_affine_locally P).diagonal f,
+    ∃ (𝒰 : Scheme.open_cover.{u} Y) [∀ i, is_affine (𝒰.obj i)], by exactI
+      ∀ (i : 𝒰.J), P.diagonal (pullback.snd : pullback f (𝒰.map i) ⟶ _),
+    ∀ (𝒰 : Scheme.open_cover.{u} Y) [∀ i, is_affine (𝒰.obj i)] (i : 𝒰.J), by exactI
+      P.diagonal (pullback.snd : pullback f (𝒰.map i) ⟶ _),
+    ∀ {U : Scheme} (g : U ⟶ Y) [is_affine U] [is_open_immersion g], by exactI
+      P.diagonal (pullback.snd : pullback f g ⟶ _),
+    ∃ (𝒰 : Scheme.open_cover.{u} Y) [∀ i, is_affine (𝒰.obj i)]
+      (𝒰' : Π i, Scheme.open_cover.{u} (pullback f (𝒰.map i))) [∀ i j, is_affine ((𝒰' i).obj j)],
+    by exactI ∀ i j k, P (pullback.map_desc ((𝒰' i).map j) ((𝒰' i).map k) pullback.snd)] :=
+begin
+  tfae_have : 1 → 4,
+  { introv H hU hg _ _, resetI, apply P.diagonal_of_target_affine_locally; assumption },
+  tfae_have : 4 → 3,
+  { introv H h𝒰, resetI, apply H },
+  tfae_have : 3 → 2,
+  { exact λ H, ⟨Y.affine_cover, infer_instance, H Y.affine_cover⟩ },
+  tfae_have : 2 → 5,
+  { rintro ⟨𝒰, h𝒰, H⟩,
+    resetI,
+    refine ⟨𝒰, infer_instance, λ _, Scheme.affine_cover _, infer_instance, _⟩,
+    intros i j k,
+    apply H },
+  tfae_have : 5 → 1,
+  { rintro ⟨𝒰, _, 𝒰', _, H⟩,
+    exactI diagonal_target_affine_locally_of_open_cover P hP f 𝒰 𝒰' H, },
+  tfae_finish
+end
+
+lemma affine_target_morphism_property.is_local.diagonal {P : affine_target_morphism_property}
+  (hP : P.is_local) : P.diagonal.is_local :=
+affine_target_morphism_property.is_local_of_open_cover_imply
+  P.diagonal
+  (P.diagonal_respects_iso hP.1)
+  (λ _ _ f, ((hP.diagonal_affine_open_cover_tfae f).out 1 3).mp)
+
+lemma diagonal_target_affine_locally_eq_target_affine_locally (P : affine_target_morphism_property)
+  (hP : P.is_local) :
+  (target_affine_locally P).diagonal = target_affine_locally P.diagonal :=
+begin
+  ext _ _ f,
+  exact ((hP.diagonal_affine_open_cover_tfae f).out 0 1).trans
+    ((hP.diagonal.affine_open_cover_tfae f).out 1 0),
+end
+
 end algebraic_geometry

src/algebraic_geometry/pullbacks.lean

@@ -5,7 +5,8 @@ Authors: Andrew Yang
 -/
 import algebraic_geometry.gluing
 import category_theory.limits.opposites
-import algebraic_geometry.Gamma_Spec_adjunction
+import algebraic_geometry.AffineScheme
+import category_theory.limits.shapes.diagonal
 
 /-!
 # Fibred products of schemes
@@ -245,7 +246,8 @@ def gluing : Scheme.glue_data.{u} :=
   t_fac := λ i j k, begin
     apply pullback.hom_ext,
     apply pullback.hom_ext,
-    all_goals { simp }
+    all_goals { simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd,
+      t_fst_fst, t_fst_snd, t_snd, category.assoc] }
   end,
   cocycle := λ i j k, cocycle 𝒰 f g i j k }
 
@@ -558,6 +560,13 @@ has_pullback_of_cover (Z.affine_cover.pullback_cover f) f g
 
 instance : has_pullbacks Scheme := has_pullbacks_of_has_limit_cospan _
 
+instance {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [is_affine X] [is_affine Y] [is_affine Z] :
+  is_affine (pullback f g) :=
+is_affine_of_iso (pullback.map f g (Spec.map (Γ.map f.op).op) (Spec.map (Γ.map g.op).op)
+  (Γ_Spec.adjunction.unit.app X) (Γ_Spec.adjunction.unit.app Y) (Γ_Spec.adjunction.unit.app Z)
+  (Γ_Spec.adjunction.unit.naturality f) (Γ_Spec.adjunction.unit.naturality g) ≫
+    (preserves_pullback.iso Spec _ _).inv)
+
 /-- Given an open cover `{ Xᵢ }` of `X`, then `X ×[Z] Y` is covered by `Xᵢ ×[Z] Y`. -/
 @[simps J obj map]
 def open_cover_of_left (𝒰 : open_cover X) (f : X ⟶ Z) (g : Y ⟶ Z) : open_cover (pullback f g) :=
@@ -592,6 +601,23 @@ begin
   apply pullback.hom_ext; simp,
 end
 
+/-- Given an open cover `{ Xᵢ }` of `X` and an open cover `{ Yⱼ }` of `Y`, then
+`X ×[Z] Y` is covered by `Xᵢ ×[Z] Yⱼ`. -/
+@[simps J obj map]
+def open_cover_of_left_right (𝒰X : X.open_cover) (𝒰Y : Y.open_cover)
+  (f : X ⟶ Z) (g : Y ⟶ Z) : (pullback f g).open_cover :=
+begin
+  fapply ((open_cover_of_left 𝒰X f g).bind (λ x, open_cover_of_right 𝒰Y (𝒰X.map x ≫ f) g)).copy
+    (𝒰X.J × 𝒰Y.J)
+    (λ ij, pullback (𝒰X.map ij.1 ≫ f) (𝒰Y.map ij.2 ≫ g))
+    (λ ij, pullback.map _ _ _ _ (𝒰X.map ij.1) (𝒰Y.map ij.2) (𝟙 _)
+      (category.comp_id _) (category.comp_id _))
+    (equiv.sigma_equiv_prod _ _).symm
+    (λ _, iso.refl _),
+  rintro ⟨i, j⟩,
+  apply pullback.hom_ext; simpa,
+end
+
 /-- (Implementation). Use `open_cover_of_base` instead. -/
 def open_cover_of_base' (𝒰 : open_cover Z) (f : X ⟶ Z) (g : Y ⟶ Z) : open_cover (pullback f g) :=
 begin
@@ -639,3 +665,16 @@ end
 end pullback
 
 end algebraic_geometry.Scheme
+
+namespace algebraic_geometry
+
+instance {X Y S X' Y' S' : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S')
+  (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f')
+  (e₂ : g ≫ i₃ = i₂ ≫ g') [is_open_immersion i₁] [is_open_immersion i₂] [mono i₃] :
+  is_open_immersion (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) :=
+begin
+  rw pullback_map_eq_pullback_fst_fst_iso_inv,
+  apply_instance
+end
+
+end algebraic_geometry

src/category_theory/limits/shapes/pullbacks.lean

@@ -946,6 +946,12 @@ abbreviation pullback.map {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [h
 pullback.lift (pullback.fst ≫ i₁) (pullback.snd ≫ i₂)
   (by simp [← eq₁, ← eq₂, pullback.condition_assoc])
 
+/-- The canonical map `X ×ₛ Y ⟶ X ×ₜ Y` given `S ⟶ T`. -/
+abbreviation pullback.map_desc {X Y S T : C} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T)
+  [has_pullback f g] [has_pullback (f ≫ i) (g ≫ i)] :
+  pullback f g ⟶ pullback (f ≫ i) (g ≫ i) :=
+pullback.map f g (f ≫ i) (g ≫ i) (𝟙 _) (𝟙 _) i (category.id_comp _).symm (category.id_comp _).symm
+
 
 /--
 Given such a diagram, then there is a natural morphism `W ⨿ₛ X ⟶ Y ⨿ₜ Z`.
@@ -963,6 +969,11 @@ abbreviation pushout.map {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X) [ha
 pushout.desc (i₁ ≫ pushout.inl) (i₂ ≫ pushout.inr)
   (by { simp only [← category.assoc, eq₁, eq₂], simp [pushout.condition] })
 
+/-- The canonical map `X ⨿ₛ Y ⟶ X ⨿ₜ Y` given `S ⟶ T`. -/
+abbreviation pushout.map_lift {X Y S T : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T)
+  [has_pushout f g] [has_pushout (i ≫ f) (i ≫ g)] :
+  pushout (i ≫ f) (i ≫ g) ⟶ pushout f g :=
+pushout.map (i ≫ f) (i ≫ g) f g (𝟙 _) (𝟙 _) i (category.comp_id _) (category.comp_id _)
 
 /-- Two morphisms into a pullback are equal if their compositions with the pullback morphisms are
     equal -/
@@ -1077,6 +1088,13 @@ begin
   tidy
 end
 
+lemma pullback.map_desc_comp {X Y S T S' : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S)
+  (i' : S ⟶ S') [has_pullback f g] [has_pullback (f ≫ i) (g ≫ i)]
+  [has_pullback (f ≫ i ≫ i') (g ≫ i ≫ i')] [has_pullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')] :
+  pullback.map_desc f g (i ≫ i') = pullback.map_desc f g i ≫ pullback.map_desc _ _ i' ≫
+    (pullback.congr_hom (category.assoc _ _ _) (category.assoc _ _ _)).hom :=
+by { ext; simp }
+
 /-- If `f₁ = f₂` and `g₁ = g₂`, we may construct a canonical
 isomorphism `pushout f₁ g₁ ≅ pullback f₂ g₂` -/
 @[simps hom]
@@ -1102,6 +1120,14 @@ begin
     rw category.id_comp }
 end
 
+lemma pushout.map_lift_comp {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T)
+  (i' : S' ⟶ S) [has_pushout f g] [has_pushout (i ≫ f) (i ≫ g)]
+  [has_pushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)] [has_pushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)] :
+  pushout.map_lift f g (i' ≫ i) =
+    (pushout.congr_hom (category.assoc _ _ _) (category.assoc _ _ _)).hom ≫
+    pushout.map_lift _ _ i' ≫ pushout.map_lift f g i :=
+by { ext; simp }
+
 section
 
 variables (G : C ⥤ D)

src/category_theory/morphism_property.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import category_theory.limits.shapes.pullbacks
+import category_theory.limits.shapes.diagonal
 import category_theory.arrow
 import category_theory.limits.shapes.comm_sq
 
@@ -373,6 +373,53 @@ full_subcategory (λ (F : C ⥤ D), W.is_inverted_by F)
 def functors_inverting.mk {W : morphism_property C} {D : Type*} [category D]
 (F : C ⥤ D) (hF : W.is_inverted_by F) : W.functors_inverting D := ⟨F, hF⟩
 
+section diagonal
+
+variables [has_pullbacks C] {P : morphism_property C}
+
+/-- For `P : morphism_property C`, `P.diagonal` is a morphism property that holds for `f : X ⟶ Y`
+whenever `P` holds for `X ⟶ Y xₓ Y`. -/
+def diagonal (P : morphism_property C) : morphism_property C :=
+λ X Y f, P (pullback.diagonal f)
+
+lemma diagonal_iff {X Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (pullback.diagonal f) := iff.rfl
+
+lemma respects_iso.diagonal (hP : P.respects_iso) : P.diagonal.respects_iso :=
+begin
+  split,
+  { introv H,
+    rwa [diagonal_iff, pullback.diagonal_comp, hP.cancel_left_is_iso, hP.cancel_left_is_iso,
+      ← hP.cancel_right_is_iso _ _, ← pullback.condition, hP.cancel_left_is_iso],
+    apply_instance },
+  { introv H,
+    delta diagonal,
+    rwa [pullback.diagonal_comp, hP.cancel_right_is_iso] }
+end
+
+lemma stable_under_composition.diagonal
+  (hP : stable_under_composition P) (hP' : respects_iso P) (hP'' : stable_under_base_change P) :
+  P.diagonal.stable_under_composition :=
+begin
+  introv X h₁ h₂,
+  rw [diagonal_iff, pullback.diagonal_comp],
+  apply hP, { assumption },
+  rw hP'.cancel_left_is_iso,
+  apply hP''.snd,
+  assumption
+end
+
+lemma stable_under_base_change.diagonal
+  (hP : stable_under_base_change P) (hP' : respects_iso P) :
+  P.diagonal.stable_under_base_change :=
+stable_under_base_change.mk hP'.diagonal
+begin
+  introv h,
+  rw [diagonal_iff, diagonal_pullback_fst, hP'.cancel_left_is_iso, hP'.cancel_right_is_iso],
+  convert hP.base_change_map f _ _; simp; assumption
+end
+
+end diagonal
+
 end morphism_property
 
 end category_theory