TCC lecture 4

noetherian.lean

import tactic -- a bunch of tactics
import ring_theory.noetherian -- Noetherian rings
/-

# Using ideals in Lean

Throughout, `R` is a commutative ring.

## The type of ideals of a ring

The type `ideal R` is the type of ideals of `R`.

This means that an ideal `J : ideal R` is a *term*, not a type. In particular elements of `J`
are not terms of type `J` (because that doesn't make sense, because `J` is not a type).

In Lean, elements of `J : ideal R` are terms `r : R`, i.e. terms *of type `R`*, for which the
proposition `r ∈ J` is true. Note the use of the set theory `∈`, which is notation for
`mem` (or, to give it its full name, `has_mem.mem`). In general `mem` eats a term of type `R`
and a term of type `S`, where `S` is "set-like" (i.e. its terms correspond to subsets of `R`),
and returns a proposition.

-/

variables (R : Type) [comm_ring R] (J : ideal R) (a : R)

#check a ∈ J -- it's a true-false statement

-- #check (a : J) -- doesn't typecheck

/-

## Ideals are a lattice

We are used to writing things like `I ⊆ J` if `I` and `J` are ideals of `R`, but there is
an abstraction of `⊆, ⊂, ∩` and so on, called a *lattice*, and lattice notation is
traditionally `≤, <, ⊓`. This is the notation used in Lean.

`≤` is called `le`
`<` is called `lt`
`⊓` is called `inf`
`⊔` is called `sup`. What do you think the sup of two ideals is, given that it must be an ideal?

-/

-- Let I,J,K be ideals of a ring.
example (I J K : ideal R)
  -- If I ⊆ J and J ⊆ K
  (hIJ : I ≤ J) (hJK : J ≤ K)
  -- then
  :
  -- I ⊆ K
  I ≤ K :=
begin
  sorry,
end

example (I J : ideal R) (x : R) : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J :=
begin
  sorry
end

example (I J : ideal R) (x : R) : x ∈ I ⊔ J ↔ ∃ (i ∈ I) (j ∈ J), i + j = x :=
begin
  sorry,
end

-- The `ideal.span` of a subset of `R` is the ideal generated by it.

example (S : set R) : S ⊆ ideal.span S :=
begin
  sorry
end

example (S T : set R) : S ⊆ T → ideal.span S ≤ ideal.span T :=
begin
  sorry,
end

/-

## Lattices and categories

A lattice is a partial order and hence a very simple type of category; all the hom sets
have size 0 or 1, with Hom(I,J) of size 1 iff I ≤ J. Note that in Lean, a proposition
is a type, and the number of terms of that type is 1 if the proposition is true and 0 if
it's false, so you can think of `Hom(I,J)` as being *equal* to `I ≤ J`.

The previous lemma shows that `ideal.span` is the data of a functor between the lattice of
subsets of `R` and the lattice of ideals of `R`. The axioms of a functor (`id` and `comp`) are
vacuously true because all hom sets have size 1, so `ideal.span` is a functor.

Similarly the forgetful functor is also a functor:
-/

example (I J : ideal R) : I ≤ J → (↑I : set R) ⊆ J :=
begin
  sorry,
end

-- In fact `ideal.span` is a left adjoint to the forgetful functor `↑` from ideals to subsets.

def gc : galois_connection (ideal.span : set R → ideal R) (coe : ideal R → set R) :=
begin
  intros S J,
  sorry,
end

example : galois_insertion (ideal.span : set R → ideal R) (coe : ideal R → set R) :=
galois_connection.to_galois_insertion (gc R)
begin
  sorry
end

/-

## Finiteness

There are three forms of finiteness in Lean, unfortunately.

1) `set.finite`, a nonconstructive noncomputable predicate on sets saying "I am finite".
This is the easiest of the three concepts for mathematicians to use (in the sense that it's
easiest to get the hang of).

-/

-- the *statement* (which could be true or false) that the subset `S` of `X` is finite.
example (X : Type) (S : set X) : Prop := set.finite S

-- subset of a finite subset of X is finite
example (X : Type) {S T : set X} (hS : S.finite) (hTS : T ⊆ S) : T.finite :=
begin
  sorry
