feat(topology/sheaves): presheaf on indiscrete space is sheaf iff val…

…ue at empty is terminal (#16694)

+ Show that the indiscrete topology (⊤ : topological_space α), defined to be the topology generated by nothing, consists of exactly the empty set and the whole space.

+ Show that a presheaf on an indiscrete space (in particular the one point space) is a sheaf if its value at the empty set is a terminal object.

+ Generalize universe level in the converse `is_terminal_of_empty` (which holds for any space).

Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

src/topology/order.lean

@@ -256,6 +256,19 @@ lemma is_open_implies_is_open_iff {a b : topological_space α} :
   (∀ s, a.is_open s → b.is_open s) ↔ b ≤ a :=
 iff.rfl
 
+/-- The only open sets in the indiscrete topology are the empty set and the whole space. -/
+lemma topological_space.is_open_top_iff {α} (U : set α) :
+  (⊤ : topological_space α).is_open U ↔ U = ∅ ∨ U = univ :=
+⟨λ h, begin
+  induction h with V h _ _ _ _ ih₁ ih₂ _ _ ih,
+  { cases h }, { exact or.inr rfl },
+  { obtain ⟨rfl|rfl, rfl|rfl⟩ := ⟨ih₁, ih₂⟩; simp },
+  { rw [sUnion_eq_empty, or_iff_not_imp_left],
+    intro h, push_neg at h, obtain ⟨U, hU, hne⟩ := h,
+    have := (ih U hU).resolve_left hne, subst this,
+    refine sUnion_eq_univ_iff.2 (λ a, ⟨_, hU, trivial⟩) },
+end, by { rintro (rfl|rfl), exacts [@is_open_empty _ ⊤, @is_open_univ _ ⊤] }⟩
+
 /-- A topological space is discrete if every set is open, that is,
   its topology equals the discrete topology `⊥`. -/
 class discrete_topology (α : Type*) [t : topological_space α] : Prop :=

src/topology/sets/opens.lean

@@ -151,6 +151,10 @@ by rw [← subtype.coe_injective.eq_iff, opens.coe_bot, ← set.not_nonempty_iff
 lemma ne_bot_iff_nonempty (U : opens α) : U ≠ ⊥ ↔ set.nonempty (U : set α) :=
 by rw [ne.def, ← opens.not_nonempty_iff_eq_bot, not_not]
 
+/-- An open set in the indiscrete topology is either empty or the whole space. -/
+lemma eq_bot_or_top {α} [t : topological_space α] (h : t = ⊤) (U : opens α) : U = ⊥ ∨ U = ⊤ :=
+by { simp_rw ← ext_iff, unfreezingI { subst h }, exact (is_open_top_iff U.1).1 U.2 }
+
 /-- A set of `opens α` is a basis if the set of corresponding sets is a topological basis. -/
 def is_basis (B : set (opens α)) : Prop := is_topological_basis ((coe : _ → set α) '' B)
 

src/topology/sheaves/punit.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import topology.sheaves.sheaf_condition.sites
+
+/-!
+# Presheaves on punit
+
+Presheaves on punit satisfy sheaf condition iff its value at empty set is a terminal object.
+-/
+
+namespace Top.presheaf
+
+universes u v w
+
+open category_theory category_theory.limits Top opposite
+
+variables {C : Type u} [category.{v} C]
+
+lemma is_sheaf_of_is_terminal_of_indiscrete {X : Top.{w}} (hind : X.str = ⊤) (F : presheaf C X)
+  (it : is_terminal $ F.obj $ op ⊥) : F.is_sheaf :=
+λ c U s hs, begin
+  obtain rfl | hne := eq_or_ne U ⊥,
+  { intros _ _, rw @exists_unique_iff_exists _ ⟨λ _ _, _⟩,
+    { refine ⟨it.from _, λ U hU hs, is_terminal.hom_ext _ _ _⟩, rwa le_bot_iff.1 hU.le },
+    { apply it.hom_ext } },
+  { convert presieve.is_sheaf_for_top_sieve _, rw ←sieve.id_mem_iff_eq_top,
+    have := (U.eq_bot_or_top hind).resolve_left hne, subst this,
+    obtain he | ⟨⟨x⟩⟩ := is_empty_or_nonempty X,
+    { exact (hne $ topological_space.opens.ext_iff.1 $ set.univ_eq_empty_iff.2 he).elim },
+    obtain ⟨U, f, hf, hm⟩ := hs x trivial,
+    obtain rfl | rfl := U.eq_bot_or_top hind,
+    { cases hm }, { convert hf } },
+end
+
+lemma is_sheaf_iff_is_terminal_of_indiscrete {X : Top.{w}} (hind : X.str = ⊤)
+  (F : presheaf C X) : F.is_sheaf ↔ nonempty (is_terminal $ F.obj $ op ⊥) :=
+⟨λ h, ⟨sheaf.is_terminal_of_empty ⟨F, h⟩⟩, λ ⟨it⟩, is_sheaf_of_is_terminal_of_indiscrete hind F it⟩
+
+lemma is_sheaf_on_punit_of_is_terminal (F : presheaf C (Top.of punit))
+  (it : is_terminal $ F.obj $ op ⊥) : F.is_sheaf :=
+is_sheaf_of_is_terminal_of_indiscrete (@subsingleton.elim (topological_space punit) _ _ _) F it
+
+lemma is_sheaf_on_punit_iff_is_terminal (F : presheaf C (Top.of punit)) :
+  F.is_sheaf ↔ nonempty (is_terminal $ F.obj $ op ⊥) :=
+⟨λ h, ⟨sheaf.is_terminal_of_empty ⟨F, h⟩⟩, λ ⟨it⟩, is_sheaf_on_punit_of_is_terminal F it⟩
+
+end Top.presheaf

src/topology/sheaves/sheaf_condition/sites.lean

@@ -487,7 +487,7 @@ namespace Top.sheaf
 open category_theory topological_space Top opposite
 
 variables {C : Type u} [category.{v} C]
-variables {X : Top.{v}} {ι : Type*} {B : ι → opens X}
+variables {X : Top.{w}} {ι : Type*} {B : ι → opens X}
 variables (F : X.presheaf C) (F' : sheaf C X) (h : opens.is_basis (set.range B))
 
 /-- The empty component of a sheaf is terminal -/