making a locally ringed space

Stream: mathlib4

[Kevin Buzzard]

In discussions with @FMLJohn I realised that I didn't know any good examples of locally ringed spaces that weren't schemes, so I tried to come up with one. My idea: X is the two point set, give it the topology such that one element is open and the other is closed, and define a sheaf of rings by letting A be a commutative R-algebra and defining the global sections to be R, the sections on {open point} to be A and the sections on the empty set to be Unit. If furthermore A and R are local (and the map between them certainly might not be a local homomorphism) then my guess is that this is a locally-ringed space!

I thought I'd check this in Lean. My first problem was choosing a two-element set. I first went with Prop because I saw it had the Sierpinski topology on it. I then realised I couldn't prove that {False} wasn't open! I got this far before losing interest:

example (U : Set Prop) : IsOpen U → U ≠ {False} := by
  classical
  intro h
  refine TopologicalSpace.GenerateOpen.rec ?_ ?_ ?_ ?_ h
  · aesop
  · have foo : True ∈ Set.univ := by simp only [Set.mem_univ]
    intro h
    rw [h] at foo
    simp at foo
  · intros S T h1 h2 h3 h4
    intro h
    have hST : True ∉ S ∩ T := by simp [h]
    have hST2 : False ∈ S ∩ T := by simp [h]
    by_cases hS : True ∈ S
    · apply h4
      ext P
      rcases Classical.propComplete P with (rfl | rfl)
      · simp [mt (Set.mem_inter hS) hST]
      · cases hST2
        simp_all
    · apply h3
      ext P
      rcases Classical.propComplete P with (rfl | rfl)
      aesop
      simp [hST2.1]
  · intro ι hι hFalse
    intro h
    -- need sUnion_eq_singleton
    sorry

lemma not_open_false : ¬ IsOpen ({False} : Set Prop) := by sorry -- follows from the above

and at that point I decided to move onto Bool, where I did get a bit further:

import Mathlib.AlgebraicGeometry.Scheme

-- remove all mention of the usual topology on Bool
attribute [-instance] instTopologicalSpaceBool instUniformSpaceBool

namespace Bool

inductive IsOpen : Set Bool → Prop
| bot : IsOpen ⊥
| top : IsOpen ⊤
| true : IsOpen {true}

@[simp, aesop safe]
lemma IsOpen_def (U : Set Bool) :
    IsOpen U ↔ U = {} ∨ U = {true, false} ∨ U = {true} := by
  constructor
  · rintro (h | h | h) <;> aesop
  · rintro (rfl | rfl | rfl)
    · exact IsOpen.bot
    · convert IsOpen.top
      ext
      simp
    · exact IsOpen.true

instance : TopologicalSpace Bool where
  IsOpen := IsOpen
  isOpen_univ := IsOpen.top
  isOpen_inter S T := by aesop
  isOpen_sUnion := by
    intro ι hι
    sorry -- can't get automation to do this

instance : DecidableEq (Set Bool) := sorry -- aargh

instance : DecidableEq (TopologicalSpace.Opens Bool) := sorry -- aargh

-- R,A rings, R -> A a map, A is the value on eta, R is the global secions
variable (R A : Type) [CommRing R] [CommRing A] [Algebra R A]

-- objects
open CommRingCat in
noncomputable def f (U : TopologicalSpace.Opens Bool) :
    CommRingCat := if U = ⊥ then of Unit else if U = ⊤ then of R else of A

-- #synth IsScalarTower R A Unit -- this works, and that's the diagram which we need to commute

-- morphisms are always "the obvious one"; note that R -> A -> Unit is an IsScalarTower
def φ (U V : TopologicalSpace.Opens Bool) (g : V ⟶ U) : f R A U ⟶ f R A V :=
  -- want to break into the 9 cases
  sorry

open AlgebraicGeometry

noncomputable def thing : LocallyRingedSpace where
  carrier := {
    α := Bool
  }
  presheaf := {
    obj := fun U ↦ f R A U.unop
    map := fun f ↦ by
      sorry
    map_id := sorry
    map_comp := sorry
  }
  IsSheaf := sorry
  localRing := sorry

