Skip to content

Instantly share code, notes, and snippets.

@kbuzzard
Created October 31, 2022 15:58
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Embed
What would you like to do?
TCC lecture 4
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment