feat(algebraic_geometry/prime_spectrum): first definitions (leanprove…

…r-community#1957)

* Start on prime spectrum

* Define comap betwee prime spectra; prove continuity

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* chore(*): rename `filter.inhabited_of_mem_sets` to `nonempty_of_mem_sets` (leanprover-community#1943)

In other names `inhabited` means that we have a `default` element.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(linear_algebra/multilinear): cleanup of multilinear maps (leanprover-community#1921)

* staging [ci skip]

* staging

* staging

* cleanup norms

* complete currying

* docstrings

* docstrings

* cleanup

* nonterminal simp

* golf

* missing bits for derivatives

* sub_apply

* cleanup

* better docstrings

* remove two files

* reviewer's comments

* use fintype

* line too long

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(ring_theory/power_series): several simp lemmas (leanprover-community#1945)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(ring_theory/power_series): several simp lemmas

* Remove file that shouldn't be there yet

* Update src/ring_theory/power_series.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Generalise lemma to canonically_ordered_monoid

* Update name

* Fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(tactic/lint): Three new linters, update illegal_constants (leanprover-community#1947)

* add three new linters

* fix failing declarations

* restrict and rename illegal_constants linter

* update doc

* update ge_or_gt test

* update mk_nolint

* fix error

* Update scripts/mk_nolint.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update src/meta/expr.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* clarify unfolds_to_class

* fix names since name is no longer protected

also change one declaration back to instance, since it did not cause a linter failure

* fix errors, move notes to docstrings

* add comments to docstring

* update mk_all.sh

* fix linter errors

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers (leanprover-community#1952)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers

* Remove old file

* Process comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(topology/algebra/multilinear): define continuous multilinear maps (leanprover-community#1948)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(data/set/intervals): define intervals and prove basic properties (leanprover-community#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(*): migrate from `≠ ∅` to `set.nonempty` (leanprover-community#1954)

* refactor(*): migrate from `≠ ∅` to `set.nonempty`

Sorry for a huge PR but it's easier to do it in one go.
Basically, I got rid of all `≠ ∅` in theorem/def types, then fixed
compile.

I also removed most lemmas about `≠ ∅` from `set/basic` to make sure
that I didn't miss something I should change elsewhere. Should I
restore (some of) them?

* Fix compile of `archive/`

* Drop +1 unneeded argument, thanks @sgouezel.

* Fix build

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Change I to s, and little fixes

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Indentation

* Update prime_spectrum.lean

* fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Zhouhang Zhou <zhouhanz@andrew.cmu.edu>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/algebraic_geometry/prime_spectrum.lean

@@ -0,0 +1,202 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import topology.opens
+import ring_theory.ideal_operations
+
+/-!
+# Prime spectrum of a commutative ring
+
+The prime spectrum of a commutative ring is the type of all prime ideals.
+It is naturally endowed with a topology: the Zariski topology.
+
+(It is also naturally endowed with a sheaf of rings,
+but that sheaf is not constructed in this file.
+It should be contributed to mathlib in future work.)
+
+## Inspiration/contributors
+
+The contents of this file draw inspiration from
+https://github.com/ramonfmir/lean-scheme
+which has contributions from Ramon Fernandez Mir, Kevin Buzzard, Kenny Lau,
+and Chris Hughes (on an earlier repository).
+
+-/
+
+universe variables u v
+
+variables (R : Type u) [comm_ring R]
+
+/-- The prime spectrum of a commutative ring `R`
+is the type of all prime ideal of `R`.
+
+It is naturally endowed with a topology (the Zariski topology),
+and a sheaf of commutative rings (not yet in mathlib).
+It is a fundamental building block in algebraic geometry. -/
+def prime_spectrum := {I : ideal R // I.is_prime}
+
+variable {R}
+
+namespace prime_spectrum
+
+/-- A method to view a point in the prime spectrum of a commutative ring
+as an ideal of that ring. -/
+abbreviation as_ideal (x : prime_spectrum R) : ideal R := x.val
+
+instance as_ideal.is_prime (x : prime_spectrum R) :
+  x.as_ideal.is_prime := x.2
+
+@[ext] lemma ext {x y : prime_spectrum R} :
+  x = y ↔ x.as_ideal = y.as_ideal :=
+subtype.ext
+
+/-- The zero locus of a set `s` of elements of a commutative ring `R`
+is the set of all prime ideals of the ring that contain the set `s`.
+
+An element `f` of `R` can be thought of as a dependent function
+on the prime spectrum of `R`.
+At a point `x` (a prime ideal)
+the function (i.e., element) `f` takes values in the quotient ring `R` modulo the prime ideal `x`.
+In this manner, `zero_locus s` is exactly the subset of `prime_spectrum R`
+where all "functions" in `s` vanish simultaneously.
+-/
+def zero_locus (s : set R) : set (prime_spectrum R) :=
+{x | s ⊆ x.as_ideal}
+
+@[simp] lemma mem_zero_locus (x : prime_spectrum R) (s : set R) :
+  x ∈ zero_locus s ↔ s ⊆ x.as_ideal := iff.rfl
+
+lemma zero_locus_empty_of_one_mem {s : set R} (h : (1:R) ∈ s) :
+  zero_locus s = ∅ :=
+begin
+  rw set.eq_empty_iff_forall_not_mem,
+  intros x hx,
+  rw mem_zero_locus at hx,
+  have x_prime : x.as_ideal.is_prime := by apply_instance,
+  have eq_top : x.as_ideal = ⊤, { rw ideal.eq_top_iff_one, exact hx h },
+  apply x_prime.1 eq_top,
+end
+
+@[simp] lemma zero_locus_univ :
+  zero_locus (set.univ : set R) = ∅ :=
+zero_locus_empty_of_one_mem (set.mem_univ 1)
+
+@[simp] lemma zero_locus_span (s : set R) :
+  zero_locus (ideal.span s : set R) = zero_locus s :=
+begin
+  ext x,
+  simp only [mem_zero_locus],
+  split,
+  { exact set.subset.trans ideal.subset_span },
+  { intro h, rwa ← ideal.span_le at h }
+end
+
+lemma union_zero_locus_ideal (I J : ideal R) :
+  zero_locus (I : set R) ∪ zero_locus J = zero_locus (I ⊓ J : ideal R) :=
+begin
+  ext x,
+  split,
+  { rintro (h|h),
+    all_goals
+    { rw mem_zero_locus at h ⊢,
+      refine set.subset.trans _ h,
+      intros r hr, cases hr, assumption } },
+  { rintro h,
+    rw set.mem_union,
+    simp only [mem_zero_locus] at h ⊢,
+    -- TODO: The rest of this proof should be factored out.
+    rw classical.or_iff_not_imp_right,
+    intros hs r hr,
+    rw set.not_subset at hs,
+    rcases hs with ⟨s, hs1, hs2⟩,
+    apply (ideal.is_prime.mem_or_mem (by apply_instance) _).resolve_left hs2,
+    apply h,
+    rw [submodule.mem_coe, submodule.mem_inf],
+    split,
+    { exact ideal.mul_mem_left _ hr },
+    { exact ideal.mul_mem_right _ hs1 } }
+end
+
+lemma union_zero_locus (s t : set R) :
+  zero_locus s ∪ zero_locus t = zero_locus ((ideal.span s) ⊓ (ideal.span t) : ideal R) :=
+by { rw ← union_zero_locus_ideal, simp }
+
+lemma zero_locus_Union {ι : Type*} (s : ι → set R) :
+  zero_locus (⋃ i, s i) = (⋂ i, zero_locus (s i)) :=
+by { ext x, simp only [mem_zero_locus, set.mem_Inter, set.Union_subset_iff] }
+
+lemma Inter_zero_locus {ι : Type*} (s : ι → set R) :
+  (⋂ i, zero_locus (s i)) = zero_locus (⋃ i, s i) :=
+(zero_locus_Union s).symm
+
+/-- The Zariski topology on the prime spectrum of a commutative ring
+is defined via the closed sets of the topology:
+they are exactly those sets that are the zero locus of a subset of the ring. -/
+instance zariski_topology : topological_space (prime_spectrum R) :=
+topological_space.of_closed (set.range prime_spectrum.zero_locus)
+  (⟨set.univ, by simp⟩)
+  begin
+    intros Zs h,
+    rw set.sInter_eq_Inter,
+    let f : Zs → set R := λ i, classical.some (h i.2),
+    have hf : ∀ i : Zs, i.1 = zero_locus (f i) := λ i, (classical.some_spec (h i.2)).symm,
+    simp only [hf],
+    exact ⟨_, (Inter_zero_locus _).symm⟩
+  end
+  (by { rintro _ _ ⟨s, rfl⟩ ⟨t, rfl⟩, exact ⟨_, (union_zero_locus s t).symm⟩ })
+
+lemma is_open_iff (U : set (prime_spectrum R)) :
+  is_open U ↔ ∃ s, -U = zero_locus s :=
+by simp only [@eq_comm _ (-U)]; refl
+
+lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
+  is_closed Z ↔ ∃ s, Z = zero_locus s :=
+by rw [is_closed, is_open_iff, set.compl_compl]
+
+lemma zero_locus_is_closed (s : set R) :
+  is_closed (zero_locus s) :=
+by { rw [is_closed_iff_zero_locus], exact ⟨s, rfl⟩ }
+
+section comap
+variables {S : Type v} [comm_ring S] {S' : Type*} [comm_ring S']
+
+/-- The function between prime spectra of commutative rings induced by a ring homomorphism.
+This function is continuous. -/
+def comap (f : R →+* S) : prime_spectrum S → prime_spectrum R :=
+λ y, ⟨ideal.comap f y.as_ideal, by exact ideal.is_prime.comap _⟩
+
+variables (f : R →+* S)
+
+@[simp] lemma comap_as_ideal (y : prime_spectrum S) :
+  (comap f y).as_ideal = ideal.comap f y.as_ideal :=
+rfl
+
+@[simp] lemma comap_id : comap (ring_hom.id R) = id :=
+funext $ λ x, ext.mpr $ by { rw [comap_as_ideal], apply ideal.ext, intros r, simp }
+
+@[simp] lemma comap_comp (f : R →+* S) (g : S →+* S') :
+  comap (g.comp f) = comap f ∘ comap g :=
+funext $ λ x, ext.mpr $ by { simp, refl }
+
+@[simp] lemma preimage_comap_zero_locus (s : set R) :
+  (comap f) ⁻¹' (zero_locus s) = zero_locus (f '' s) :=
+begin
+  ext x,
+  simp only [mem_zero_locus, set.mem_preimage, comap_as_ideal, set.image_subset_iff],
+  refl
+end
+
+lemma comap_continuous (f : R →+* S) : continuous (comap f) :=
+begin
+  rw continuous_iff_is_closed,
+  simp only [is_closed_iff_zero_locus],
+  rintro _ ⟨s, rfl⟩,
+  exact ⟨_, preimage_comap_zero_locus f s⟩
+end
+
+end comap
+
+end prime_spectrum

src/topology/basic.lean

@@ -49,6 +49,18 @@ structure topological_space (α : Type u) :=
 
 attribute [class] topological_space
 
+/-- A constructor for topologies by specifying the closed sets,
+and showing that they satisfy the appropriate conditions. -/
+def topological_space.of_closed {α : Type u} (T : set (set α))
+  (empty_mem : ∅ ∈ T) (sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T) (union_mem : ∀ A B ∈ T, A ∪ B ∈ T) :
+  topological_space α :=
+{ is_open := λ X, -X ∈ T,
+  is_open_univ := by simp [empty_mem],
+  is_open_inter := λ s t hs ht, by simpa [set.compl_inter] using union_mem (-s) (-t) hs ht,
+  is_open_sUnion := λ s hs,
+    by rw set.compl_sUnion; exact sInter_mem (set.compl '' s)
+    (λ z ⟨y, hy, hz⟩, by simpa [hz.symm] using hs y hy) }
+
 section topological_space
 
 variables {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}