I want everything to be easy: I want Lean to be constantly saying "OK there are 3 choices for the open set so just define what you want in each case" but this is taking me longer than I want it to. I was hoping Lean would make it easy to check if I'd made a mistake with this claim that this is a locally-ringed space because if it is then it's a pretty helpful (to me) example of how pathological they can be.

[Scott Carnahan]

This is somewhat orthogonal to the main point of your post, but you can make non-scheme one-point locally ringed spaces using Spf of certain complete local rings (namely those with more than one prime ideal).

[Kevin Buzzard]

Yeah that was my 0th example of a locally ringed space: one point, any local ring as global sections. Somehow everything seems so finite here, I was really hoping I could just check all the axioms by decide but I don't know enough about computibility to make this happen.

[Mitchell Lee]

You can use docs#nhds_false:

lemma not_open_false : ¬ IsOpen ({False} : Set Prop) := by
  intro h
  have := IsOpen.mem_nhds (x := False) h rfl
  rw [nhds_false, Filter.mem_top] at this
  simpa using congr_arg (True ∈ ·) this

[Mitchell Lee]

I found this by searching Loogle for sierpinskiSpace.

Making it work with decide seems out of reach because Prop doesn't have decidable equality. You could do it with Bool, though. One way would be to add a type synonym SierpinskiSpace for Bool and define the appropriate instance TopologicalSpace SierpinskiSpace. Then you could rename sierpinskiSpace : TopologicalSpace Prop to instTopologicalSpaceProp and define a noncomputable homeomorphism between SierpinskiSpace and Prop.

[Mitchell Lee]

By the way, it's not possible to put a computable DecidableEq instance on Set Bool. This is because a Set Bool is equivalent to two Props , and Prop doesn't have decidable equality. However, it is possible to decide whether two sets are equal if membership in each of the two sets is decidable, as follows:

instance {α : Type*} {U V : Set α} [Fintype α] [∀ x, Decidable (x ∈ U)] [∀ x, Decidable (x ∈ V)] : Decidable (U = V) :=
  decidable_of_iff _ Set.ext_iff.symm

[Mitchell Lee]

Finally, here's one "real-world" example of a locally ringed space which is not a scheme: a smooth manifold, with the sheaf of real-valued smooth functions.

[Yakov Pechersky]

Here is getting automation and decide working to do the case bash:

import Mathlib.AlgebraicGeometry.Scheme

-- remove all mention of the usual topology on Bool
attribute [-instance] instTopologicalSpaceBool instUniformSpaceBool

@[simp]
lemma Finset.coeEmb_empty {α : Type*} : Finset.coeEmb (∅ : Finset α) = ∅ := by
  simp [Finset.coeEmb]

@[simp]
lemma Finset.coeEmb_eq_empty_iff {α : Type*} {s : Finset α} :
    Finset.coeEmb s = ∅ ↔ s = ∅ := by
  simp [Finset.coeEmb]

@[simp]
lemma Finset.mem_coeEmb_mk_iff {α : Type*} {s : Multiset α} {hs} {x : α} :
    x ∈ Finset.coeEmb ⟨s, hs⟩ ↔ x ∈ s := by
  simp [Finset.coeEmb]

@[simp]
lemma Finset.mk_eq_empty_iff {α : Type*} {s : Multiset α} {hs} :
    (⟨s, hs⟩ : Finset α) = ∅ ↔ s = 0 := by
  simp [Finset.eq_empty_iff_forall_not_mem,  Multiset.eq_zero_iff_forall_not_mem]

@[simp]
lemma Exists.and_not_and_iff {X : Type*} {P Q : X → Prop} :
    (∃ x, P x ∧ ¬ P x ∧ Q x) ↔ False := by
  simp (config := {contextual := true})

@[simp]
lemma Exists.and_not_and_iff' {X : Type*} {P Q : X → Prop} :
    (∃ x, P x ∧ Q x ∧ ¬ P x) ↔ False := by
  simp (config := {contextual := true})

@[simp]
lemma Exists.not_and_and_iff {X : Type*} {P Q : X → Prop} :
    (∃ x, ¬ P x ∧ P x ∧ Q x) ↔ False := by
  simp (config := {contextual := true})

@[simp]
lemma Exists.not_and_and_iff' {X : Type*} {P Q : X → Prop} :
    (∃ x, ¬ P x ∧ Q x ∧ P x) ↔ False := by
  simp (config := {contextual := true})
