19.8. Reduction to the affine case🔗

The most important technique in scheme theory is certainly the reduction to affine situations and commutative algebra. We first explain a few of the basic tools for this and then give an example how these can be used to prove a standard fact.

19.8.1. (Open) covers🔗

Any reduction to a local problem starts with an (affine) open cover. These can be pulled back along morphisms, refined, etc.

AlgebraicGeometry.Scheme.OpenCover.{v, u} (X : Scheme) : Type (max (v + 1) (u + 1))#check Scheme.OpenCover

Pullback an open cover along an arbitrary morphism:

example (f : X ⟶ Y) (𝒰 : Y.OpenCover) : X.OpenCover :=
  𝒰.pullback₁ f

Refine every component of an open cover by an open cover:

example (𝒰 : X.OpenCover) (𝒱 : ∀ i, (𝒰.X i).OpenCover) :
    X.OpenCover :=
  𝒰.bind 𝒱

A choice of affine cover of X.

example (X : Scheme) : X.OpenCover :=
  X.affineCover

The components of X.affineCover are definitionally equal to some Spec R for some R.

example (X : Scheme) (i : X.affineCover.I₀) :
    ∃ R, X.affineCover.X i = Spec R :=
  ⟨_, rfl⟩

19.8.2. Example🔗

The goal of this section is to define flat morphisms of schemes and to prove that a morphism is flat if it is stalkwise flat.

Here is a definition of a flat morphism of schemes: A morphism of schemes f : X \to Y is flat if for every affine open U \subseteq Y and V \subseteq f^{-1}(U), the induced ring homomorphism \mathcal{O}_Y(U) \to \mathcal{O}_X(V) is flat.

@[mk_iff]
class Flat (f : X ⟶ Y) : Prop where
  flat_of_isAffineOpen :
    ∀ (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U),
      IsAffineOpen U → IsAffineOpen V →
      (f.appLE U V e).hom.Flat

To connect flat morphisms of schemes to ring homomorphism, we need to provide an instance of HasRingHomProperty:

instance :
    HasRingHomProperty @Flat RingHom.Flat where
  isLocal_ringHomProperty := RingHom.Flat.propertyIsLocal
  eq_affineLocally' := byR:TypeS:TypeT:Typeinst✝¹:CommRing Rinst✝:CommRing SP:MorphismProperty SchemeX:SchemeY:Scheme⊢ @Flat = affineLocally fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
    ext X Y fR:TypeS:TypeT:Typeinst✝¹:CommRing Rinst✝:CommRing SP:MorphismProperty SchemeX✝:SchemeY✝:SchemeX:SchemeY:Schemef:X ⟶ Y⊢ Flat f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] => RingHom.Flat) f
    rw [flat_iff,R:TypeS:TypeT:Typeinst✝¹:CommRing Rinst✝:CommRing SP:MorphismProperty SchemeX✝:SchemeY✝:SchemeX:SchemeY:Schemef:X ⟶ Y⊢ (∀ (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U),
    IsAffineOpen U → IsAffineOpen V → (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
  affineLocally (fun {R S} [CommRing R] [CommRing S] => RingHom.Flat) f affineLocally_iff_affineOpens_leR:TypeS:TypeT:Typeinst✝¹:CommRing Rinst✝:CommRing SP:MorphismProperty SchemeX✝:SchemeY✝:SchemeX:SchemeY:Schemef:X ⟶ Y⊢ (∀ (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U),
    IsAffineOpen U → IsAffineOpen V → (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).Flat]R:TypeS:TypeT:Typeinst✝¹:CommRing Rinst✝:CommRing SP:MorphismProperty SchemeX✝:SchemeY✝:SchemeX:SchemeY:Schemef:X ⟶ Y⊢ (∀ (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U),
    IsAffineOpen U → IsAffineOpen V → (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).Flat
    simp only [Scheme.affineOpens, Set.coe_setOf,
      Set.mem_setOf_eq, Subtype.forall]R:TypeS:TypeT:Typeinst✝¹:CommRing Rinst✝:CommRing SP:MorphismProperty SchemeX✝:SchemeY✝:SchemeX:SchemeY:Schemef:X ⟶ Y⊢ (∀ (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U),
    IsAffineOpen U → IsAffineOpen V → (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
  ∀ (a : Y.Opens) (b : IsAffineOpen a) (a_1 : X.Opens) (b_1 : IsAffineOpen a_1) (e : a_1 ≤ f ⁻¹ᵁ a),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f a a_1 e)).Flat
    grindAll goals completed! 🐙

After this, we get some meta properties for free, for example that flat is local on the target:

example : IsZariskiLocalAtTarget @Flat :=
  inferInstance

With these preparations, we can now prove that a morphism that is stalkwise flat is flat:

theorem flat_of_flat_stalkMap (f : X ⟶ Y)
    (H : ∀ x, (f.stalkMap x).hom.Flat) :
    Flat f := byX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat⊢ Flat f
  -- We may assume `Y` is of the form `Spec R`
  wlog hY : ∃ R, Y = Spec R generalizing X Y finrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec R⊢ Flat fX✝:SchemeY✝:SchemeX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FlathY:∃ R, Y = Spec R⊢ Flat f
  ·inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec R⊢ Flat f rw [IsZariskiLocalAtTarget.iff_of_openCover
      (P := @Flat) Y.affineCoverinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec R⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Flat (Scheme.Cover.pullbackHom Y.affineCover f i)]inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec R⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Flat (Scheme.Cover.pullbackHom Y.affineCover f i)
    intro iinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1⊢ Flat (Scheme.Cover.pullbackHom Y.affineCover f i)
    refine this _ ?_ ⟨_, rfl⟩inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1⊢ ∀ (x : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)),
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Cover.pullbackHom Y.affineCover f i) x)).Flat
    intro xinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Cover.pullbackHom Y.affineCover f i) x)).Flat
    rw [RingHom.Flat.respectsIso.arrow_mk_iso_iffinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ (CommRingCat.Hom.hom ?m.67).FlatinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ Arrow.mk (Scheme.Hom.stalkMap (Scheme.Cover.pullbackHom Y.affineCover f i) x) ≅ Arrow.mk ?m.67X:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ CommRingCatX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ CommRingCatX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ ?m.64 ⟶ ?m.65]inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ (CommRingCat.Hom.hom ?m.67).FlatinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ Arrow.mk (Scheme.Hom.stalkMap (Scheme.Cover.pullbackHom Y.affineCover f i) x) ≅ Arrow.mk ?m.67X:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ CommRingCatX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ CommRingCatX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ ?m.64 ⟶ ?m.65
    ·inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ (CommRingCat.Hom.hom ?m.67).Flat apply HinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ ↥X
      bdsimp at xinrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥(pullback f (Y.affineCover.f i))⊢ ↥X
      exact pullback.fst f _ xAll goals completed! 🐙
    ·inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ Arrow.mk (Scheme.Hom.stalkMap (Scheme.Cover.pullbackHom Y.affineCover f i) x) ≅
  Arrow.mk (Scheme.Hom.stalkMap f ((pullback.fst f (Y.affineCover.f i)) x)) dsimp [Scheme.Cover.pullbackHom]inrX:SchemeY:Schemef:X ⟶ YH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X Y : Scheme} (f : X ⟶ Y),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ R, Y = Spec R) → Flat fhY:¬∃ R, Y = Spec Ri:Y.affineCover.toPreZeroHypercover.1x:↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)⊢ Arrow.mk (Scheme.Hom.stalkMap (pullback.snd f (Y.affineCover.f i)) x) ≅
  Arrow.mk (Scheme.Hom.stalkMap f ((pullback.fst f (Y.affineCover.f i)) x))
      apply Iso.symm <| Scheme.stalkMapIsoOfIsPullback
        (IsPullback.of_hasPullback _ (Y.affineCover.f i)) _All goals completed! 🐙
  -- Replace `Y` by `Spec R` in the context and goal.
  obtain ⟨R, rfl⟩ := hYX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat⊢ Flat f
  wlog hX : ∃ S, X = Spec S generalizing X finrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec S⊢ Flat fX✝:SchemeY:SchemeR:CommRingCatX:Schemef:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FlathX:∃ S, X = Spec S⊢ Flat f
  ·inrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec S⊢ Flat f rw [IsZariskiLocalAtSource.iff_of_openCover
      (P := @Flat) X.affineCoverinrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec S⊢ ∀ (i : X.affineCover.I₀), Flat (X.affineCover.f i ≫ f)]inrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec S⊢ ∀ (i : X.affineCover.I₀), Flat (X.affineCover.f i ≫ f)
    intro iinrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀⊢ Flat (X.affineCover.f i ≫ f)
    refine this _ ?_ ⟨_, rfl⟩inrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀⊢ ∀ (x : ↥(X.affineCover.X i)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.affineCover.f i ≫ f) x)).Flat
    intro xinrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀x:↥(X.affineCover.X i)⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.affineCover.f i ≫ f) x)).Flat
    rw [Scheme.Hom.stalkMap_comp,inrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀x:↥(X.affineCover.X i)⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((X.affineCover.f i) x) ≫ Scheme.Hom.stalkMap (X.affineCover.f i) x)).Flat CommRingCat.hom_comp,inrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀x:↥(X.affineCover.X i)⊢ ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.affineCover.f i) x)).comp
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((X.affineCover.f i) x)))).Flat
      RingHom.Flat.respectsIso.cancel_right_isIsoinrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀x:↥(X.affineCover.X i)⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((X.affineCover.f i) x))).Flat]inrX✝:SchemeY:SchemeX:SchemeR:CommRingCatf:X ⟶ Spec RH:∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flatthis:∀ {X : Scheme} (f : X ⟶ Spec R),
  (∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) → (∃ S, X = Spec S) → Flat fhX:¬∃ S, X = Spec Si:X.affineCover.I₀x:↥(X.affineCover.X i)⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f ((X.affineCover.f i) x))).Flat
    apply HAll goals completed! 🐙
  -- Replace `X` by `Spec S` in the context and goal.
  obtain ⟨S, rfl⟩ := hXX:SchemeY:SchemeR:CommRingCatS:CommRingCatf:Spec S ⟶ Spec RH:∀ (x : ↥(Spec S)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat⊢ Flat f
  -- Replace `f` by `Spec.map φ` in the context and goal.
  obtain ⟨φ, rfl⟩ := Spec.map_surjective fX:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SH:∀ (x : ↥(Spec S)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x)).Flat⊢ Flat (Spec.map φ)
  /- Since we have shown before that flat morphisms of
  schemes correspond to flat ring homomorphisms, we can now
  turn the goal into commutative algebra. -/
  rw [HasRingHomProperty.Spec_iff (P := @Flat)X:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SH:∀ (x : ↥(Spec S)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x)).Flat⊢ (CommRingCat.Hom.hom φ).Flat]X:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SH:∀ (x : ↥(Spec S)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x)).Flat⊢ (CommRingCat.Hom.hom φ).Flat
  /- Finally, use the fact from commutative algebra, that
  flatness of ring maps can be checked on stalks. -/
  apply RingHom.Flat.ofLocalizationPrimeX:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SH:∀ (x : ↥(Spec S)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x)).Flat⊢ ∀ (J : Ideal ↑S) (x : J.IsPrime),
  (fun {R S} [CommRing R] [CommRing S] => RingHom.Flat)
    (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) J) J (CommRingCat.Hom.hom φ) ⋯)
  intro P hPX:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SH:∀ (x : ↥(Spec S)), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x)).FlatP:Ideal ↑ShP:P.IsPrime⊢ (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯).Flat
  specialize H ⟨P, hP⟩X:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SP:Ideal ↑ShP:P.IsPrimeH:(CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP })).Flat⊢ (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯).Flat
  rwa [RingHom.Flat.respectsIso.arrow_mk_iso_iff
    (Scheme.arrowStalkMapSpecIso φ _)X:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SP:Ideal ↑ShP:P.IsPrimeH:(CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) { asIdeal := P, isPrime := hP }).asIdeal
        { asIdeal := P, isPrime := hP }.asIdeal (CommRingCat.Hom.hom φ) ⋯))).Flat⊢ (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯).Flat]X:SchemeY:SchemeR:CommRingCatS:CommRingCatφ:R ⟶ SP:Ideal ↑ShP:P.IsPrimeH:(CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) { asIdeal := P, isPrime := hP }).asIdeal
        { asIdeal := P, isPrime := hP }.asIdeal (CommRingCat.Hom.hom φ) ⋯))).Flat⊢ (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯).Flat at H