環とイデアル

環論でも同じ設計が現れます． Subring R は部分環，Ideal R はイデアルを表す bundled structure です． 可換環のイデアルでは，加法で閉じていて，外からの積で閉じていることを使います．

#check Subring
#check Ideal
#check RingEquiv

section Ideals

variable {R : Type*} [CommRing R]
variable (I J : Ideal R)

example {x y : R} (hx : x ∈ I) (hy : y ∈ I) : x + y ∈ I := by
  exact I.add_mem hx hy

example {x : R} (hx : x ∈ I) (r : R) : r * x ∈ I := by
  exact I.mul_mem_left r hx

example : ((I ⊓ J : Ideal R) : Set R) = (I : Set R) ∩ (J : Set R) := by
  rfl

example (x : R) : x ∈ (⊥ : Ideal R) ↔ x = 0 := by
  exact Ideal.mem_bot

#check Ideal.Quotient.mk
#check Ideal.Quotient.eq_zero_iff_mem
#check Ideal.map
#check Ideal.comap

end Ideals

Ideal.Quotient I は商環です． 商を扱うときは，代表元に依存しない定義であることを証明する必要があります． このため，最初は #check で定義や補題の型を確認しながら進めるのが安全です．

演習問題

1. 可換環のイデアル I J : Ideal R について，I ⊓ J の元であることを集合の交わりとして読み替えてください．

   example {R : Type*} [CommRing R] (I J : Ideal R) (x : R) :
       x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J := by
     -- `rfl` または `simp` を試す．
     sorry
   

2. 可換環で，イデアルの元に外から掛けてもイデアルに入ることを左右両方で確認してください．

   example {R : Type*} [CommRing R] (I : Ideal R) {x : R} (hx : x ∈ I) (r : R) :
       x * r ∈ I := by
     -- 可換性で `r * x` に直すか，既存補題を探す．
     sorry