namespace Bool

inductive IsOpen : Set Bool → Prop
| bot : IsOpen ⊥
| top : IsOpen ⊤
| true : IsOpen {true}

@[simp, aesop safe]
lemma IsOpen_def (U : Set Bool) :
    IsOpen U ↔ U = {} ∨ U = {true, false} ∨ U = {true} := by
  constructor
  · rintro (h | h | h) <;> aesop
  · rintro (rfl | rfl | rfl)
    · exact IsOpen.bot
    · convert IsOpen.top
      ext
      simp
    · exact IsOpen.true

instance : Fintype (Set Bool) := by infer_instance
instance : Fintype (Set (Set Bool)) := by infer_instance

lemma foo {P : Set Bool → Prop} :
    (∀ x : Set Bool, P x) ↔ P ∅ ∧ P {true} ∧ P {false} ∧ P ⊤ := by
  constructor
  · intro H
    simp [H]
  · intro ⟨hb, ht, hf, hu⟩ x
    fin_cases x
    · convert hb
      ext
      simp [Finset.coeEmb_empty (α := Bool)]
    · convert ht
      ext
      simp [Finset.mem_coeEmb_mk_iff (α := Bool)]
    · convert hf
      ext
      simp [Finset.mem_coeEmb_mk_iff (α := Bool)]
    · convert hu
      ext
      simp [Finset.mem_coeEmb_mk_iff (α := Bool)]

instance (P : Set Bool → Prop) [DecidablePred (fun s : Finset Bool => P s)] :
    Decidable (∃ t : Set Bool, P t) :=
  if he : P (∅ : Finset Bool) then isTrue ⟨_, he⟩
  else if ht : P ({true} : Finset Bool) then isTrue ⟨_, ht⟩
  else if hf : P ({false} : Finset Bool) then isTrue ⟨_, hf⟩
  else if hu : P (Finset.univ : Finset Bool) then isTrue ⟨_, hu⟩
  else isFalse (not_exists_of_forall_not (by
    intro x
    fin_cases x
    all_goals simpa
  ))

instance : TopologicalSpace Bool where
  IsOpen := IsOpen
  isOpen_univ := IsOpen.top
  isOpen_inter S T := by aesop
  isOpen_sUnion := by
    intro ι hι
    simp_rw [IsOpen_def] at hι
    fin_cases ι
    all_goals simp [Finset.coeEmb_empty (α := Set Bool), Finset.coeEmb_empty (α := Bool),
      Finset.mem_coeEmb_mk_iff (α := Set Bool), Finset.coeEmb_eq_empty_iff (α := Bool),
      Set.ext_iff, Finset.mem_coeEmb_mk_iff (α := Set Bool), Finset.mem_coeEmb_mk_iff (α := Bool),
            _root_.and_assoc, _root_.and_comm, _root_.and_left_comm, foo] at hι ⊢
    all_goals decide

[Yakov Pechersky]

There might be a way to get the parts I'm doing syntactically (modification of coeEmb expressions) to work through decide also

[Andrew Yang]

import Mathlib.AlgebraicGeometry.Scheme

-- remove all mention of the usual topology on Bool
attribute [-instance] instTopologicalSpaceBool instUniformSpaceBool

open CategoryTheory

namespace Bool

@[aesop safe [cases]]
inductive IsOpen : Set Bool → Type
| bot : IsOpen ∅
| top : IsOpen Set.univ
| true : IsOpen {true}

