feat(library/theories/commutative_algebra/ideal.lean): add ideals and ring quotient
This commit is contained in:
Jeremy Avigad
parent
e72032d46a
commit
2cdefbbf0c
3 changed files with 676 additions and 0 deletions
|
|
@ -0,0 +1,4 @@
|
|||
theories.commutative_algebra
|
||||
============================
|
||||
|
||||
* [ideal](ideal.lean)
|
||||
671
library/theories/commutative_algebra/ideal.lean
Normal file
671
library/theories/commutative_algebra/ideal.lean
Normal file
|
|
@ -0,0 +1,671 @@
|
|||
/-
|
||||
Copyright (c) 2016 Marcos Mazari. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Ideals and quotient rings.
|
||||
|
||||
Authors: Marcos Mazari, Jeremy Avigad
|
||||
-/
|
||||
import data.set algebra.ring theories.move
|
||||
open function eq.ops algebra set classical
|
||||
|
||||
/- TODO: move -/
|
||||
|
||||
abbreviation contrapos := @not_imp_not_of_imp
|
||||
|
||||
lemma ne_of_not_mem_of_mem {A : Type} {I J : set A} {y : A} (H1 : y ∉ I) (H2 : y ∈ J) : I ≠ J :=
|
||||
by intro H; rewrite H at H1; exact H1 H2
|
||||
|
||||
lemma exists_mem_and_not_mem_of_not_subset {A : Type} {I J : set A} (H : ¬ J ⊆ I) :
|
||||
∃ y, y ∈ J ∧ y ∉ I :=
|
||||
obtain x (Hx : ¬ (x ∈ J → x ∈ I)), from exists_not_of_not_forall H,
|
||||
exists.intro x (and_not_of_not_implies Hx)
|
||||
|
||||
lemma exists_mem_and_not_mem_of_ne_of_subset {A : Type} {I J : set A} (H1 : I ≠ J) (H2 : I ⊆ J) :
|
||||
∃ y, y ∈ J ∧ y ∉ I :=
|
||||
exists_mem_and_not_mem_of_not_subset (assume H, H1 (eq_of_subset_of_subset H2 H))
|
||||
|
||||
/- TODO: move to file for additive subgroups -/
|
||||
|
||||
section
|
||||
|
||||
variable {A : Type}
|
||||
|
||||
structure is_zero_closed [class] [has_zero A] (S : set A) : Prop :=
|
||||
(zero_mem : zero ∈ S)
|
||||
|
||||
proposition zero_mem [has_zero A] {S : set A} [is_zero_closed S] : 0 ∈ S :=
|
||||
is_zero_closed.zero_mem _ S
|
||||
|
||||
structure is_add_closed [class] [has_add A] (S : set A) : Prop :=
|
||||
(add_mem : ∀₀ a ∈ S, ∀₀ b ∈ S, a + b ∈ S)
|
||||
|
||||
proposition add_mem [has_add A] {S : set A} [is_add_closed S] {a : A} (aS : a ∈ S) {b : A}
|
||||
(bS : b ∈ S) :
|
||||
a + b ∈ S :=
|
||||
is_add_closed.add_mem _ S aS bS
|
||||
|
||||
structure is_neg_closed [class] [has_neg A] (S : set A) : Prop :=
|
||||
(neg_mem : ∀₀ a ∈ S, -a ∈ S)
|
||||
|
||||
proposition neg_mem [has_neg A] {S : set A} [is_neg_closed S] {a : A} (aS : a ∈ S) : -a ∈ S :=
|
||||
is_neg_closed.neg_mem _ S aS
|
||||
|
||||
proposition mem_of_neg_mem [add_group A] {S : set A} [is_neg_closed S] {a : A} (naS : -a ∈ S) :
|
||||
a ∈ S :=
|
||||
by rewrite -neg_neg; exact neg_mem naS
|
||||
|
||||
proposition neg_mem_iff [add_group A] {S : set A} [is_neg_closed S] (a : A) : -a ∈ S ↔ a ∈ S :=
|
||||
iff.intro mem_of_neg_mem neg_mem
|
||||
|
||||
proposition sub_mem_swap [add_group A] {S : set A} [is_neg_closed S] {a b : A} (H : b - a ∈ S) :
|
||||
a - b ∈ S :=
|
||||
mem_of_neg_mem (by rewrite neg_sub; assumption)
|
||||
|
||||
proposition sub_mem_iff [add_group A] {S : set A} [is_neg_closed S] (a b : A) :
|
||||
a - b ∈ S ↔ b - a ∈ S :=
|
||||
iff.intro sub_mem_swap sub_mem_swap
|
||||
|
||||
structure is_add_subgroup [class] [add_group A] (S : set A)
|
||||
extends is_zero_closed S, is_add_closed S, is_neg_closed S : Prop
|
||||
|
||||
definition set_add [has_add A] (S T : set A) : set A := {x | ∃₀ y ∈ S, ∃₀ z ∈ T, x = y + z}
|
||||
|
||||
end
|
||||
|
||||
namespace set_add
|
||||
infix + := set_add
|
||||
end set_add
|
||||
open set_add
|
||||
|
||||
section
|
||||
|
||||
variables {A : Type}
|
||||
|
||||
proposition mem_set_add [has_add A] {S T : set A} {a b c : A}
|
||||
(aS : a ∈ S) (bT : b ∈ T) (ceq : c = a + b) :
|
||||
c ∈ S + T :=
|
||||
exists.intro a (and.intro aS (exists.intro b (and.intro bT ceq)))
|
||||
|
||||
proposition subset_set_add_right [add_monoid A] (S T : set A) [is_zero_closed T] : S ⊆ S + T :=
|
||||
take a, assume aS, mem_set_add aS zero_mem (by simp)
|
||||
|
||||
proposition subset_set_add_left [add_monoid A] (S T : set A) [is_zero_closed S] : T ⊆ S + T :=
|
||||
take a, assume aT, mem_set_add zero_mem aT (by simp)
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
variable {A : Type}
|
||||
variable [comm_ring A]
|
||||
|
||||
structure is_ideal [class] (I : set A) extends is_zero_closed I, is_add_closed I : Prop :=
|
||||
(mul_arb_mem : ∀ x, ∀₀ y ∈ I, x * y ∈ I)
|
||||
|
||||
proposition mul_arb_mem {I : set A} [is_ideal I] (x : A) {y : A} (yI : y ∈ I) : x * y ∈ I :=
|
||||
is_ideal.mul_arb_mem _ I x yI
|
||||
|
||||
proposition is_add_subgroup_of_is_ideal [instance] (I : set A) [is_ideal I] : is_add_subgroup I :=
|
||||
is_add_subgroup.mk zero_mem (@add_mem _ _ _ _)
|
||||
(λ a aI, by rewrite [neg_eq_neg_one_mul]; apply mul_arb_mem _ aI)
|
||||
|
||||
proposition mul_arb_mem' {I : set A} [H : is_ideal I] {x : A} (xI : x ∈ I) (y : A) : x * y ∈ I :=
|
||||
by rewrite mul.comm; apply mul_arb_mem y xI
|
||||
|
||||
lemma eq_univ_of_one_mem_of_is_ideal {I : set A} (H : 1 ∈ I) [is_ideal I] : I = univ :=
|
||||
eq_univ_of_forall (take x, have x * 1 ∈ I, from mul_arb_mem x H, by simp)
|
||||
|
||||
theorem is_ideal_inter ( I J : set A) (HI : is_ideal I)
|
||||
(HJ : is_ideal J) : is_ideal (I ∩ J) :=
|
||||
have H1 : 0 ∈ I ∩ J, from and.intro zero_mem zero_mem,
|
||||
have H2 : ∀₀ x ∈ I ∩ J, ∀₀ y ∈ I ∩ J, x + y ∈ I ∩ J, from
|
||||
take x, assume xIJ, take y, assume yIJ,
|
||||
obtain xI xJ, from xIJ,
|
||||
obtain yI yJ, from yIJ,
|
||||
show x + y ∈ I ∩ J, from and.intro (add_mem xI yI) (add_mem xJ yJ),
|
||||
have H3 : ∀ x, ∀₀ y ∈ I ∩ J, x * y ∈ I ∩ J, from
|
||||
take x y, assume yIJ,
|
||||
obtain yI yJ, from yIJ,
|
||||
show x * y ∈ I ∩ J, from and.intro (mul_arb_mem x yI)(mul_arb_mem x yJ),
|
||||
show is_ideal (I ∩ J), from is_ideal.mk H1 H2 H3
|
||||
|
||||
theorem is_ideal_singleton_zero : is_ideal '{(0 : A)} :=
|
||||
have H1 : 0 ∈ '{0}, from mem_singleton 0,
|
||||
have H2 : ∀₀ x ∈ '{0}, ∀₀ y ∈ '{0}, x + y ∈ '{0}, from
|
||||
take x, assume xmem, take y, assume ymem,
|
||||
by rewrite [eq_of_mem_singleton xmem, eq_of_mem_singleton ymem, zero_add]; apply mem_singleton,
|
||||
have H3 : ∀x, ∀₀ y ∈ '{0}, x * y ∈ '{0}, from
|
||||
take x y, assume ymem,
|
||||
by rewrite [eq_of_mem_singleton ymem, mul_zero]; apply mem_singleton,
|
||||
is_ideal.mk H1 H2 H3
|
||||
|
||||
lemma is_ideal_univ : is_ideal (@univ A) :=
|
||||
have H1 : 0 ∈ @univ A, from trivial,
|
||||
have H2: ∀₀ x ∈ univ, ∀₀ y ∈ univ, x + y ∈ (@univ A), from λ x xmem y ymem, trivial,
|
||||
have H3 : ∀ x, ∀₀ y ∈ univ, x * y ∈ (@univ A), from λ x y ymem, trivial,
|
||||
is_ideal.mk H1 H2 H3
|
||||
|
||||
lemma is_ideal_set_add [instance] (I J : set A) [is_ideal I] [is_ideal J] : is_ideal (I + J) :=
|
||||
have H1 : 0 ∈ I + J, from
|
||||
mem_set_add zero_mem zero_mem (by simp),
|
||||
have H2 : ∀₀ x ∈ I + J, ∀₀ y ∈ I + J, x + y ∈ I + J, from
|
||||
λ x xmem y ymem,
|
||||
obtain ix [ixI [jx [jxJ xeq]]], from xmem,
|
||||
obtain iy [iyI [jy [jyJ yeq]]], from ymem,
|
||||
show x + y ∈ I + J, from
|
||||
mem_set_add (add_mem ixI iyI) (add_mem jxJ jyJ)
|
||||
(by rewrite [xeq, yeq, *add.assoc, add.left_comm jx]),
|
||||
have H3 : ∀ x, ∀₀ y ∈ I + J, x * y ∈ I + J, from
|
||||
λ x y ymem,
|
||||
obtain iy [iyI [jy [jyJ yeq]]], from ymem,
|
||||
show x * y ∈ I + J, from
|
||||
mem_set_add (mul_arb_mem x iyI) (mul_arb_mem x jyJ)
|
||||
(by rewrite [yeq, left_distrib]),
|
||||
is_ideal.mk H1 H2 H3
|
||||
|
||||
lemma set_add_subset_of_is_ideal {S T I : set A} [is_ideal I] (SsubI : S ⊆ I) (TsubI : T ⊆ I) :
|
||||
S + T ⊆ I :=
|
||||
take x, suppose x ∈ S + T,
|
||||
obtain s [sS [t [tT xeq]]], from this,
|
||||
have s + t ∈ I, from add_mem (SsubI sS) (TsubI tT),
|
||||
show x ∈ I, by rewrite xeq; apply this
|
||||
|
||||
/- ideal generated by a set -/
|
||||
|
||||
inductive ideal_generated_by (S : set A) : A → Prop :=
|
||||
| generators_mem : ∀ {x}, x ∈ S → ideal_generated_by S x
|
||||
| zero_closed : ideal_generated_by S 0
|
||||
| add_closed : ∀ {x y}, ideal_generated_by S x → ideal_generated_by S y →
|
||||
ideal_generated_by S (x + y)
|
||||
| mul_arb_closed : ∀ r {x}, ideal_generated_by S x → ideal_generated_by S (r * x)
|
||||
|
||||
theorem subset_ideal_generated_by (S : set A) : S ⊆ ideal_generated_by S :=
|
||||
λ x xS, ideal_generated_by.generators_mem xS
|
||||
|
||||
theorem is_ideal_ideal_generated_by [instance] (S : set A) : is_ideal (ideal_generated_by S) :=
|
||||
is_ideal.mk
|
||||
(ideal_generated_by.zero_closed S)
|
||||
(λ x xmem y ymem, ideal_generated_by.add_closed xmem ymem)
|
||||
(λ r x xmem, ideal_generated_by.mul_arb_closed r xmem)
|
||||
|
||||
theorem ideal_generated_by_subset {S : set A} {I : set A} [is_ideal I] (H : S ⊆ I) :
|
||||
ideal_generated_by S ⊆ I :=
|
||||
begin
|
||||
intro x xiS,
|
||||
induction xiS with a ains a b aiS biS aI bI r a aiS aI,
|
||||
{exact H ains},
|
||||
{exact zero_mem},
|
||||
{exact add_mem aI bI},
|
||||
exact mul_arb_mem r aI
|
||||
end
|
||||
|
||||
theorem ideal_generated_by_eq {S : set A} {I : set A} [is_ideal I] (SsubI : S ⊆ I)
|
||||
(H : ∀ J, is_ideal J → S ⊆ J → I ⊆ J) :
|
||||
ideal_generated_by S = I :=
|
||||
eq_of_subset_of_subset
|
||||
(ideal_generated_by_subset SsubI)
|
||||
(H _ _ (subset_ideal_generated_by S))
|
||||
|
||||
theorem ideal_generated_by_eq_of_is_ideal {S : set A} [is_ideal S] : ideal_generated_by S = S :=
|
||||
ideal_generated_by_eq (subset.refl _) (λ J iJ sJ, sJ)
|
||||
|
||||
definition principal_ideal (a : A) : set A := ideal_generated_by '{a}
|
||||
|
||||
theorem mem_principal_ideal (a : A) : a ∈ principal_ideal a :=
|
||||
subset_ideal_generated_by _ (mem_singleton a)
|
||||
|
||||
theorem is_ideal_principal_ideal [instance] (a : A) : is_ideal (principal_ideal a) :=
|
||||
is_ideal_ideal_generated_by _
|
||||
|
||||
theorem principal_ideal_eq (a : A) : principal_ideal a = {b | ∃ r, b = r * a} :=
|
||||
have is_ideal {b | ∃ r, b = r * a}, from
|
||||
is_ideal.mk
|
||||
(exists.intro 0 (by simp))
|
||||
(λ x xmem y ymem,
|
||||
obtain r xeq, from xmem, obtain s yeq, from ymem,
|
||||
exists.intro (r + s) (by rewrite [xeq, yeq, right_distrib]))
|
||||
(λ x y ymem,
|
||||
obtain r yeq, from ymem,
|
||||
exists.intro (x * r) (by rewrite [yeq, mul.assoc])),
|
||||
ideal_generated_by_eq
|
||||
(singleton_subset_of_mem (exists.intro 1 (by simp)))
|
||||
(take J, suppose is_ideal J, suppose '{a} ⊆ J,
|
||||
have a ∈ J, from mem_of_singleton_subset this,
|
||||
show {b | ∃ r, b = r * a} ⊆ J, from
|
||||
take b, suppose ∃ r, b = r * a,
|
||||
obtain r beq, from this,
|
||||
show b ∈ J, by rewrite beq; exact mul_arb_mem r `a ∈ J`)
|
||||
|
||||
theorem ideal_generated_by_union_eq (S T: set A) :
|
||||
ideal_generated_by (S ∪ T) = ideal_generated_by S + ideal_generated_by T :=
|
||||
-- TODO: why are these needed?
|
||||
have is_ideal (ideal_generated_by S + ideal_generated_by T), from is_ideal_set_add _ _,
|
||||
have is_add_subgroup (ideal_generated_by T), from is_add_subgroup_of_is_ideal _,
|
||||
have is_zero_closed (ideal_generated_by T), from is_add_subgroup.to_is_zero_closed _,
|
||||
have is_add_subgroup (ideal_generated_by S), from is_add_subgroup_of_is_ideal _,
|
||||
have is_zero_closed (ideal_generated_by S), from is_add_subgroup.to_is_zero_closed _,
|
||||
ideal_generated_by_eq
|
||||
(union_subset
|
||||
(subset.trans (subset_ideal_generated_by S) (subset_set_add_right _ _))
|
||||
(subset.trans (subset_ideal_generated_by T) (subset_set_add_left _ _)))
|
||||
(take J, assume idealJ, assume JsubST,
|
||||
set_add_subset_of_is_ideal
|
||||
(ideal_generated_by_subset (subset.trans (subset_union_left _ _) JsubST))
|
||||
(ideal_generated_by_subset (subset.trans (subset_union_right _ _) JsubST)))
|
||||
|
||||
lemma ideal_generated_by_union_singleton (I : set A) [is_ideal I] (a : A) :
|
||||
ideal_generated_by (I ∪ '{a}) = {b | ∃₀ y ∈ I, ∃ z, b = y + z * a} :=
|
||||
begin
|
||||
rewrite [ideal_generated_by_union_eq, ideal_generated_by_eq_of_is_ideal],
|
||||
xrewrite [principal_ideal_eq],
|
||||
show I + {b | ∃ r, b = r * a} = {b | ∃ x, x ∈ I ∧ ∃ z, b = x + z * a},
|
||||
from set.ext (take y, iff.intro
|
||||
(assume ymem,
|
||||
obtain x [xI [b [[r beq] xeq]]], from ymem,
|
||||
exists.intro x (and.intro xI (exists.intro r (by rewrite [xeq, beq]))))
|
||||
(assume ymem,
|
||||
obtain x [xI [z beq]], from ymem,
|
||||
mem_set_add xI (exists.intro z rfl) beq))
|
||||
end
|
||||
|
||||
theorem exists_mul_eq_one_of_two_ideals (H : ∀ I : set A, is_ideal I → I = univ ∨ I = '{0})
|
||||
{x : A} (H1 : x ≠ 0) :
|
||||
∃ y, x * y = 1 :=
|
||||
or.elim (H (principal_ideal x) _)
|
||||
(suppose principal_ideal x = univ,
|
||||
have 1 ∈ principal_ideal x, by rewrite this; apply mem_univ,
|
||||
have ∃r, 1 = r*x, by rewrite [principal_ideal_eq x at this]; apply this,
|
||||
obtain r oneeq, from this,
|
||||
exists.intro r (by rewrite [oneeq, mul.comm]))
|
||||
(suppose principal_ideal x = '{0},
|
||||
have x ∈ '{0}, by rewrite -this; apply mem_principal_ideal x,
|
||||
have x = 0, from eq_of_mem_singleton this,
|
||||
absurd this H1)
|
||||
|
||||
theorem principal_ideal_subset {I : set A} [is_ideal I] {a : A} (aI : a ∈ I) :
|
||||
principal_ideal a ⊆ I :=
|
||||
take x,
|
||||
suppose x ∈ principal_ideal a,
|
||||
have ∃ r, x = r * a, by rewrite [principal_ideal_eq at this]; apply this,
|
||||
obtain r xeq, from this,
|
||||
show x ∈ I, by rewrite xeq; apply mul_arb_mem r aI
|
||||
|
||||
theorem exists_mem_and_ne_zero_of_is_ideal {I : set A} [is_ideal I] (H : I ≠ '{0}) :
|
||||
∃ y, y ∈ I ∧ y ≠ 0 :=
|
||||
have '{0} ⊆ I, from singleton_subset zero_mem,
|
||||
have ∃y , (y ∈ I ∧ y ∉ '{0}),
|
||||
from exists_mem_and_not_mem_of_ne_of_subset (ne.symm H) this,
|
||||
obtain y [yI ynmem], from this,
|
||||
exists.intro y (and.intro yI (assume yeq, ynmem (mem_singleton_of_eq yeq)))
|
||||
|
||||
theorem eq_univ_of_is_ideal_of_one_mem {I : set A} [is_ideal I] (H : 1 ∈ I) : I = univ :=
|
||||
eq_univ_of_forall (take x, by rewrite -mul_one; apply mul_arb_mem _ H)
|
||||
|
||||
theorem eq_univ_or_eq_singleton_zero_of_is_ideal (H : ∀ x : A , x ≠ 0 → ∃ y, x * y = 1)
|
||||
{I : set A} [is_ideal I] : I = univ ∨ I = '{0} :=
|
||||
by_cases
|
||||
(suppose I = '{0}, or.inr this)
|
||||
(suppose I ≠ '{0},
|
||||
obtain x [xI xne0], from exists_mem_and_ne_zero_of_is_ideal this,
|
||||
obtain y (xyeq : x * y = 1), from H x xne0,
|
||||
have 1 ∈ I, by rewrite -xyeq; exact mul_arb_mem' xI _,
|
||||
have I = univ, from eq_univ_of_is_ideal_of_one_mem this,
|
||||
or.inl this)
|
||||
|
||||
-- TODO: move
|
||||
private definition inhabited_of_has_zero [instance] : inhabited A :=
|
||||
inhabited.mk 0
|
||||
|
||||
noncomputable private definition classical_inv (x : A) : A :=
|
||||
if H : x = 0 then 0 else epsilon (λ y, x * y = 1)
|
||||
|
||||
private theorem mul_classical_inv (H : ∀ x : A , x ≠ 0 → ∃ y, x * y = 1) (x : A) (H' : x ≠ 0) :
|
||||
x * (classical_inv x) = 1 :=
|
||||
by rewrite [↑classical_inv, dif_neg H']; apply epsilon_spec (H x H')
|
||||
|
||||
private theorem classical_inv_mul (H : ∀ x : A , x ≠ 0 → ∃ y, x * y = 1) (x : A) (H' : x ≠ 0) :
|
||||
(classical_inv x) * x = 1 :=
|
||||
by rewrite [mul.comm, mul_classical_inv H x H']
|
||||
|
||||
private theorem classical_inv_zero : classical_inv (0 : A) = 0 :=
|
||||
by rewrite [↑classical_inv, dif_pos rfl]
|
||||
|
||||
noncomputable definition discrete_field_of_comm_ring (H : ∀ x : A , x ≠ 0 → ∃ y, x * y = 1)
|
||||
(H' : 0 ≠ 1) :
|
||||
discrete_field A :=
|
||||
⦃ discrete_field, (_ : comm_ring A),
|
||||
inv := classical_inv,
|
||||
zero_ne_one := H',
|
||||
inv_mul_cancel := classical_inv_mul H,
|
||||
mul_inv_cancel := mul_classical_inv H,
|
||||
has_decidable_eq := _,
|
||||
inv_zero := classical_inv_zero
|
||||
⦄
|
||||
|
||||
end
|
||||
|
||||
|
||||
/- quotient ring -/
|
||||
|
||||
namespace quotient_ring
|
||||
variables {A : Type} [comm_ring A] (K : set A) [is_ideal K]
|
||||
|
||||
local notation a `~` b := b - a ∈ K
|
||||
|
||||
private lemma rel_rfl (a : A) : a ~ a := by rewrite sub_self; apply zero_mem
|
||||
|
||||
private lemma rel_symm (a b : A) (H : a ~ b) : b ~ a :=
|
||||
mem_of_neg_mem (by rewrite neg_sub; apply H)
|
||||
|
||||
private lemma rel_trans (a b c : A) (H₁ : a ~ b) (H₂ : b ~ c) : a ~ c :=
|
||||
have c - a = (c - b) + (b - a), by simp,
|
||||
show c - a ∈ K, by rewrite this; exact add_mem H₂ H₁
|
||||
|
||||
private lemma add_well_defined {a1 a2 b1 b2 : A} (H1 : a1 ~ b1) (H2 : a2 ~ b2) :
|
||||
a1 + a2 ~ b1 + b2 :=
|
||||
have (b1 + b2) - (a1 + a2) = (b1 - a1) + (b2 - a2), by simp,
|
||||
by rewrite this; apply add_mem H1 H2
|
||||
|
||||
private lemma neg_well_defined {a b : A} (H : a ~ b) : (-a ~ -b) :=
|
||||
mem_of_neg_mem (by rewrite [neg_neg_sub_neg]; apply H)
|
||||
|
||||
private lemma mul_well_defined {a1 a2 b1 b2 : A} (H1 : a1 ~ b1) (H2 : a2 ~ b2) :
|
||||
a1 * a2 ~ b1 * b2 :=
|
||||
have b1 * b2 - a1 * a2 = (b1 - a1) * b2 + a1 * (b2 - a2),
|
||||
by rewrite [mul_sub_right_distrib, mul_sub_left_distrib, *sub_eq_add_neg, add.assoc,
|
||||
neg_add_cancel_left],
|
||||
begin
|
||||
rewrite this, apply add_mem,
|
||||
{exact mul_arb_mem' H1 _},
|
||||
exact mul_arb_mem _ H2
|
||||
end
|
||||
|
||||
definition quotient_ring_setoid : setoid A :=
|
||||
setoid.mk (λ a b, b - a ∈ K) (mk_equivalence _ (rel_rfl K) (rel_symm K) (rel_trans K))
|
||||
|
||||
local attribute quotient_ring_setoid [instance]
|
||||
|
||||
definition quotient [reducible] : Type := quot (quotient_ring_setoid K)
|
||||
|
||||
definition qproj (a : A) : quotient K := @quot.mk A (quotient_ring_setoid K) a
|
||||
|
||||
infix ` / ` := λ (A' : Type) [comm_ring A'] K' [is_ideal K'], quotient K'
|
||||
infix ` '+ `:65 := λ {A' : Type} [comm_ring A'] a K' [is_ideal K'], qproj K' a
|
||||
|
||||
variable {K}
|
||||
|
||||
theorem qproj_eq_qproj {a b : A} (H : b - a ∈ K) : a '+ K = b '+ K :=
|
||||
quot.sound H
|
||||
|
||||
theorem sub_mem_of_qproj_eq_qproj {a b : A} (H : a '+ K = b '+ K) : b - a ∈ K :=
|
||||
quot.exact H
|
||||
|
||||
theorem qproj_eq_qproj_iff (a b : A) : a '+ K = b '+ K ↔ b - a ∈ K :=
|
||||
iff.intro sub_mem_of_qproj_eq_qproj qproj_eq_qproj
|
||||
|
||||
-- TODO: replace in group.quotient as well
|
||||
proposition quotient_induction {P : A / K → Prop} (h : ∀ a, P (a '+ K)) : ∀ a, P a :=
|
||||
take a, quot.induction_on a h
|
||||
|
||||
proposition quotient_induction_on {P : A / K → Prop} (a : A / K) (h : ∀ a, P (a '+ K)) : P a :=
|
||||
quot.induction_on a h
|
||||
|
||||
proposition quotient_induction₂ {P : A / K → A / K → Prop}
|
||||
(h : ∀ a₁ a₂, P (a₁ '+ K) (a₂ '+ K)) :
|
||||
∀ a₁ a₂, P a₁ a₂ :=
|
||||
take a₁ a₂, quot.induction_on₂ a₁ a₂ h
|
||||
|
||||
proposition quotient_induction_on₂ {P : A / K → A / K → Prop}
|
||||
(a₁ a₂ : A / K) (h : ∀ a₁ a₂, P (a₁ '+ K) (a₂ '+ K)) :
|
||||
P a₁ a₂ :=
|
||||
quot.induction_on₂ a₁ a₂ h
|
||||
|
||||
proposition exists_eq_qproj : ∀ a : A / K, ∃ a', a = a' '+ K :=
|
||||
quotient_induction (λ a, exists.intro _ rfl)
|
||||
|
||||
private definition qadd : A / K → A / K → A / K :=
|
||||
quot.lift₂
|
||||
(λ a b, (a + b) '+ K)
|
||||
(take a₁ a₂ b₁ b₂, assume Ha : a₁ ~ b₁, assume Hb : a₂ ~ b₂,
|
||||
quot.sound (add_well_defined K Ha Hb))
|
||||
|
||||
private definition qmul : A / K → A / K → A / K :=
|
||||
quot.lift₂
|
||||
(λ a b, (a * b) '+ K)
|
||||
(take a₁ a₂ b₁ b₂, assume Ha : a₁ ~ b₁, assume Hb : a₂ ~ b₂,
|
||||
quot.sound (mul_well_defined K Ha Hb))
|
||||
|
||||
private definition qzero : A / K := 0 '+ K
|
||||
|
||||
private definition qone : A / K := 1 '+ K
|
||||
|
||||
private lemma qproj_eq_qproj_of_eq {a b : A} (H : a = b) : (a '+ K) = (b '+ K) := by rewrite H
|
||||
|
||||
private theorem qadd_comm (a b : A / K) : qadd a b = qadd b a :=
|
||||
quot.induction_on₂ a b
|
||||
(take a b, qproj_eq_qproj_of_eq (add.comm a b))
|
||||
|
||||
private theorem qadd_assoc (a b c : A / K) : qadd (qadd a b) c = qadd a (qadd b c) :=
|
||||
quot.induction_on₃ a b c
|
||||
(take a b c, qproj_eq_qproj_of_eq (add.assoc a b c))
|
||||
|
||||
private definition qneg : A / K → A / K :=
|
||||
quot.lift
|
||||
(λ a , (-a) '+ K)
|
||||
(take a1 a2, assume Ha : a1 ~ a2, quot.sound (neg_well_defined K Ha))
|
||||
|
||||
private theorem qadd_left_inverse (a : A/ K) : qadd (qneg a) a = qzero :=
|
||||
quot.induction_on a
|
||||
(take a, qproj_eq_qproj_of_eq (add.left_inv a))
|
||||
|
||||
private theorem zero_qadd (a : A / K) : qadd qzero a = a :=
|
||||
quot.induction_on a
|
||||
(take a, qproj_eq_qproj_of_eq (zero_add a))
|
||||
|
||||
private theorem qadd_zero (a : A / K) : qadd a qzero = a :=
|
||||
quot.induction_on a
|
||||
(take a, qproj_eq_qproj_of_eq (add_zero a))
|
||||
|
||||
private theorem qmul_comm (a b : A / K) : qmul a b = qmul b a :=
|
||||
quot.induction_on₂ a b
|
||||
(take a b, qproj_eq_qproj_of_eq (mul.comm a b))
|
||||
|
||||
private theorem qmul_assoc (a b c : A / K) : qmul (qmul a b) c = qmul a (qmul b c) :=
|
||||
quot.induction_on₃ a b c
|
||||
(take a b c, qproj_eq_qproj_of_eq (mul.assoc a b c))
|
||||
|
||||
private theorem one_qmul (a : A / K) : qmul qone a = a :=
|
||||
quot.induction_on a
|
||||
(take a, qproj_eq_qproj_of_eq (one_mul a))
|
||||
|
||||
private theorem qmul_one (a : A / K) : qmul a qone = a :=
|
||||
quot.induction_on a
|
||||
(take a, qproj_eq_qproj_of_eq (mul_one a))
|
||||
|
||||
private theorem left_distrib (a b c : A/K) : qmul a (qadd b c)= qadd (qmul a b) (qmul a c) :=
|
||||
quot.induction_on₃ a b c
|
||||
(take a b c, qproj_eq_qproj_of_eq (left_distrib a b c))
|
||||
|
||||
private theorem right_distrib (a b c : A/K) : qmul (qadd a b) c = qadd (qmul a c) (qmul b c) :=
|
||||
quot.induction_on₃ a b c
|
||||
(take a b c, qproj_eq_qproj_of_eq (right_distrib a b c))
|
||||
|
||||
private theorem qadd_comm (a b : A / K) : qadd a b = qadd b a :=
|
||||
quot.induction_on b
|
||||
(quot.induction_on a
|
||||
(take a b,
|
||||
have (b + a) - (a + b) = 0, by simp,
|
||||
have (b + a) - (a + b) ∈ K, by rewrite this; exact zero_mem,
|
||||
quot.sound this))
|
||||
|
||||
protected definition to_ring [instance] : comm_ring (quotient K) :=
|
||||
⦃ comm_ring,
|
||||
add := qadd,
|
||||
add_assoc := qadd_assoc,
|
||||
zero := qzero,
|
||||
zero_add := zero_qadd,
|
||||
add_zero := qadd_zero,
|
||||
neg := qneg,
|
||||
add_left_inv := qadd_left_inverse,
|
||||
add_comm := qadd_comm,
|
||||
mul := qmul,
|
||||
mul_assoc := qmul_assoc,
|
||||
one := qone,
|
||||
one_mul := one_qmul,
|
||||
mul_one := qmul_one,
|
||||
left_distrib := left_distrib,
|
||||
right_distrib := right_distrib,
|
||||
mul_comm := qmul_comm
|
||||
⦄
|
||||
|
||||
variable (K)
|
||||
theorem qproj_zero : 0 '+ K = 0 := rfl
|
||||
theorem qproj_one : 1 '+ K = 1 := rfl
|
||||
variable {K}
|
||||
|
||||
theorem qproj_eq_zero_iff (a : A) : a '+ K = 0 ↔ a ∈ K :=
|
||||
by krewrite [qproj_eq_qproj_iff, sub_mem_iff, sub_zero]
|
||||
|
||||
theorem mem_of_qproj_eq_zero {a : A} (H : a '+ K = 0 '+ K) : a ∈ K :=
|
||||
iff.mp (qproj_eq_zero_iff a) H
|
||||
|
||||
theorem qproj_eq_zero {a : A} (H : a ∈ K) : a '+ K = 0 :=
|
||||
iff.mpr (qproj_eq_zero_iff a) H
|
||||
|
||||
end quotient_ring
|
||||
|
||||
/- prime and maximal ideals -/
|
||||
|
||||
section
|
||||
variables {A : Type} [comm_ring A]
|
||||
open quotient_ring
|
||||
|
||||
structure is_prime_ideal [class] (I : set A) extends is_ideal I : Prop :=
|
||||
(is_prime : ∀ ⦃a b⦄, a * b ∈ I → a ∈ I ∨ b ∈ I)
|
||||
(nontrivial : I ≠ univ)
|
||||
|
||||
structure is_maximal_ideal [class] (I : set A) extends is_ideal I : Prop :=
|
||||
(is_maximal : ∀ ⦃J : set A⦄, is_ideal J → J ⊇ I → J = I ∨ J = univ)
|
||||
(nontrivial : I ≠ univ)
|
||||
|
||||
theorem mem_or_mem_of_is_prime {I : set A} [is_prime_ideal I] {a b : A} (H : a * b ∈ I) :
|
||||
a ∈ I ∨ b ∈ I :=
|
||||
is_prime_ideal.is_prime H
|
||||
|
||||
theorem ne_univ_of_is_prime (I : set A) [is_prime_ideal I] : I ≠ univ :=
|
||||
@is_prime_ideal.nontrivial _ _ I _
|
||||
|
||||
theorem is_maximal {I : set A} [is_maximal_ideal I] {J : set A} [idealJ : is_ideal J] (H : J ⊇ I) :
|
||||
J = I ∨ J = univ :=
|
||||
is_maximal_ideal.is_maximal idealJ H
|
||||
|
||||
theorem qproj_eq_zero_or_qproj_eq_zero_of_is_prime_ideal {I : set A} [is_prime_ideal I] (a b : A)
|
||||
(H : (a '+ I) * (b '+ I) = 0) :
|
||||
a '+ I = 0 ∨ b '+ I = 0 :=
|
||||
begin
|
||||
rewrite [+qproj_eq_zero_iff],
|
||||
apply mem_or_mem_of_is_prime,
|
||||
apply mem_of_qproj_eq_zero,
|
||||
exact H
|
||||
end
|
||||
|
||||
theorem is_prime_ideal_of_forall {I : set A} [is_ideal I]
|
||||
(H : ∀ a b, (a '+ I) * (b '+ I) = 0 → a '+ I = 0 ∨ b '+ I = 0) (H' : I ≠ univ) :
|
||||
is_prime_ideal I :=
|
||||
⦃ is_prime_ideal, (_ : is_ideal I),
|
||||
is_prime := begin
|
||||
intro a b abI,
|
||||
rewrite [-+qproj_eq_zero_iff],
|
||||
apply H,
|
||||
exact qproj_eq_zero abI
|
||||
end,
|
||||
nontrivial := H'
|
||||
⦄
|
||||
|
||||
theorem exists_qproj_mul_qproj_eq_one_of_is_maximal {I : set A} [is_maximal_ideal I] {a : A}
|
||||
(H : a '+ I ≠ 0) :
|
||||
∃ y, (a '+ I) * (y '+ I) = 1 :=
|
||||
have ideal_generated_by (I ∪ '{a}) ≠ I, from
|
||||
assume otherwise,
|
||||
have a ∈ ideal_generated_by (I ∪ '{a}),
|
||||
from subset_ideal_generated_by _ (mem_unionr (mem_singleton _)),
|
||||
have a ∉ I, from λ H', H (qproj_eq_zero H'),
|
||||
show false, begin apply this, rewrite -otherwise, assumption end,
|
||||
have ideal_generated_by (I ∪ '{a}) = univ, from
|
||||
or.resolve_left
|
||||
(is_maximal (subset.trans (subset_union_left _ _) (subset_ideal_generated_by _))) this,
|
||||
have 1 ∈ {b | ∃₀ y ∈ I, ∃ z, b = y + z * a},
|
||||
by rewrite [-ideal_generated_by_union_singleton, this]; apply mem_univ,
|
||||
obtain y [yI [z (oneeq : 1 = y + z * a)]], from this,
|
||||
exists.intro z (qproj_eq_qproj
|
||||
(show 1 - a * z ∈ I, by rewrite [oneeq, mul.comm, add_sub_cancel]; exact yI))
|
||||
|
||||
theorem is_maximal_ideal_of_forall {I : set A} [is_ideal I]
|
||||
(H : ∀ a, a '+ I ≠ 0 → ∃ y, (a '+ I) * (y '+ I) = 1) (H' : I ≠ univ) :
|
||||
is_maximal_ideal I :=
|
||||
⦃ is_maximal_ideal, (_ : is_ideal I),
|
||||
is_maximal := take J, suppose is_ideal J, suppose J ⊇ I,
|
||||
by_cases
|
||||
(suppose J = I, or.inl this)
|
||||
(suppose J ≠ I,
|
||||
obtain a [aJ anI],
|
||||
from exists_mem_and_not_mem_of_ne_of_subset (ne.symm this) `J ⊇ I`,
|
||||
have a '+ I ≠ 0, from λ H', anI (mem_of_qproj_eq_zero H'),
|
||||
obtain y (Hy : (a '+ I) * (y '+ I) = 1), from H _ this,
|
||||
have 1 - a * y ∈ I, from sub_mem_of_qproj_eq_qproj Hy,
|
||||
have 1 - a * y + a * y ∈ J, from add_mem (`J ⊇ I` this) (mul_arb_mem' aJ _),
|
||||
have 1 ∈ J, by rewrite [sub_add_cancel at this]; exact this,
|
||||
show J = I ∨ J = univ, from or.inr (eq_univ_of_is_ideal_of_one_mem this)),
|
||||
nontrivial := H'
|
||||
⦄
|
||||
|
||||
definition integral_domain_quotient_of_is_prime_ideal [instance] (I : set A) [is_prime_ideal I] :
|
||||
integral_domain (A / I) :=
|
||||
have H : ∀ a b : A / I, a * b = 0 → a = 0 ∨ b = 0, from
|
||||
quotient_induction₂ qproj_eq_zero_or_qproj_eq_zero_of_is_prime_ideal,
|
||||
have H' : (0 : A / I) ≠ 1, from
|
||||
assume otherwise,
|
||||
have 1 - 0 ∈ I, from sub_mem_of_qproj_eq_qproj otherwise,
|
||||
have I = univ, from eq_univ_of_is_ideal_of_one_mem (by rewrite [sub_zero at this]; exact this),
|
||||
show false, from is_prime_ideal.nontrivial _ I this,
|
||||
⦃ integral_domain, (_ : comm_ring (A / I)),
|
||||
eq_zero_or_eq_zero_of_mul_eq_zero := H,
|
||||
zero_ne_one := H'
|
||||
⦄
|
||||
|
||||
theorem is_prime_ideal_of_forall_quotient {I : set A} [is_ideal I]
|
||||
(H : ∀ a b : A / I, a * b = 0 → a = 0 ∨ b = 0) (H' : I ≠ univ) :
|
||||
is_prime_ideal I :=
|
||||
is_prime_ideal_of_forall (λ a b, H _ _) H'
|
||||
|
||||
noncomputable definition discrete_field_quotient_of_is_maximal_ideal [instance]
|
||||
(I : set A) [is_maximal_ideal I] :
|
||||
discrete_field (A / I) :=
|
||||
have H : ∀ x : A / I, x ≠ 0 → ∃ y, x * y = 1, from
|
||||
quotient_induction
|
||||
(take a, assume anz,
|
||||
obtain y Hy, from exists_qproj_mul_qproj_eq_one_of_is_maximal anz,
|
||||
exists.intro (y '+ I) Hy),
|
||||
have H' : (0 : A / I) ≠ 1, from
|
||||
assume otherwise,
|
||||
have 1 - 0 ∈ I, from sub_mem_of_qproj_eq_qproj otherwise,
|
||||
have I = univ, from eq_univ_of_is_ideal_of_one_mem (by rewrite [sub_zero at this]; exact this),
|
||||
show false, from is_maximal_ideal.nontrivial _ I this,
|
||||
discrete_field_of_comm_ring H H'
|
||||
|
||||
theorem is_maximal_ideal_of_forall_quotient {I : set A} [is_ideal I]
|
||||
(H : ∀ a : A / I, a ≠ 0 → ∃ b, a * b = 1) (H' : I ≠ univ) :
|
||||
is_maximal_ideal I :=
|
||||
is_maximal_ideal_of_forall
|
||||
(λ a aIne0,
|
||||
obtain b Hb, from H _ aIne0,
|
||||
obtain b' (beq : b = b' '+ I), from exists_eq_qproj b,
|
||||
exists.intro b' (by rewrite -beq; exact Hb))
|
||||
H'
|
||||
|
||||
theorem is_prime_ideal_of_is_maximal_ideal [instance] {I : set A} [is_maximal_ideal I] :
|
||||
is_prime_ideal I :=
|
||||
is_prime_ideal_of_forall_quotient
|
||||
(@eq_zero_or_eq_zero_of_mul_eq_zero _ _)
|
||||
(is_maximal_ideal.nontrivial _ I)
|
||||
|
||||
end
|
||||
|
|
@ -5,6 +5,7 @@ theories
|
|||
* [combinatorics](combinatorics/combinatorics.md)
|
||||
* [group_theory](group_theory/group_theory.md)
|
||||
* [finite_group_theory](finite_group_theory/finite_group_theory.md) : group theory based on finsets
|
||||
* [commutative_algebra](commutative_algebra/commutative_algebra.md)
|
||||
* [topology](topology/topology.md)
|
||||
* [analysis](analysis/analysis.md)
|
||||
* [measure_theory](measure_theory/measure_theory.md)
|
||||
Loading…
Reference in a new issue