-
Notifications
You must be signed in to change notification settings - Fork 297
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
0f831bb
commit 518f265
Showing
1 changed file
with
142 additions
and
137 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 |
|---|---|---|
| @@ -1,199 +1,204 @@ | ||
| import algebra.ring data.equiv.basic | ||
|
|
||
| open ring | ||
| variables {R : Type*} {F : Type*} | ||
|
|
||
| structure ring_isom (R : Type*) (F : Type*) [ring R] [ring F] extends equiv R F := | ||
| (isom_is_hom : is_ring_hom (equiv.to_fun to_equiv)) | ||
| class is_ring_anti_hom [ring R] [ring F] (f : R → F) : Prop := | ||
| (map_one : f 1 = 1) | ||
| (map_mul : ∀ {x y : R}, f (x * y) = f y * f x) | ||
| (map_add : ∀ {x y : R}, f (x + y) = f x + f y) | ||
|
|
||
| namespace ring_isom | ||
| namespace is_ring_anti_hom | ||
|
|
||
| variables {R : Type*} {F : Type*} [ring R] [ring F] (Hs : ring_isom R F) (x y : R) | ||
| variables [ring R] [ring F] (f : R → F) [is_ring_anti_hom f] | ||
|
|
||
| open ring_isom | ||
| instance : is_add_group_hom f := | ||
| ⟨λ _ _, is_ring_anti_hom.map_add f⟩ | ||
|
|
||
| def isom := (equiv.to_fun Hs.to_equiv) | ||
| lemma map_zero : f 0 = 0 := | ||
| is_add_group_hom.zero f | ||
|
|
||
| instance : is_ring_hom (isom Hs) := ring_isom.isom_is_hom Hs | ||
| lemma map_neg {x} : f (-x) = -f x := | ||
| is_add_group_hom.neg f x | ||
|
|
||
| def map_add : | ||
| isom Hs (x + y) = isom Hs x + isom Hs y := is_ring_hom.map_add (isom Hs) | ||
| lemma map_sub {x y} : f (x - y) = f x - f y := | ||
| is_add_group_hom.sub f x y | ||
|
|
||
| def map_mul : | ||
| isom Hs (x * y) = isom Hs x * isom Hs y := is_ring_hom.map_mul (isom Hs) | ||
| end is_ring_anti_hom | ||
|
|
||
| def map_one : | ||
| isom Hs (1) = 1 := is_ring_hom.map_one (isom Hs) | ||
| variables (R F) | ||
|
|
||
| lemma bijective : | ||
| function.bijective (isom Hs) := equiv.bijective Hs.to_equiv | ||
| structure ring_isom [ring R] [ring F] extends R ≃ F := | ||
| [hom : is_ring_hom to_fun] | ||
|
|
||
| lemma map_zero : | ||
| isom Hs (0 : R) = 0 := | ||
| exists.elim | ||
| ((bijective Hs).right 0) | ||
| (λ a H, | ||
| have He : (isom Hs a) * (isom Hs 0) = 0, | ||
| from (eq_comm.mp H) ▸ (ring.zero_mul (isom Hs 0)), | ||
| (ring.mul_zero a) ▸ ((eq_comm.mp (map_mul Hs a 0)) ▸ He)) | ||
| namespace ring_isom | ||
|
|
||
| lemma map_zero_iff {x : R} : | ||
| isom Hs x = 0 ↔ x = 0 := | ||
| ⟨ λ H, (function.injective.eq_iff (bijective Hs).left).mp ((eq_comm.mp (map_zero Hs)) ▸ H), | ||
| λ H, (eq_comm.mp H) ▸ (map_zero Hs) ⟩ | ||
| variables {R F} [ring R] [ring F] (Hs : ring_isom R F) (x y : R) | ||
|
|
||
| lemma map_neg : | ||
| isom Hs (-x) = -isom Hs x := | ||
| have H : isom Hs (-x + x) = 0, | ||
| from eq_comm.mp (neg_add_self x) ▸ map_zero Hs, | ||
| add_eq_zero_iff_eq_neg.mp ((map_add Hs (-x) x) ▸ H) | ||
| instance : has_coe_to_fun (ring_isom R F) := | ||
| ⟨_, λ Hs, Hs.to_fun⟩ | ||
|
|
||
| lemma map_neg_one : | ||
| isom Hs (-1) = -1 := (map_one Hs) ▸ (map_neg Hs 1) | ||
| instance : is_ring_hom Hs := Hs.hom | ||
|
|
||
| end ring_isom | ||
| lemma map_add : Hs (x + y) = Hs x + Hs y := | ||
| is_ring_hom.map_add Hs | ||
|
|
||
| def ring_auto {R : Type*} [ring R] := ring_isom R R | ||
| lemma map_zero : Hs 0 = 0 := | ||
| is_ring_hom.map_zero Hs | ||
|
|
||
| class is_ring_anti_hom {R : Type*} {F :Type*} [ring R] [ring F] (f : R → F) : Prop := | ||
| (map_add : ∀ {x y : R}, f (x + y) = f x + f y) | ||
| (map_mul : ∀ {x y : R}, f (x * y) = f y * f x) | ||
| (map_one : f 1 = 1) | ||
| lemma map_neg : Hs (-x) = -Hs x := | ||
| is_ring_hom.map_neg Hs | ||
|
|
||
| structure ring_anti_isom (R : Type*) (F : Type*) [ring R] [ring F] extends equiv R F := | ||
| (anti_isom_is_anti_hom : is_ring_anti_hom (equiv.to_fun to_equiv)) | ||
| lemma map_sub : Hs (x - y) = Hs x - Hs y := | ||
| is_ring_hom.map_sub Hs | ||
|
|
||
| namespace ring_anti_isom | ||
| lemma map_mul : Hs (x * y) = Hs x * Hs y := | ||
| is_ring_hom.map_mul Hs | ||
|
|
||
| variables {R : Type*} {F : Type*} [ring R] [ring F] (Hs : ring_anti_isom R F) (x y : R) | ||
| lemma map_one : Hs 1 = 1 := | ||
| is_ring_hom.map_one Hs | ||
|
|
||
| open ring_anti_isom | ||
| lemma map_neg_one : Hs (-1) = -1 := | ||
| Hs.map_one ▸ Hs.map_neg 1 | ||
|
|
||
| def anti_isom := (equiv.to_fun Hs.to_equiv) | ||
| lemma bijective : function.bijective Hs := | ||
| Hs.to_equiv.bijective | ||
|
|
||
| instance : is_ring_anti_hom (anti_isom Hs) := ring_anti_isom.anti_isom_is_anti_hom Hs | ||
| lemma map_zero_iff {x : R} : Hs x = 0 ↔ x = 0 := | ||
| ⟨λ H, Hs.bijective.1 $ H.symm ▸ Hs.map_zero.symm, | ||
| λ H, H.symm ▸ Hs.map_zero⟩ | ||
|
|
||
| def map_add : | ||
| anti_isom Hs (x + y) = anti_isom Hs x + anti_isom Hs y := is_ring_anti_hom.map_add (anti_isom Hs) | ||
| variables (R) | ||
| protected def refl [ring R] : ring_isom R R := | ||
| { hom := ⟨rfl, λ _ _, rfl, λ _ _, rfl⟩, | ||
| .. equiv.refl R } | ||
|
|
||
| def map_mul : | ||
| anti_isom Hs (x * y) = anti_isom Hs y * anti_isom Hs x := is_ring_anti_hom.map_mul (anti_isom Hs) | ||
| end ring_isom | ||
|
|
||
| def map_one : | ||
| anti_isom Hs (1) = 1 := is_ring_anti_hom.map_one (anti_isom Hs) | ||
| def ring_auto [ring R] := ring_isom R R | ||
|
|
||
| lemma bijective : | ||
| function.bijective (anti_isom Hs) := equiv.bijective Hs.to_equiv | ||
| structure ring_anti_isom [ring R] [ring F] extends R ≃ F := | ||
| [anti_hom : is_ring_anti_hom to_fun] | ||
|
|
||
| lemma map_zero : | ||
| anti_isom Hs 0 = 0 := | ||
| exists.elim | ||
| ((bijective Hs).right 0) | ||
| (λ a H, | ||
| have He : (anti_isom Hs 0) * (anti_isom Hs a) = 0, | ||
| from (eq_comm.mp H) ▸ (ring.mul_zero (anti_isom Hs 0)), | ||
| (ring.mul_zero a) ▸ ((eq_comm.mp (ring_anti_isom.map_mul Hs a 0)) ▸ He)) | ||
| namespace ring_anti_isom | ||
|
|
||
| lemma map_zero_iff {x : R} : | ||
| anti_isom Hs x = 0 ↔ x = 0 := | ||
| ⟨ λ H, (function.injective.eq_iff (bijective Hs).left).mp ((eq_comm.mp (map_zero Hs)) ▸ H), | ||
| λ H, (eq_comm.mp H) ▸ (map_zero Hs) ⟩ | ||
| variables {R F} [ring R] [ring F] (Hs : ring_anti_isom R F) (x y : R) | ||
|
|
||
| lemma map_neg : | ||
| anti_isom Hs (-x) = -anti_isom Hs x := | ||
| have H : anti_isom Hs (-x + x) = 0, | ||
| from eq_comm.mp (neg_add_self x) ▸ map_zero Hs, | ||
| add_eq_zero_iff_eq_neg.mp ((ring_anti_isom.map_add Hs (-x) x) ▸ H) | ||
| instance : has_coe_to_fun (ring_anti_isom R F) := | ||
| ⟨_, λ Hs, Hs.to_fun⟩ | ||
|
|
||
| lemma map_neg_one : | ||
| anti_isom Hs (-1) = -1 := (ring_anti_isom.map_one Hs) ▸ (map_neg Hs 1) | ||
| instance : is_ring_anti_hom Hs := Hs.anti_hom | ||
|
|
||
| end ring_anti_isom | ||
| lemma map_add : Hs (x + y) = Hs x + Hs y := | ||
| is_ring_anti_hom.map_add Hs | ||
|
|
||
| def comm_ring.hom_to_anti_hom {R : Type*} {F : Type*} [comm_ring R] [comm_ring F] (f : R → F) [is_ring_hom f] : | ||
| is_ring_anti_hom f := | ||
| { map_add := λ {x y : R}, is_ring_hom.map_add f, | ||
| map_mul := begin intros, have He : mul x y = x * y, refl, rw He, rw mul_comm, rw is_ring_hom.map_mul f, refl, end, | ||
| map_one := is_ring_hom.map_one f} | ||
| lemma map_zero : Hs 0 = 0 := | ||
| is_ring_anti_hom.map_zero Hs | ||
|
|
||
| def comm_ring.anti_hom_to_hom {R : Type*} {F : Type*} [comm_ring R] [comm_ring F] (f : R → F) [is_ring_anti_hom f] : | ||
| is_ring_hom f := | ||
| { map_add := λ {x y : R}, is_ring_anti_hom.map_add f, | ||
| map_mul := begin begin intros, have He : mul x y = x * y, refl, rw He, rw mul_comm, rw is_ring_anti_hom.map_mul f, refl, end, end, | ||
| map_one := is_ring_anti_hom.map_one f} | ||
| lemma map_neg : Hs (-x) = -Hs x := | ||
| is_ring_anti_hom.map_neg Hs | ||
|
|
||
| instance ring_isom.to_is_ring_hom {R : Type*} {F : Type*} [ring R] [ring F] (Hs : ring_isom R F) : | ||
| is_ring_hom Hs.to_equiv.to_fun := Hs.isom_is_hom | ||
| lemma map_sub : Hs (x - y) = Hs x - Hs y := | ||
| is_ring_anti_hom.map_sub Hs | ||
|
|
||
| instance ring_anti_isom.to_is_ring_anti_hom {R : Type*} {F : Type*} [ring R] [ring F] (Hs : ring_anti_isom R F) : | ||
| is_ring_anti_hom Hs.to_equiv.to_fun := Hs.anti_isom_is_anti_hom | ||
| lemma map_mul : Hs (x * y) = Hs y * Hs x := | ||
| is_ring_anti_hom.map_mul Hs | ||
|
|
||
| def comm_ring.isom_to_anti_isom {R : Type*} {F : Type*} [comm_ring R] [comm_ring F] (Hs : ring_isom R F) : | ||
| ring_anti_isom R F := | ||
| { to_equiv := Hs.to_equiv, | ||
| anti_isom_is_anti_hom := comm_ring.hom_to_anti_hom (ring_isom.isom Hs)} | ||
| lemma map_one : Hs 1 = 1 := | ||
| is_ring_anti_hom.map_one Hs | ||
|
|
||
| def comm_ring.anti_isom_to_isom {R : Type*} {F : Type*} [comm_ring R] [comm_ring F] (Hs : ring_anti_isom R F) : | ||
| ring_isom R F := | ||
| { to_equiv := Hs.to_equiv, | ||
| isom_is_hom := comm_ring.anti_hom_to_hom (ring_anti_isom.anti_isom Hs)} | ||
| lemma map_neg_one : Hs (-1) = -1 := | ||
| Hs.map_one ▸ Hs.map_neg 1 | ||
|
|
||
| def ring_anti_auto {R : Type*} [ring R] := ring_anti_isom R R | ||
| lemma bijective : function.bijective Hs := Hs.to_equiv.bijective | ||
|
|
||
| structure ring_invo (R : Type*) [ring R] extends ring_anti_isom R R := | ||
| (invo_comp_self : ∀ (x : R), (equiv.to_fun to_equiv) (((equiv.to_fun to_equiv) x)) = x) | ||
| lemma map_zero_iff {x : R} : Hs x = 0 ↔ x = 0 := | ||
| ⟨λ H, Hs.bijective.1 $ H.symm ▸ Hs.map_zero.symm, | ||
| λ H, H.symm ▸ Hs.map_zero⟩ | ||
|
|
||
| end ring_anti_isom | ||
|
|
||
| def ring_anti_auto [ring R] := ring_anti_isom R R | ||
|
|
||
| structure ring_invo [ring R] := | ||
| (to_fun : R → R) | ||
| [anti_hom : is_ring_anti_hom to_fun] | ||
| (to_fun_to_fun : ∀ x, to_fun (to_fun x) = x) | ||
|
|
||
| open ring_invo | ||
|
|
||
| namespace ring_invo | ||
|
|
||
| variables {R : Type*} [ring R] (Hi : ring_invo R) (x y : R) | ||
| variables {R} [ring R] (Hi : ring_invo R) (x y : R) | ||
|
|
||
| instance : has_coe_to_fun (ring_invo R) := | ||
| ⟨_, λ Hi, Hi.to_fun⟩ | ||
|
|
||
| instance : is_ring_anti_hom Hi := Hi.anti_hom | ||
|
|
||
| def to_ring_anti_auto : ring_anti_auto R := | ||
| { inv_fun := Hi, | ||
| left_inv := Hi.to_fun_to_fun, | ||
| right_inv := Hi.to_fun_to_fun, | ||
| .. Hi } | ||
|
|
||
| def invo := equiv.to_fun (ring_anti_isom.to_equiv Hi.to_ring_anti_isom) | ||
| lemma map_add : Hi (x + y) = Hi x + Hi y := | ||
| Hi.to_ring_anti_auto.map_add x y | ||
|
|
||
| def map_add : | ||
| invo Hi (x + y) = invo Hi (x) + invo Hi (y) := ring_anti_isom.map_add (Hi.to_ring_anti_isom) x y | ||
| lemma map_zero : Hi 0 = 0 := | ||
| Hi.to_ring_anti_auto.map_zero | ||
|
|
||
| def map_mul : | ||
| invo Hi (x * y) = invo Hi (y) * invo Hi (x) := ring_anti_isom.map_mul (Hi.to_ring_anti_isom) x y | ||
| lemma map_neg : Hi (-x) = -Hi x := | ||
| Hi.to_ring_anti_auto.map_neg x | ||
|
|
||
| def map_one : | ||
| invo Hi (1 : R) = 1 := ring_anti_isom.map_one (Hi.to_ring_anti_isom) | ||
| lemma map_sub : Hi (x - y) = Hi x - Hi y := | ||
| Hi.to_ring_anti_auto.map_sub x y | ||
|
|
||
| def invo_invo : | ||
| invo Hi (invo Hi (x)) = x := invo_comp_self Hi x | ||
|
|
||
| def bijective : | ||
| function.bijective (invo Hi) := equiv.bijective (ring_invo.to_ring_anti_isom Hi).to_equiv | ||
| lemma map_mul : Hi (x * y) = Hi y * Hi x := | ||
| Hi.to_ring_anti_auto.map_mul x y | ||
|
|
||
| def map_zero : | ||
| invo Hi (0 : R) = 0 := ring_anti_isom.map_zero (Hi.to_ring_anti_isom) | ||
| lemma map_one : Hi 1 = 1 := | ||
| Hi.to_ring_anti_auto.map_one | ||
|
|
||
| def map_zero_iff {x : R} : | ||
| invo Hi x = 0 ↔ x = 0 := ring_anti_isom.map_zero_iff (Hi.to_ring_anti_isom) | ||
| lemma map_neg_one : Hi (-1) = -1 := | ||
| Hi.to_ring_anti_auto.map_neg_one | ||
|
|
||
| def map_neg : | ||
| invo Hi (-x) = -(invo Hi x) := ring_anti_isom.map_neg (Hi.to_ring_anti_isom) x | ||
| lemma bijective : function.bijective Hi := | ||
| Hi.to_ring_anti_auto.bijective | ||
|
|
||
| def map_neg_one : | ||
| invo Hi (-1 : R) = -1 := ring_anti_isom.map_neg_one (Hi.to_ring_anti_isom) | ||
| lemma map_zero_iff {x : R} : Hi x = 0 ↔ x = 0 := | ||
| Hi.to_ring_anti_auto.map_zero_iff | ||
|
|
||
| end ring_invo | ||
| set_option trace.simplify true | ||
|
|
||
| def id_is_equiv (R : Type*) : equiv R R := | ||
| ⟨id, id, λ x, by rw [id.def, id.def], λ x, by rw [id.def, id.def]⟩ | ||
| section comm_ring | ||
| variables (R F) [comm_ring R] [comm_ring F] | ||
|
|
||
| protected def ring_invo.id : ring_invo R := | ||
| { anti_hom := ⟨rfl, mul_comm, λ _ _, rfl⟩, | ||
| to_fun_to_fun := λ _, rfl, | ||
| .. equiv.refl R } | ||
|
|
||
| protected def ring_anti_isom.refl : ring_anti_isom R R := | ||
| (ring_invo.id R).to_ring_anti_auto | ||
|
|
||
| variables {R F} | ||
|
|
||
| theorem comm_ring.hom_to_anti_hom (f : R → F) [is_ring_hom f] : is_ring_anti_hom f := | ||
| { map_add := λ _ _, is_ring_hom.map_add f, | ||
| map_mul := λ _ _, by rw [is_ring_hom.map_mul f, mul_comm], | ||
| map_one := is_ring_hom.map_one f} | ||
|
|
||
| theorem comm_ring.anti_hom_to_hom (f : R → F) [is_ring_anti_hom f] : is_ring_hom f := | ||
| { map_add := λ _ _, is_ring_anti_hom.map_add f, | ||
| map_mul := λ _ _, by rw [is_ring_anti_hom.map_mul f, mul_comm], | ||
| map_one := is_ring_anti_hom.map_one f} | ||
|
|
||
| def id_is_isom (R : Type*) [ring R] : ring_isom R R := | ||
| ⟨ id_is_equiv R, | ||
| λ (x y : R), by dunfold id_is_equiv; simp only [id.def], | ||
| by dunfold id_is_equiv; simp, | ||
| by dunfold id_is_equiv; simp only [id.def]⟩ | ||
| def comm_ring.isom_to_anti_isom (Hs : ring_isom R F) : ring_anti_isom R F := | ||
| { anti_hom := comm_ring.hom_to_anti_hom Hs, | ||
| .. Hs.to_equiv } | ||
|
|
||
| def id_is_anti_isom (R : Type*) [comm_ring R] : ring_anti_isom R R := comm_ring.isom_to_anti_isom (id_is_isom R) | ||
| def comm_ring.anti_isom_to_isom (Hs : ring_anti_isom R F) : ring_isom R F := | ||
| { hom := comm_ring.anti_hom_to_hom Hs, | ||
| .. Hs.to_equiv } | ||
|
|
||
| def id_is_invo (R : Type*) [comm_ring R] : ring_invo R := | ||
| ⟨ id_is_anti_isom R, | ||
| begin | ||
| dunfold id_is_anti_isom id_is_isom id_is_equiv comm_ring.isom_to_anti_isom, | ||
| simp, | ||
| end⟩ | ||
| end comm_ring |