@[simp]
lemma isOpen_empty (h : IsOpen ∅) : h = .bot := by
  have (x : Set Bool) (h : x = ⊥) (h' : IsOpen x) : HEq h' IsOpen.bot := by
    cases h' <;> simp_all [Set.ext_iff]
  simpa using this _ rfl h

@[simp]
lemma isOpen_univ (h : IsOpen Set.univ) : h = .top := by
  have (x : Set Bool) (h : x = ⊤) (h' : IsOpen x) : HEq h' IsOpen.top := by
    cases h' <;> simp_all [Set.ext_iff]
  simpa using this _ rfl h

@[simp]
lemma isOpen_true (h : IsOpen {true}) : h = .true := by
  have (x : Set Bool) (h : x = {true}) (h' : IsOpen x) : HEq h' IsOpen.true := by
    cases h' <;> simp_all [Set.ext_iff]
  simpa using this _ rfl h

@[ext] lemma isOpen_ext {S} (h₁ h₂ : IsOpen S) : h₁ = h₂ := by aesop

lemma IsOpen_def (U : Set Bool) :
    Nonempty (IsOpen U) ↔ U = {} ∨ U = {true, false} ∨ U = {true} := by
  constructor
  · rintro (h | h | h) <;> aesop
  · rintro (rfl | rfl | rfl)
    · exact ⟨IsOpen.bot⟩
    · constructor
      convert IsOpen.top
      ext
      simp
    · exact ⟨IsOpen.true⟩

@[simp]
lemma not_isOpen (U : Set Bool) :
    IsEmpty (IsOpen U) ↔ false ∈ U ∧ true ∉ U := by
  suffices true ∉ U → (false ∉ U → true ∈ U ↔ false ∈ U) by
    rw [← not_nonempty_iff]; simpa [IsOpen_def, Set.ext_iff]
  intros H
  simp [H]

instance : TopologicalSpace Bool where
  IsOpen := Nonempty ∘ IsOpen
  isOpen_univ := ⟨IsOpen.top⟩
  isOpen_inter S T := by aesop (add simp IsOpen_def)
  isOpen_sUnion := by
    intro ι hι
    by_contra h
    simp only [Function.comp_apply, not_nonempty_iff, not_isOpen, Set.mem_sUnion, not_exists,
      _root_.not_and] at h
    obtain ⟨⟨i, hi, hi'⟩, H⟩ := h
    have := hι i hi
    rw [Function.comp_apply, ← not_isEmpty_iff, not_isOpen] at this
    exact this ⟨hi', H _ hi⟩

lemma grothendieckTopology_bool (x) (hx : x ≠ ⊥) :
    (Opens.grothendieckTopology Bool).sieves x = {⊤} := by
  apply subset_antisymm; swap
  · rintro _ rfl
    exact (Opens.grothendieckTopology Bool).top_mem _
  intros S hS
  rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top]
  rcases x with ⟨x, ⟨⟨⟩⟩⟩
  · simp at hx
  · obtain ⟨⟨V, ⟨⟨⟩⟩⟩, f, hf, hV⟩ := hS false trivial
    · cases hV
    · exact hf
    · cases hV
  · obtain ⟨⟨V, ⟨⟨⟩⟩⟩, f, hf, hV⟩ := hS true rfl
    · cases hV
    · cases f.le (show false ∈ _ from trivial)
    · exact hf

-- R,A rings, R -> A a map, A is the value on eta, R is the global secions
variable (R A : Type) [CommRing R] [CommRing A] [Algebra R A]

-- objects
open CommRingCat in
noncomputable def f (U : Set Bool) : Bool.IsOpen U → CommRingCat
  | .bot => .of Unit
  | .top => .of R
  | .true => .of A

@[simp] lemma not_insert_subset_empty {α} (s : Set α) (x : α) : ¬ insert x s ⊆ ∅ := by
  rw [Set.subset_empty_iff, ← ne_eq, ← Set.nonempty_iff_ne_empty]; exact ⟨x, by simp⟩

def φ (U V : Set Bool) (_g : V ≤ U) :
    (hU : Bool.IsOpen U) → (hV : Bool.IsOpen V) → f R A U hU ⟶ f R A V hV
  | _, .bot => algebraMap _ Unit
  | .bot, .top => by aesop
  | .top, .top => RingHom.id _
  | .true, .top => by aesop
  | .bot, .true => by aesop
  | .top, .true => algebraMap R A
  | .true, .true => RingHom.id _

open AlgebraicGeometry

@[simps]
noncomputable def prething : PresheafedSpace CommRingCat where
  carrier := TopCat.of Bool
  presheaf := {
    obj := fun U ↦ f R A U.unop.1 U.unop.2.some
    map := fun {U V} f ↦ φ R A U.unop.1 V.unop.1 f.unop.le U.unop.2.some V.unop.2.some
    map_id := by
      rintro ⟨U, ⟨h⟩⟩
      dsimp only
      rw [Bool.isOpen_ext (Nonempty.some _) h]
      aesop
    map_comp := by
      rintro ⟨U, ⟨hU⟩⟩ ⟨V, ⟨hV⟩⟩ ⟨W, ⟨hW⟩⟩ ⟨⟨⟨e₁ : V ⊆ U⟩⟩⟩ ⟨⟨⟨e₂ : W ⊆ V⟩⟩⟩
      dsimp
      rw [Bool.isOpen_ext (Nonempty.some _) hU, Bool.isOpen_ext (Nonempty.some _) hV,
        Bool.isOpen_ext (Nonempty.some _) hW]
      cases hU <;> cases hV <;> cases hW <;> simp at e₁ e₂ <;> aesop }

instance : Subsingleton ((prething R A).presheaf.obj (Opposite.op ⊥)) := by
  dsimp
  simp only [isOpen_empty]
  show Subsingleton Unit
  infer_instance

noncomputable
def stalk_false : (prething R A).presheaf.stalk false ≅ .of R := by
  let F := (TopologicalSpace.OpenNhds.inclusion false).op ⋙ (prething R A).presheaf
  haveI : Limits.IsInitial (⊤ : TopologicalSpace.OpenNhds (X := TopCat.of Bool) false) := by
    apply (config := { allowSynthFailures := true }) Limits.IsInitial.ofUnique
    intro X
    apply Nonempty.some
    rcases X with ⟨⟨X, ⟨⟨⟩⟩⟩, hX⟩
    · cases hX
    · exact ⟨⟨⟨𝟙 _⟩, fun _ ↦ Subsingleton.elim _ _⟩⟩
    · cases hX
  haveI := Limits.isIso_ι_of_isTerminal (Limits.terminalOpOfInitial this) F
  refine (asIso (Limits.colimit.ι F (Opposite.op ⊤))).symm ≪≫ eqToIso ?_
  simp [F, f]

noncomputable
def stalk_true : (prething R A).presheaf.stalk true ≅ .of A := by
  let F := (TopologicalSpace.OpenNhds.inclusion true).op ⋙ (prething R A).presheaf
  haveI : Limits.IsInitial (⟨⟨{true}, ⟨.true⟩⟩, rfl⟩ :
      TopologicalSpace.OpenNhds (X := TopCat.of Bool) true) := by
    apply (config := { allowSynthFailures := true }) Limits.IsInitial.ofUnique
    intro X
    apply Nonempty.some
    rcases X with ⟨⟨X, ⟨⟨⟩⟩⟩, hX⟩
    · cases hX
    · exact ⟨⟨⟨homOfLE le_top⟩, fun _ ↦ Subsingleton.elim _ _⟩⟩
    · exact ⟨⟨⟨𝟙 _⟩, fun _ ↦ Subsingleton.elim _ _⟩⟩
  haveI := Limits.isIso_ι_of_isTerminal (Limits.terminalOpOfInitial this) F
  refine (asIso (Limits.colimit.ι F (Opposite.op ⟨⟨{true}, ⟨.true⟩⟩, rfl⟩))).symm ≪≫ eqToIso ?_
  simp [F, f]

noncomputable def thing [LocalRing R] [LocalRing A] : LocallyRingedSpace where
  __ := prething R A
  IsSheaf := by
    rw [TopCat.Presheaf.IsSheaf,
      CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget (s := CategoryTheory.forget _),
      CategoryTheory.isSheaf_iff_isSheaf_of_type]
    rintro U S hS
    dsimp at hS U ⊢
    by_cases hU : U = ⊥
    · subst hU
      intro x _
      refine ⟨0, fun V e h ↦ ?_,
        fun _ _ ↦ Subsingleton.elim (α := (prething R A).presheaf.obj (Opposite.op ⊥)) _ _⟩
      · obtain rfl : V = ⊥ := le_bot_iff.mp e.le
        exact Subsingleton.elim (α := (prething R A).presheaf.obj (Opposite.op ⊥)) _ _
    rw [grothendieckTopology_bool U hU] at hS
    cases hS; exact Presieve.isSheafFor_top_sieve _
  localRing := by
    have : LocalRing (CommRingCat.of R) := ‹_›
    have : LocalRing (CommRingCat.of A) := ‹_›
    rintro ⟨⟩
    · exact (stalk_false R A).commRingCatIsoToRingEquiv.symm.localRing
    · exact (stalk_true R A).commRingCatIsoToRingEquiv.symm.localRing