Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(ring_theory): free_ring and free_comm_ring
- Loading branch information
1 parent
c64b67e
commit 40d09b0
Showing
2 changed files
with
475 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,267 @@ | ||
import group_theory.free_abelian_group data.equiv.algebra data.polynomial ring_theory.ideal_operations | ||
|
||
universes u v | ||
|
||
def free_comm_ring (α : Type u) : Type u := | ||
free_abelian_group $ multiset α | ||
|
||
namespace free_comm_ring | ||
|
||
variables (α : Type u) | ||
|
||
instance : add_comm_group (free_comm_ring α) := | ||
{ .. free_abelian_group.add_comm_group (multiset α) } | ||
|
||
instance : semigroup (free_comm_ring α) := | ||
{ mul := λ x, free_abelian_group.lift $ λ s2, free_abelian_group.lift (λ s1, free_abelian_group.of $ s1 + s2) x, | ||
mul_assoc := λ x y z, begin | ||
unfold has_mul.mul, | ||
refine free_abelian_group.induction_on z rfl _ _ _, | ||
{ intros s3, rw [free_abelian_group.lift.of, free_abelian_group.lift.of], | ||
refine free_abelian_group.induction_on y rfl _ _ _, | ||
{ intros s2, iterate 3 { rw free_abelian_group.lift.of }, | ||
refine free_abelian_group.induction_on x rfl _ _ _, | ||
{ intros s1, iterate 3 { rw free_abelian_group.lift.of }, rw add_assoc }, | ||
{ intros s1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih }, | ||
{ intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } }, | ||
{ intros s2 ih, iterate 4 { rw free_abelian_group.lift.neg }, rw ih }, | ||
{ intros y1 y2 ih1 ih2, iterate 4 { rw free_abelian_group.lift.add }, rw [ih1, ih2] } }, | ||
{ intros s3 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw ih }, | ||
{ intros z1 z2 ih1 ih2, iterate 2 { rw free_abelian_group.lift.add }, rw [ih1, ih2], | ||
exact (free_abelian_group.lift.add _ _ _).symm } | ||
end } | ||
|
||
instance : ring (free_comm_ring α) := | ||
{ one := free_abelian_group.of 0, | ||
mul_one := λ x, begin | ||
unfold has_mul.mul semigroup.mul has_one.one, | ||
rw free_abelian_group.lift.of, | ||
refine free_abelian_group.induction_on x rfl _ _ _, | ||
{ intros s, rw [free_abelian_group.lift.of, add_zero] }, | ||
{ intros s ih, rw [free_abelian_group.lift.neg, ih] }, | ||
{ intros x1 x2 ih1 ih2, rw [free_abelian_group.lift.add, ih1, ih2] } | ||
end, | ||
one_mul := λ x, begin | ||
unfold has_mul.mul semigroup.mul has_one.one, | ||
refine free_abelian_group.induction_on x rfl _ _ _, | ||
{ intros s, rw [free_abelian_group.lift.of, free_abelian_group.lift.of, zero_add] }, | ||
{ intros s ih, rw [free_abelian_group.lift.neg, ih] }, | ||
{ intros x1 x2 ih1 ih2, rw [free_abelian_group.lift.add, ih1, ih2] } | ||
end, | ||
left_distrib := λ x y z, free_abelian_group.lift.add _ _ _, | ||
right_distrib := λ x y z, begin | ||
unfold has_mul.mul semigroup.mul, | ||
refine free_abelian_group.induction_on z rfl _ _ _, | ||
{ intros s, iterate 3 { rw free_abelian_group.lift.of }, rw free_abelian_group.lift.add, refl }, | ||
{ intros s ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_add], refl }, | ||
{ intros z1 z2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2], | ||
rw [add_assoc, add_assoc], congr' 1, apply add_left_comm } | ||
end, | ||
.. free_comm_ring.add_comm_group α, | ||
.. free_comm_ring.semigroup α } | ||
|
||
instance : comm_ring (free_comm_ring α) := | ||
{ mul_comm := λ x y, begin | ||
refine free_abelian_group.induction_on x (zero_mul y) _ _ _, | ||
{ intros s, refine free_abelian_group.induction_on y (zero_mul _).symm _ _ _, | ||
{ intros t, unfold has_mul.mul semigroup.mul ring.mul, | ||
iterate 4 { rw free_abelian_group.lift.of }, rw add_comm }, | ||
{ intros t ih, rw [mul_neg_eq_neg_mul_symm, ih, neg_mul_eq_neg_mul] }, | ||
{ intros y1 y2 ih1 ih2, rw [mul_add, add_mul, ih1, ih2] } }, | ||
{ intros s ih, rw [neg_mul_eq_neg_mul_symm, ih, neg_mul_eq_mul_neg] }, | ||
{ intros x1 x2 ih1 ih2, rw [add_mul, mul_add, ih1, ih2] } | ||
end | ||
.. free_comm_ring.ring α } | ||
|
||
variables {α} | ||
def of (x : α) : free_comm_ring α := | ||
free_abelian_group.of [x] | ||
|
||
section lift | ||
|
||
variables {β : Type v} [comm_ring β] (f : α → β) | ||
|
||
def lift : free_comm_ring α → β := | ||
free_abelian_group.lift $ λ s, (s.map f).prod | ||
|
||
@[simp] lemma lift_zero : lift f 0 = 0 := rfl | ||
|
||
@[simp] lemma lift_one : lift f 1 = 1 := | ||
free_abelian_group.lift.of _ _ | ||
|
||
@[simp] lemma lift_of (x : α) : lift f (of x) = f x := | ||
(free_abelian_group.lift.of _ _).trans $ mul_one _ | ||
|
||
@[simp] lemma lift_add (x y) : lift f (x + y) = lift f x + lift f y := | ||
free_abelian_group.lift.add _ _ _ | ||
|
||
@[simp] lemma lift_neg (x) : lift f (-x) = -lift f x := | ||
free_abelian_group.lift.neg _ _ | ||
|
||
@[simp] lemma lift_sub (x y) : lift f (x - y) = lift f x - lift f y := | ||
free_abelian_group.lift.sub _ _ _ | ||
|
||
@[simp] lemma lift_mul (x y) : lift f (x * y) = lift f x * lift f y := | ||
begin | ||
refine free_abelian_group.induction_on y (mul_zero _).symm _ _ _, | ||
{ intros s2, conv { to_lhs, dsimp only [(*), mul_zero_class.mul, semiring.mul, ring.mul, semigroup.mul] }, | ||
rw [free_abelian_group.lift.of, lift, free_abelian_group.lift.of], | ||
refine free_abelian_group.induction_on x (zero_mul _).symm _ _ _, | ||
{ intros s1, iterate 3 { rw free_abelian_group.lift.of }, rw [multiset.map_add, multiset.prod_add] }, | ||
{ intros s1 ih, iterate 3 { rw free_abelian_group.lift.neg }, rw [ih, neg_mul_eq_neg_mul] }, | ||
{ intros x1 x2 ih1 ih2, iterate 3 { rw free_abelian_group.lift.add }, rw [ih1, ih2, add_mul] } }, | ||
{ intros s2 ih, rw [mul_neg_eq_neg_mul_symm, lift_neg, lift_neg, mul_neg_eq_neg_mul_symm, ih] }, | ||
{ intros y1 y2 ih1 ih2, rw [mul_add, lift_add, lift_add, mul_add, ih1, ih2] }, | ||
end | ||
|
||
instance : is_ring_hom (lift f) := | ||
{ map_one := lift_one f, | ||
map_mul := lift_mul f, | ||
map_add := lift_add f } | ||
|
||
@[simp] lemma lift_pow (x) (n : ℕ) : lift f (x ^ n) = lift f x ^ n := | ||
is_semiring_hom.map_pow _ x n | ||
|
||
theorem lift_unique (f : free_comm_ring α → β) [is_ring_hom f] : f = lift (f ∘ of) := | ||
funext $ λ x, @@free_abelian_group.lift.ext _ _ _ | ||
(is_ring_hom.is_add_group_hom f) | ||
(is_ring_hom.is_add_group_hom $ lift $ f ∘ of) | ||
(λ s, multiset.induction_on s ((is_ring_hom.map_one f).trans $ eq.symm $ lift_one _) | ||
(λ hd tl ih, show f (of hd * free_abelian_group.of tl) = lift (f ∘ of) (of hd * free_abelian_group.of tl), | ||
by rw [is_ring_hom.map_mul f, lift_mul, lift_of, ih])) | ||
|
||
end lift | ||
|
||
variables {β : Type v} (f : α → β) | ||
|
||
def map : free_comm_ring α → free_comm_ring β := | ||
lift $ of ∘ f | ||
|
||
instance : monad free_comm_ring := | ||
{ map := λ _ _, map, | ||
pure := λ _, of, | ||
bind := λ _ _ x f, lift f x } | ||
|
||
end free_comm_ring | ||
|
||
def free_comm_ring_pempty_equiv_int : free_comm_ring pempty.{u+1} ≃r ℤ := | ||
{ to_fun := free_comm_ring.lift $ pempty.rec _, | ||
inv_fun := coe, | ||
left_inv := λ x, free_abelian_group.induction_on x rfl | ||
(λ s, multiset.induction_on s rfl $ pempty.rec _) | ||
(λ s ih, by rw [free_comm_ring.lift_neg, int.cast_neg, ih]) | ||
(λ x1 x2 ih1 ih2, by rw [free_comm_ring.lift_add, int.cast_add, ih1, ih2]), | ||
right_inv := λ i, int.induction_on i rfl | ||
(λ i ih, by rw [int.cast_add, int.cast_one, free_comm_ring.lift_add, free_comm_ring.lift_one, ih]) | ||
(λ i ih, by rw [int.cast_sub, int.cast_one, free_comm_ring.lift_sub, free_comm_ring.lift_one, ih]), | ||
hom := by apply_instance } | ||
|
||
def free_comm_ring_punit_equiv_polynomial_int : free_comm_ring punit.{u+1} ≃r polynomial ℤ := | ||
{ to_fun := free_comm_ring.lift $ λ _, polynomial.X, | ||
inv_fun := polynomial.eval₂ coe (free_comm_ring.of punit.star), | ||
left_inv := λ x, begin | ||
haveI : is_semiring_hom (coe : int → free_comm_ring punit.{u+1}) := | ||
@@is_ring_hom.is_semiring_hom _ _ _ (@@int.cast.is_ring_hom _), | ||
exact free_abelian_group.induction_on x rfl | ||
(λ s, multiset.induction_on s rfl $ λ hd tl ih, show polynomial.eval₂ coe (free_comm_ring.of punit.star) | ||
(free_comm_ring.lift (λ (_x : punit), polynomial.X) (free_comm_ring.of hd * free_abelian_group.of tl)) = | ||
free_comm_ring.of hd * free_abelian_group.of tl, | ||
by cases hd; rw [free_comm_ring.lift_mul, free_comm_ring.lift_of, polynomial.eval₂_mul, polynomial.eval₂_X, ih]) | ||
(λ s ih, by rw [free_comm_ring.lift_neg, ← neg_one_mul, polynomial.eval₂_mul, | ||
← polynomial.C_1, ← polynomial.C_neg, polynomial.eval₂_C, | ||
int.cast_neg, int.cast_one, neg_one_mul, ih]) | ||
(λ x1 x2 ih1 ih2, by rw [free_comm_ring.lift_add, polynomial.eval₂_add, ih1, ih2]) | ||
end, | ||
right_inv := λ x, begin | ||
haveI : is_semiring_hom (coe : int → free_comm_ring punit.{u+1}) := | ||
@@is_ring_hom.is_semiring_hom _ _ _ (@@int.cast.is_ring_hom _), | ||
have : ∀ i : ℤ, free_comm_ring.lift (λ _ : punit, polynomial.X) ↑i = polynomial.C i, | ||
{ exact λ i, int.induction_on i | ||
(by rw [int.cast_zero, free_comm_ring.lift_zero, polynomial.C_0]) | ||
(λ i ih, by rw [int.cast_add, int.cast_one, free_comm_ring.lift_add, free_comm_ring.lift_one, ih, polynomial.C_add, polynomial.C_1]) | ||
(λ i ih, by rw [int.cast_sub, int.cast_one, free_comm_ring.lift_sub, free_comm_ring.lift_one, ih, polynomial.C_sub, polynomial.C_1]) }, | ||
exact polynomial.induction_on x | ||
(λ i, by rw [polynomial.eval₂_C, this]) | ||
(λ p q ihp ihq, by rw [polynomial.eval₂_add, free_comm_ring.lift_add, ihp, ihq]) | ||
(λ n i ih, by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_C, polynomial.eval₂_X, | ||
free_comm_ring.lift_mul, free_comm_ring.lift_pow, free_comm_ring.lift_of, this]) | ||
end, | ||
hom := by apply_instance } | ||
|
||
variables (α : Type u) [comm_ring α] | ||
|
||
def polynomial' : Type u := | ||
ideal.quotient (ideal.span | ||
(insert (free_comm_ring.of (some 1) - 1) | ||
(set.range (λ xy : α × α, free_comm_ring.of (some (xy.1 + xy.2)) - (free_comm_ring.of (some xy.1) + free_comm_ring.of (some xy.2))) ∪ | ||
set.range (λ xy : α × α, free_comm_ring.of (some (xy.1 * xy.2)) - (free_comm_ring.of (some xy.1) * free_comm_ring.of (some xy.2))))) : ideal (free_comm_ring (option α))) | ||
|
||
namespace polynomial' | ||
|
||
instance : comm_ring (polynomial' α) := | ||
ideal.quotient.comm_ring _ | ||
|
||
variables {α} | ||
|
||
def C (x : α) : polynomial' α := | ||
ideal.quotient.mk _ (free_comm_ring.of $ some x) | ||
|
||
def X : polynomial' α := | ||
ideal.quotient.mk _ (free_comm_ring.of none) | ||
|
||
instance C.is_ring_hom : is_ring_hom (@C α _) := | ||
{ map_one := ideal.quotient.eq.2 $ ideal.subset_span $ or.inl rfl, | ||
map_mul := λ x y, ideal.quotient.eq.2 $ ideal.subset_span $ or.inr $ or.inr $ | ||
set.mem_range.2 ⟨(x, y), rfl⟩, | ||
map_add := λ x y, ideal.quotient.eq.2 $ ideal.subset_span $ or.inr $ or.inl $ | ||
set.mem_range.2 ⟨(x, y), rfl⟩ } | ||
|
||
variables {β : Type v} [comm_ring β] | ||
|
||
section eval₂ | ||
|
||
def eval₂ (f : α → β) [is_ring_hom f] (x : β) : polynomial' α → β := | ||
ideal.quotient.lift _ (free_comm_ring.lift $ λ s, option.rec_on s x f) $ λ p hp, begin | ||
refine submodule.span_induction hp _ rfl _ _, | ||
{ intros p hp, cases hp with hp hp, | ||
{ subst hp, rw [free_comm_ring.lift_sub, free_comm_ring.lift_of, free_comm_ring.lift_one], | ||
change f 1 - 1 = 0, rw [is_ring_hom.map_one f, sub_self] }, | ||
rcases hp with ⟨⟨s, t⟩, rfl⟩ | ⟨⟨s, t⟩, rfl⟩, | ||
{ simp only [free_comm_ring.lift_sub, free_comm_ring.lift_add, free_comm_ring.lift_of], | ||
rw [is_ring_hom.map_add f, sub_self] }, | ||
{ simp only [free_comm_ring.lift_sub, free_comm_ring.lift_mul, free_comm_ring.lift_of], | ||
rw [is_ring_hom.map_mul f, sub_self] } }, | ||
{ intros y z ih1 ih2, rw [free_comm_ring.lift_add, ih1, ih2, add_zero] }, | ||
{ intros y z ih, rw [smul_eq_mul, free_comm_ring.lift_mul, ih, mul_zero] } | ||
end | ||
|
||
variables (f : α → β) [is_ring_hom f] | ||
|
||
@[simp] lemma eval₂_add (x p q) : eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q := | ||
quotient.induction_on₂' p q $ λ _ _, free_comm_ring.lift_add _ _ _ | ||
|
||
@[simp] lemma eval₂_neg (x p) : eval₂ f x (-p) = -eval₂ f x p := | ||
quotient.induction_on' p $ λ _, free_comm_ring.lift_neg _ _ | ||
|
||
@[simp] lemma eval₂_sub (x p q) : eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q := | ||
quotient.induction_on₂' p q $ λ _ _, free_comm_ring.lift_sub _ _ _ | ||
|
||
end eval₂ | ||
|
||
theorem eval₂_unique (f : polynomial' α → β) [is_ring_hom f] : | ||
f = eval₂ (f ∘ C) (f X) := | ||
funext $ λ p, quotient.induction_on' p $ λ x, begin | ||
change f (ideal.quotient.mk _ x) = eval₂ (f ∘ C) (f X) (ideal.quotient.mk _ x), | ||
refine free_abelian_group.induction_on x (is_ring_hom.map_zero f) _ _ _, | ||
{ intros s, unfold eval₂, rw [ideal.quotient.lift_mk, free_comm_ring.lift, free_abelian_group.lift.of], | ||
refine multiset.induction_on s (is_ring_hom.map_one f) _, | ||
rintros (_|x) s ih, | ||
{ change f (X * ideal.quotient.mk _ (free_abelian_group.of s)) = _, | ||
simp only [multiset.map_cons, multiset.prod_cons, is_ring_hom.map_mul f, ih] }, | ||
{ change f (C x * ideal.quotient.mk _ (free_abelian_group.of s)) = _, | ||
simp only [multiset.map_cons, multiset.prod_cons, is_ring_hom.map_mul f, ih] } }, | ||
{ intros s ih, rw [ideal.quotient.mk_neg, is_ring_hom.map_neg f, ih, eval₂_neg] }, | ||
{ intros s1 s2 ih1 ih2, rw [ideal.quotient.mk_add, is_ring_hom.map_add f, ih1, ih2, eval₂_add] } | ||
end | ||
|
||
end polynomial' |
Oops, something went wrong.