end

-- union of two finite subsets of X is finite
example (X : Type) {S T : set X} (hS : S.finite) (hT : T.finite) : (S ∪ T).finite :=
begin
  sorry,
end

-- product of a finite subset of X and a finite subset of Y is a finite subset of X × Y
example (X Y : Type) {S : set X} {T : set Y} (hS : S.finite) (hT : T.finite) : (S.prod T).finite :=
begin
  sorry
end

-- Image of a finite set under a map is finite
example (X Y : Type) (f : X → Y) {S : set X} (hS : S.finite) : (f '' S).finite :=
begin
  sorry,
end


/-
2) `finset X`, the type of finite subsets of `X`.

This is *constructive* finiteness, so a bit of a nightmare.

-/

def finset1 {X : Type} [decidable_eq X] (a b : X) : finset X := {a,b}
def finset2 {X : Type} [decidable_eq X] (a b : X) : finset X := {b,a}

example (X : Type) [decidable_eq X] (a b : X) : finset1 a b = finset2 a b :=
begin
  sorry,
end

-- All the same results will be true but will be a bit more annoying to prove.
-- In fact I guess some of them will be definitions not theorems
-- Let's try to do unions
example (X : Type) (S T : finset X) : finset X := sorry

-- There's a coercion from `finset X` to `set X`, but remember that these are distinct types.
-- The up-arrow is a function from `finset X` to `set X`. It is not the "inclusion" in any sense
-- in Lean, just like the function from ℕ to ℤ isn't the inclusion.
example (X : Type) [decidable_eq X] (F : finset X) : set X := ↑F

-- You can prove that the corresponding set is finite
example (X : Type) [decidable_eq X] (F : finset X) : set.finite (F : set X) :=
begin
  sorry,
end

-- Conversely given a subset of `X` which is finite, you can make a term of type `finset X`

example (X : Type) (S : set X) (hS : S.finite) : finset X := sorry

-- These constructions should hopefully round trip
example (X : Type) : {S : set X // S.finite} ≃ finset X :=
sorry

/-

3) `fintype`. This is *constructive* finiteness but this time for a type. A term of type `fintype X`
can be thought of as "a proof that the type `X` only has finitely many terms", but it's not a proof;
it's *data* rather than something you "prove". Blame the constructivists.

-/

-- let X be the set {a,b}
@[derive decidable_eq]
inductive X : Type
| a : X
| b : X

-- actually the elements are `X.a` and `X.b`

example (P : Prop) (h1 h2 : P) : h1 = h2 := rfl

def fin1 : fintype X :=
{ elems := ({X.a,X.b} : finset X),
  complete := begin
    sorry,
  end }

def fin2 : fintype X :=
{ elems := ({X.b,X.a} : finset X),
  complete := begin
    sorry,
  end }

example : fin1 = fin2 := sorry

/-

4) `finite`. This is a predicate on types, saying that they only have finitely many terms.

-/

example : finite (fin 37) :=
begin
  sorry
end

-- It's quite new. Let's see if we can get it working.

example {X Y : Type} (hX : finite X) (hY : finite Y) : finite (X × Y) :=
begin
  sorry
end

/-

## Finitely generated ideals

`ideal.fg` is the predicate saying that an ideal is finitely-generated.

Let's see if we can prove that the ideal spanned by a finite set is finitely-generated
-/

example (T : set R) (hS : T.finite) : (ideal.span T).fg :=
begin
  sorry
end

-- Let's prove the image of a f.g. ideal under a ring hom is f.g.
example (S : Type) [comm_ring S] (f : R →+* S) (I : ideal R) (hI : I.fg) :
  (I.map f).fg :=
begin
  sorry
end

/-

## Noetherian rings

A ring is Noetherian if all ideals are finitely-generated.
There are various equivalent statements all in the API,
in the file `ring_theory.noetherian`

-/

-- This is Theorem 3.2 in Keith Conrad's notes on Noetherian rings
-- https://kconrad.math.uconn.edu/blurbs/ringtheory/noetherian-ring.pdf
example [is_noetherian_ring R] (φ : R →+* R) (hφ : function.surjective φ) :
  function.injective φ :=
begin
  sorry
end