9. 군과 환

군과 환의 연산에 대해 추론하는 방법은 제 2.2 절에서 살펴보았습니다. 이후 제 7.2 절에서는 군 구조와 같은 추상적인 대수적 구조를 정의하는 방법과 함께 가우스 정수 위의 환 구조와 같은 구체적인 인스턴스를 정의하는 방법을 살펴보았습니다. Chapter 8에서는 Mathlib에서 추상적인 구조의 계층을 다루는 방법을 설명했습니다.

이 장에서는 군과 환을 더 자세히 다룹니다. Mathlib에서 이 주제들을 다루는 방식의 모든 측면을 다룰 수는 없으며, Mathlib이 끊임없이 성장하고 있기 때문에 더욱 그렇습니다. 하지만 라이브러리로 들어가는 진입점을 제공하고, 핵심 개념이 어떻게 사용되는지 보여 드리겠습니다. Chapter 8의 논의와 일부 겹치는 부분이 있지만, 여기서는 이 주제들을 다루는 방식 뒤에 있는 설계 결정보다는 Mathlib을 사용하는 방법에 초점을 맞추겠습니다. 따라서 일부 예제를 이해하려면 Chapter 8의 배경 지식을 다시 살펴보아야 할 수도 있습니다.

9.1. 모노이드와 군

9.1.1. 모노이드와 그 사상

추상대수학 강의는 흔히 군에서 시작하여 환, 체, 벡터 공간으로 나아갑니다. 이 방식에서는 환의 곱셈을 다룰 때 다소 억지스러운 설명이 필요합니다. 곱셈 연산은 군 구조에서 오는 것이 아니지만, 많은 증명이 군론에서 이 새로운 상황으로 그대로 옮겨지기 때문입니다. 종이와 펜으로 수학을 할 때 가장 흔한 해결책은 그러한 증명을 연습 문제로 남겨 두는 것입니다. 덜 효율적이지만 더 안전하고 형식화에 더 적합한 방법은 모노이드를 사용하는 것입니다. 타입 M 위의 모노이드 구조는 결합법칙을 만족하고 항등원을 갖는 내부 합성 법칙입니다. 모노이드는 주로 군과 환의 곱셈 구조를 함께 다루기 위해 사용됩니다. 하지만 자연스러운 예도 많이 있습니다. 예를 들어, 덧셈을 갖춘 자연수 집합은 모노이드를 이룹니다.

실용적인 관점에서 보면, Mathlib을 사용할 때 모노이드는 대부분 무시해도 됩니다. 하지만 Mathlib 파일을 살펴보며 보조정리를 찾을 때는 모노이드가 존재한다는 사실을 알고 있어야 합니다. 그렇지 않으면 어떤 명제가 원소의 가역성을 요구하지 않아서 실제로는 모노이드 쪽에 있는데도 군론 파일에서 그 명제를 찾고 있게 될 수 있습니다.

타입 M 위의 모노이드 구조들의 타입은 Monoid M으로 씁니다. 함수 Monoid는 타입 클래스이므로 거의 항상 인스턴스 암시적 인자로(다시 말해 대괄호 안에) 나타납니다. 기본적으로 Monoid는 연산에 곱셈 표기법을 사용합니다. 덧셈 표기법을 쓰려면 대신 AddMonoid를 사용하십시오. 이 구조들의 가환 버전은 Monoid 앞에 접두사 Comm을 붙입니다.

example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x

example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y

AddMonoid가 라이브러리에 있기는 하지만, 비가환 연산에 덧셈 표기법을 사용하면 일반적으로 혼란스럽다는 점에 유의하십시오.

모노이드 M과 N 사이의 사상들의 타입은 MonoidHom M N이라고 하며 M →* N으로 씁니다. 이러한 사상을 M의 원소에 적용하면 Lean은 이를 자동으로 M에서 N으로 가는 함수로 간주합니다. 덧셈 버전은 AddMonoidHom이라고 하며 M →+ N으로 씁니다.

example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
  f.map_mul x y

example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
  f.map_zero

이러한 사상들은 묶인 사상(bundled map)입니다. 즉, 사상과 그 성질 일부를 하나로 묶어 둔 것입니다. 묶인 사상에 대해서는 제 8.2 절에서 설명한다는 점을 기억하십시오. 여기서는 사상을 합성할 때 일반적인 함수 합성을 사용할 수 없다는, 다소 아쉬운 결과만 짚어 둡니다. 대신 MonoidHom.comp와 AddMonoidHom.comp를 사용해야 합니다.

example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
    (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f

9.1.2. 군과 그 사상

군에 대해서는 앞으로 훨씬 더 많은 이야기를 하게 될 것입니다. 군은 모든 원소가 역원을 가진다는 추가 성질을 갖는 모노이드입니다.

example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x

앞에서 본 ring 택틱과 마찬가지로, 임의의 군에서 성립하는 모든 항등식을 증명하는 group 택틱이 있습니다. (동등하게 말하면, 이 택틱은 자유군에서 성립하는 항등식을 증명합니다.)

example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
  group

가환 덧셈군의 항등식을 위한 abel이라는 택틱도 있습니다.

example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
  abel

흥미롭게도, 군 준동형사상은 군 사이의 모노이드 준동형사상에 지나지 않습니다. 따라서 앞의 예제 중 하나를 복사하여 붙여 넣고 Monoid를 Group으로 바꾸기만 하면 됩니다.

example {G H : Type*} [Group G] [Group H] (x y : G) (f : G →* H) : f (x * y) = f x * f y :=
  f.map_mul x y

물론 다음과 같은 새로운 성질도 얻게 됩니다:

example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ :=
  f.map_inv x

모노이드 준동형사상의 정의는 항등원이 항등원으로 보내지도록 강제하지만 군 준동형사상의 경우에는 이것이 자동으로 성립하므로, 군 준동형사상을 구성할 때 불필요한 작업을 해야 하지 않을까 걱정할 수도 있습니다. 실제로 추가 작업은 어렵지 않지만, 이를 피할 수 있도록 합성 법칙과 호환되는 군 사이의 함수로부터 군 준동형사상을 만들어 주는 함수가 있습니다.

example {G H : Type*} [Group G] [Group H] (f : G → H) (h : ∀ x y, f (x * y) = f x * f y) :
    G →* H :=
  MonoidHom.mk' f h

≃*로 표기되는 군(또는 모노이드) 동형사상의 타입 MulEquiv도 있습니다(덧셈 표기에서는 ≃+로 표기되는 AddEquiv가 있습니다). f : G ≃* H의 역은 MulEquiv.symm f : H ≃* G이고, f와 g의 합성은 MulEquiv.trans f g이며, G의 항등식 동형사상은 M̀ulEquiv.refl G입니다. 익명 사영 표기법을 사용하면 앞의 두 가지는 각각 f.symm과 f.trans g로 쓸 수 있습니다. 이 타입의 원소는 필요할 때 자동으로 준동형사상과 함수로 강제 변환됩니다.

example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
    f.trans f.symm = MulEquiv.refl G :=
  f.self_trans_symm

MulEquiv.ofBijective를 사용하면 전단사 준동형사상으로부터 동형사상을 만들 수 있습니다. 이렇게 하면 역함수는 계산 불가능(noncomputable)해집니다.

noncomputable example {G H : Type*} [Group G] [Group H]
    (f : G →* H) (h : Function.Bijective f) :
    G ≃* H :=
  MulEquiv.ofBijective f h

9.1.3. 부분군

군 준동형사상이 묶인(bundled) 구조인 것처럼, G의 부분군도 G 안의 집합과 그에 관련된 닫힘 성질들로 이루어진 묶인 구조입니다.

example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) :
    x * y ∈ H :=
  H.mul_mem hx hy

example {G : Type*} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) :
    x⁻¹ ∈ H :=
  H.inv_mem hx

위의 예제에서 Subgroup G는 H가 Set G의 원소일 때의 술어 IsSubgroup H가 아니라 G의 부분군들의 타입이라는 점을 이해하는 것이 중요합니다. Subgroup G에는 Set G로의 강제 변환과 G 위의 소속 술어가 갖추어져 있습니다. 이것이 어떻게, 그리고 왜 이렇게 이루어지는지에 대한 설명은 제 8.3 절를 참고하십시오.

물론 두 부분군은 같은 원소를 가질 때, 그리고 그때에만 같습니다. 이 사실은 ext 택틱에서 사용할 수 있도록 등록되어 있으므로, 두 집합이 같음을 증명할 때와 같은 방식으로 두 부분군이 같음을 증명하는 데 이 택틱을 사용할 수 있습니다.

예를 들어 ℤ가 ℚ의 덧셈 부분군임을 서술하고 증명하려면, 실제로 원하는 것은 Set ℚ로의 사영이 ℤ인, 더 정확히 말하면 ℚ 안에서의 ℤ의 상인 AddSubgroup ℚ 타입의 항을 구성하는 것입니다.

example : AddSubgroup ℚ where
  carrier := Set.range ((↑) : ℤ → ℚ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  neg_mem' := by
    rintro _ ⟨n, rfl⟩
    use -n
    simp

Mathlib는 타입 클래스를 사용하여 군의 부분군이 군 구조를 물려받는다는 것을 알고 있습니다.

example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance

이 예제에는 미묘한 점이 있습니다. 대상 H는 타입이 아니지만, Lean은 이를 G의 부분타입으로 해석하여 자동으로 타입으로 강제 변환합니다. 따라서 위 예제는 다음과 같이 더 명시적으로 다시 쓸 수 있습니다:

example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance

술어 IsSubgroup : Set G → Prop 대신 타입 Subgroup G를 두면 Subgroup G에 추가 구조를 쉽게 부여할 수 있다는 중요한 이점이 있습니다. 특히 이 타입은 포함 관계에 대해 완비 격자 구조를 가집니다. 예를 들어, G의 두 부분군의 교집합이 다시 부분군이라는 보조정리를 두는 대신, 격자 연산 ⊓를 사용하여 교집합을 구성했습니다. 그러면 격자에 관한 임의의 보조정리를 이 구성에 적용할 수 있습니다.

두 부분군의 하한의 기반 집합이 정의상 실제로 두 부분군의 교집합인지 확인해 봅시다.

example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl

기반 집합들의 교집합에 해당하는 것에 다른 표기법을 쓰는 것이 이상해 보일 수 있지만, 이 대응 관계는 상한 연산과 합집합 사이에서는 성립하지 않습니다. 부분군들의 합집합은 일반적으로 부분군이 아니기 때문입니다. 대신 합집합으로 생성된 부분군을 사용해야 하며, 이는 Subgroup.closure를 사용하여 구합니다.

example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by
  rw [Subgroup.sup_eq_closure]

또 다른 미묘한 점은 G 자체는 Subgroup G 타입을 가지지 않는다는 것입니다. 따라서 G의 부분군으로 본 G에 대해 이야기할 방법이 필요합니다. 이 역시 격자 구조가 제공합니다: 전체 부분군이 이 격자의 최대 원소입니다.

example {G : Type*} [Group G] (x : G) : x ∈ (⊤ : Subgroup G) := trivial

마찬가지로 이 격자의 최소 원소는 항등원만을 원소로 갖는 부분군입니다.

example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot

군과 부분군을 다루는 연습으로, 전체 군의 원소에 의한 부분군의 켤레를 정의해 볼 수 있습니다.

def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where
  carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
  one_mem' := by
    dsimp
    sorry
  inv_mem' := by
    dsimp
    sorry
  mul_mem' := by
    dsimp
    sorry

앞의 두 주제를 함께 엮으면, 군 준동형사상을 사용하여 부분군을 앞으로 밀어 보내거나 뒤로 당겨 올 수 있습니다. Mathlib의 명명 규칙에서는 이 연산들을 map과 comap이라고 부릅니다. 이들은 흔히 쓰이는 수학 용어는 아니지만, “푸시포워드”나 “직상(direct image)”보다 짧다는 장점이 있습니다.

example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
  Subgroup.map f G'

example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
  Subgroup.comap f H'

#check Subgroup.mem_map
#check Subgroup.mem_comap

특히 준동형사상 f에 의한 최소 부분군의 역상은 f의 핵이라고 불리는 부분군이며, f의 치역 또한 부분군입니다.

example {G H : Type*} [Group G] [Group H] (f : G →* H) (g : G) :
    g ∈ MonoidHom.ker f ↔ f g = 1 :=
  f.mem_ker

example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : H) :
    h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h :=
  f.mem_range

군 준동형사상과 부분군을 다루는 연습으로, 몇 가지 기본적인 성질을 증명해 봅시다. 이 성질들은 Mathlib에 이미 증명되어 있으므로, 이 연습문제에서 도움을 얻고 싶다면 exact?를 너무 서둘러 사용하지 마십시오.

section exercises
variable {G H : Type*} [Group G] [Group H]

open Subgroup

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  sorry

example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
  sorry

variable {K : Type*} [Group K]

-- Remember you can use the `ext` tactic to prove an equality of subgroups.
example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
    comap (ψ.comp φ) U = comap φ (comap ψ U) := by
  sorry

-- Pushing a subgroup along one homomorphism and then another is equal to
-- pushing it forward along the composite of the homomorphisms.
example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
    map (ψ.comp φ) S = map ψ (S.map φ) := by
  sorry

end exercises

매우 고전적인 두 가지 결과로 Mathlib의 부분군 소개를 마무리합시다. 라그랑주 정리는 유한군의 부분군의 기수가 그 군의 기수를 나눈다는 것을 말합니다. 실로우 제1정리는 라그랑주 정리의 부분적인 역으로 잘 알려진 정리입니다.

Mathlib의 이 부분은 부분적으로 계산이 가능하도록 구성되어 있지만, 다음의 open scoped 명령을 사용하여 Lean이 어쨌든 비구성적 논리를 사용하도록 할 수 있습니다.

open scoped Classical


example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G :=
  ⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩

open Subgroup

example {G : Type*} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n :=
  Sylow.exists_subgroup_card_pow_prime p hdvd

다음 두 연습 문제에서는 라그랑주 보조정리의 따름정리를 유도합니다. (이 따름정리도 이미 Mathlib에 있으므로 exact?를 너무 성급하게 사용하지 마십시오.)

lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} :
    H = ⊥ ↔ Nat.card H = 1 := by
  suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
    simpa [eq_bot_iff_forall, Nat.card_eq_one_iff_exists]
  sorry

#check card_dvd_of_le

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  sorry

9.1.4. 구체적인 군

Mathlib에서는 구체적인 군도 다룰 수 있지만, 대개 추상적인 이론을 다루는 것보다 더 복잡합니다. 예를 들어, 임의의 타입 X가 주어지면 X의 순열들이 이루는 군은 Equiv.Perm X입니다. 특히 대칭군 \(\mathfrak{S}_n\)은 Equiv.Perm (Fin n)입니다. 이 군에 대한 추상적인 결과를 서술할 수도 있습니다. 예를 들어 X가 유한하면 Equiv.Perm X가 순환치환들로 생성된다고 서술할 수 있습니다.

open Equiv

example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
  Perm.closure_isCycle

완전히 구체적으로 순환치환들의 실제 곱을 계산할 수도 있습니다. 아래에서는 주어진 표현식에 simp 택틱을 호출하는 #simp 명령을 사용합니다. 표기 c[]는 순환 순열을 정의하는 데 사용됩니다. 이 예제에서 결과는 ℕ의 순열입니다. 처음 나오는 수에 (1 : Fin 5)와 같은 타입 명시를 붙이면 Perm (Fin 5)에서의 계산으로 만들 수 있습니다.

#simp [mul_assoc] c[1, 2, 3] * c[2, 3, 4]

구체적인 군을 다루는 또 다른 방법은 자유군과 군의 표시(presentation)를 사용하는 것입니다. 타입 α 위의 자유군은 FreeGroup α이고, 포함 관계 사상은 FreeGroup.of : α → FreeGroup α입니다. 예를 들어 a, b, c로 표기되는 세 원소를 갖는 타입 S와, 이에 대응하는 자유군의 원소 ab⁻¹를 정의해 봅시다.

section FreeGroup

inductive S | a | b | c

open S

def myElement : FreeGroup S := (.of a) * (.of b)⁻¹

Lean이 .of가 FreeGroup.of를 의미한다는 것을 알 수 있도록 정의의 기대 타입을 명시했다는 점에 유의하십시오.

자유군의 보편 성질은 동치 FreeGroup.lift로 구현되어 있습니다. 예를 들어, a를 c[1, 2, 3]으로, b를 c[2, 3, 1]로, c를 c[2, 3]으로 보내는 FreeGroup S에서 Perm (Fin 5)로의 군 준동형사상을 정의해 봅시다.

def myMorphism : FreeGroup S →* Perm (Fin 5) :=
  FreeGroup.lift fun | .a => c[1, 2, 3]
                     | .b => c[2, 3, 1]
                     | .c => c[2, 3]

마지막 구체적인 예로, 세제곱이 항등원인 하나의 원소로 생성되는 군(따라서 이 군은 \(\mathbb{Z}/3\)과 동형이 됩니다)을 정의하고, 그 군에서 Perm (Fin 5)로 가는 사상을 만드는 방법을 살펴봅시다.

정확히 하나의 원소를 갖는 타입으로는 유일한 원소가 ()로 표기되는 Unit을 사용하겠습니다. 함수 PresentedGroup은 관계들의 집합, 즉 어떤 자유군의 원소들의 집합을 받아, 이 자유군을 관계들로 생성되는 정규 부분군으로 나눈 몫군을 반환합니다. (더 일반적인 몫을 다루는 방법은 제 9.1.6 절에서 살펴보겠습니다.) 이 과정을 어느 정도 정의 뒤에 숨기고 있으므로, deriving Group을 사용하여 myGroup에 대한 군 인스턴스가 강제로 생성되도록 합니다.

def myGroup := PresentedGroup {.of () ^ 3} deriving Group

표시된 군의 보편 성질은 관계들을 대상 군의 항등원으로 보내는 함수로부터 이 군에서 나가는 사상을 만들 수 있음을 보장합니다. 따라서 그러한 함수와 그 조건이 성립한다는 증명이 필요합니다. 그런 다음 이 증명을 PresentedGroup.toGroup에 넘겨 원하는 군 준동형사상을 얻을 수 있습니다.

def myMap : Unit → Perm (Fin 5)
| () => c[1, 2, 3]

lemma compat_myMap :
    ∀ r ∈ ({.of () ^ 3} : Set (FreeGroup Unit)), FreeGroup.lift myMap r = 1 := by
  rintro _ rfl
  simp
  decide

def myNewMorphism : myGroup →* Perm (Fin 5) := PresentedGroup.toGroup compat_myMap

end FreeGroup

9.1.5. 군 작용

군론이 수학의 다른 분야와 상호작용하는 중요한 방식 중 하나는 군 작용을 활용하는 것입니다. 군 G가 어떤 타입 X에 작용하는 것은 G에서 Equiv.Perm X로 가는 사상에 지나지 않습니다. 따라서 어떤 의미에서 군 작용은 앞의 논의에서 이미 다룬 셈입니다. 하지만 이 사상을 계속 들고 다니고 싶지는 않습니다. 대신 가능한 한 Lean이 이를 자동으로 추론해 주기를 원합니다. 그래서 이를 위한 타입 클래스가 있으며, 그것이 MulAction G X입니다. 이 구성의 단점은 같은 군이 같은 타입에 여러 방식으로 작용하게 하려면 각기 다른 타입 클래스 인스턴스를 갖는 타입 동의어를 정의하는 등 다소 번거로운 우회가 필요하다는 점입니다.

특히 이를 통해 군의 원소 g가 점 x에 작용하는 것을 g • x로 나타낼 수 있습니다.

noncomputable section GroupActions

example {G X : Type*} [Group G] [MulAction G X] (g g': G) (x : X) :
    g • (g' • x) = (g * g') • x :=
  (mul_smul g g' x).symm

덧셈군을 위한 버전인 AddAction도 있으며, 여기서 작용은 +ᵥ로 나타냅니다. 이는 예를 들어 아핀 공간의 정의에 사용됩니다.

example {G X : Type*} [AddGroup G] [AddAction G X] (g g' : G) (x : X) :
    g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x :=
  (add_vadd g g' x).symm

바탕이 되는 군 준동형사상은 MulAction.toPermHom이라고 합니다.

open MulAction

example {G X : Type*} [Group G] [MulAction G X] : G →* Equiv.Perm X :=
  toPermHom G X

예시로, 임의의 군 G를 순열군, 즉 Perm G로 보내는 케일리 동형사상 매장을 어떻게 정의하는지 살펴봅시다. [MulAction G G]를 인스턴스화할 때 Lean은 왼쪽 곱셈으로 주어지는 표준 군 작용을 찾으며, 이것이 바로 우리가 원하는 것입니다.

def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
  Equiv.Perm.subgroupOfMulAction G G

위 정의 이전의 어떤 것도 모노이드가 아닌 군을 요구하지 않았다는(사실상 곱셈 연산이 주어진 임의의 타입이면 충분했다는) 점에 유의하십시오.

군이라는 조건이 실제로 필요해지는 것은 X를 궤도들로 분할하고자 할 때입니다. 이에 대응하는 X 위의 동치 관계는 MulAction.orbitRel이라고 합니다. 이것은 전역 인스턴스로 선언되어 있지 않습니다.

example {G X : Type*} [Group G] [MulAction G X] : Setoid X := orbitRel G X

이를 이용하면 X가 G의 작용에 의해 궤도들로 분할된다는 것을 서술할 수 있습니다. 더 정확히 말하면, X와 의존 곱 (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) 사이의 전단사를 얻는데, 여기서 Quotient.out' ω는 단순히 ω로 사영되는 원소 하나를 고릅니다. 이 의존 곱의 원소는 ⟨ω, x⟩ 형태의 쌍이며, 여기서 x의 타입 orbit G (Quotient.out' ω)는 ω에 의존한다는 것을 떠올리십시오.

example {G X : Type*} [Group G] [MulAction G X] :
    X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out ω)) :=
  MulAction.selfEquivSigmaOrbits G X

특히 X가 유한할 때, 이를 Fintype.card_congr 및 Fintype.card_sigma와 결합하면 X의 기수가 궤도들의 기수의 합임을 유도할 수 있습니다. 나아가, 궤도들은 안정자군의 왼쪽 이동 작용에 의한 G의 몫과 전단사 대응을 이룹니다. 부분군의 이러한 왼쪽 이동 작용은 / 표기법으로 군을 부분군으로 나눈 몫을 정의하는 데 사용되므로, 다음과 같은 간결한 명제를 사용할 수 있습니다.

example {G X : Type*} [Group G] [MulAction G X] (x : X) :
    orbit G x ≃ G ⧸ stabilizer G x :=
  MulAction.orbitEquivQuotientStabilizer G x

위의 두 결과를 결합한 중요한 특수한 경우는 X가 부분군 H의 평행이동 작용이 주어진 군 G인 경우입니다. 이 경우 모든 안정자군이 자명하므로 모든 궤도는 H와 전단사 대응을 이루며, 다음을 얻습니다:

example {G : Type*} [Group G] (H : Subgroup G) : G ≃ (G ⧸ H) × H :=
  groupEquivQuotientProdSubgroup

이것은 앞에서 본 라그랑주 정리의 개념적 변형입니다. 이 버전은 유한성 가정을 전혀 하지 않는다는 점에 주목하십시오.

이 절의 연습 문제로, 이전 연습 문제에서 정의한 conjugate를 사용하여 군이 자신의 부분군에 켤레로 작용하는 작용을 만들어 봅시다.

variable {G : Type*} [Group G]

lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
  sorry

instance : MulAction G (Subgroup G) where
  smul := conjugate
  one_smul := by
    sorry
  mul_smul := by
    sorry

end GroupActions

9.1.6. 몫군

앞에서 부분군이 군에 작용하는 것을 논의할 때 몫 G ⧸ H가 등장하는 것을 보았습니다. 일반적으로 이것은 타입일 뿐입니다. 몫 사상이 군 준동형사상이 되도록 하는 군 구조를 여기에 부여할 수 있는 것은 H가 정규 부분군일 때이며 오직 그때뿐입니다(그리고 이때 그 군 구조는 유일합니다).

정규성 가정은 타입 클래스 Subgroup.Normal이므로, 타입 클래스 추론이 이를 사용하여 몫 위의 군 구조를 유도할 수 있습니다.

noncomputable section QuotientGroup

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
  QuotientGroup.mk' H

몫군의 보편 성질은 QuotientGroup.lift를 통해 사용할 수 있습니다: 군 준동형사상 φ는 그 핵이 N을 포함하기만 하면 G ⧸ N으로 내려갑니다.

example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] {M : Type*}
    [Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
  QuotientGroup.lift N φ h

위 코드 조각에서 대상 군을 M이라고 부른 것은 M에 모노이드 구조만 있어도 충분하다는 단서입니다.

중요한 특수한 경우는 N = ker φ인 경우입니다. 이 경우 내려간 사상은 단사이며, 그 상으로의 군 동형사상을 얻습니다. 이 결과는 흔히 제1 동형사상 정리라고 불립니다.

example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
    G ⧸ MonoidHom.ker φ →* MonoidHom.range φ :=
  QuotientGroup.quotientKerEquivRange φ

사상 φ : G →* G'와 몫군 사영 Quotient.mk' N'의 합성에 보편 성질을 적용하면, G ⧸ N에서 G' ⧸ N'으로 가는 사상을 목표로 삼을 수도 있습니다. φ에 요구되는 조건은 보통 “φ가 N을 N' 안으로 보내야 한다”라고 표현됩니다. 그러나 이는 φ가 N'을 N 위로 당겨야 한다고 요구하는 것과 동치이며, 당김의 정의에는 존재 한정기호가 포함되지 않으므로 후자의 조건이 다루기 더 편합니다.

example {G G': Type*} [Group G] [Group G']
    {N : Subgroup G} [N.Normal] {N' : Subgroup G'} [N'.Normal]
    {φ : G →* G'} (h : N ≤ Subgroup.comap φ N') : G ⧸ N →* G' ⧸ N':=
  QuotientGroup.map N N' φ h

염두에 두어야 할 미묘한 점 하나는 타입 G ⧸ N이 (정의상 동등성의 수준에서) 실제로 N에 의존한다는 것입니다. 따라서 두 정규 부분군 N과 M이 같다는 증명이 있다고 해서 대응하는 몫 타입들이 정의상 같아지지는 않습니다. 하지만 이 경우에도 보편 성질은 동형사상을 제공합니다.

example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
    [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h

이 절의 마지막 연습 문제들로, H와 K가 유한군 G의 서로소인 정규 부분군이고 이들의 기수의 곱이 G의 기수와 같다면 G가 H × K와 동형임을 증명하겠습니다. 이 문맥에서 서로소라는 것은 H ⊓ K = ⊥임을 의미한다는 점을 상기하십시오.

먼저 부분군이 정규이거나 서로소라는 가정 없이 라그랑주 보조정리를 조금 다루어 보겠습니다.

section
variable {G : Type*} [Group G] {H K : Subgroup G}

open MonoidHom

#check Nat.card_pos -- The nonempty argument will be automatically inferred for subgroups
#check Subgroup.index_eq_card
#check Subgroup.index_mul_card
#check Nat.eq_of_mul_eq_mul_right

lemma aux_card_eq [Finite G] (h' : Nat.card G = Nat.card H * Nat.card K) :
    Nat.card (G ⧸ H) = Nat.card K := by
  sorry

이제부터 부분군들이 정규이고 서로소라고 가정하며, 기수 조건도 가정합니다. 이제 원하는 동형사상의 첫 번째 구성 요소를 만듭니다.

variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K)
  (h' : Nat.card G = Nat.card H * Nat.card K)

#check Nat.bijective_iff_injective_and_card
#check ker_eq_bot_iff
#check restrict
#check ker_restrict

def iso₁ : K ≃* G ⧸ H := by
  sorry

이제 두 번째 구성 요소를 정의할 수 있습니다. G₀에서 G₁으로 가는 사상과 G₀에서 G₂로 가는 사상으로부터 G₀에서 G₁ × G₂로 가는 사상을 만들어 주는 MonoidHom.prod가 필요합니다.

def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
  sorry

이제 모든 조각을 하나로 합칠 준비가 되었습니다.

#check MulEquiv.prodCongr

def finalIso : G ≃* H × K :=
  sorry

9.2. 환

9.2.1. 환, 환의 단원, 준동형사상, 부분환

타입 R 위의 환 구조의 타입은 Ring R입니다. 곱셈이 가환이라고 가정하는 변형은 CommRing R입니다. ring 택틱이 가환환의 공리로부터 따라 나오는 모든 등식을 증명한다는 것은 이미 살펴보았습니다.

example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

더 특이한 변형에서는 R 위의 덧셈이 군을 이룰 것을 요구하지 않고 덧셈 모노이드를 이루는 것만 요구합니다. 이에 대응하는 타입 클래스는 Semiring R과 CommSemiring R입니다. 자연수의 타입은 CommSemiring R의 중요한 인스턴스이며, 자연수 값을 가지는 함수의 타입도 모두 마찬가지입니다. 또 다른 중요한 예는 환의 아이디얼의 타입이며, 이는 아래에서 다룹니다. ring 택틱의 이름은 이중으로 오해를 불러일으킵니다. 교환법칙을 가정하지만 반환에서도 작동하기 때문입니다. 다시 말해, 이 택틱은 모든 CommSemiring에 적용됩니다.

example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

곱셈 항등원의 존재나 곱셈의 결합법칙을 가정하지 않는 환 클래스와 반환 클래스도 있습니다. 여기서는 이것들을 다루지 않겠습니다.

전통적으로 환론 입문에서 가르치는 개념 중 일부는 실제로는 그 바탕에 있는 곱셈 모노이드에 관한 것입니다. 대표적인 예가 환의 단원(unit) 정의입니다. 모든 (곱셈) 모노이드 M에는 양쪽 역원이 존재함을 나타내는 술어 IsUnit : M → Prop, Mˣ로 표기하는 단원들의 타입 Units M, 그리고 M으로의 강제 변환이 있습니다. Units M 타입은 가역 원소를 그 역원과 함께 묶으며, 둘이 실제로 서로의 역원임을 보장하는 성질도 함께 묶습니다. 이 구현 세부 사항은 주로 계산 가능한 함수를 정의할 때 중요합니다. 대부분의 경우에는 IsUnit.unit {x : M} : IsUnit x → Mˣ를 사용하여 단원을 만들 수 있습니다. 가환인 경우에는 x를 단원으로 본 것을 만들어 주는 Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ도 있습니다.

example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x

example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x

example {M : Type*} [Monoid M] : Group Mˣ := inferInstance

두 (반)환 R과 S 사이의 환 사상의 타입은 RingHom R S이며, 표기는 R →+* S입니다.

example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) :
    f (x + y) = f x + f y := f.map_add x y

example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ :=
  Units.map f

동형사상 버전은 RingEquiv이며, 표기는 ≃+*입니다.

부분 모노이드 및 부분군과 마찬가지로 환 R의 부분환을 나타내는 Subring R 타입이 있지만, 환을 부분환으로 나눈 몫을 만들 수는 없으므로 이 타입은 부분군 타입보다 훨씬 덜 유용합니다.

example {R : Type*} [Ring R] (S : Subring R) : Ring S := inferInstance

또한 RingHom.range가 부분환을 만든다는 점에도 주목하십시오.

9.2.2. 아이디얼과 몫

역사적인 이유로 Mathlib에는 가환환에 대한 아이디얼 이론만 있습니다. (환 라이브러리는 원래 현대 대수기하학의 기초를 향해 빠르게 나아가기 위해 개발되었습니다.) 따라서 이 절에서는 가환 (반)환을 다룹니다. R의 아이디얼은 R-가군으로 본 R의 부분가군으로 정의됩니다. 가군은 이후 선형대수 장에서 다루지만, 관련 보조정리 대부분이(전부는 아닙니다) 아이디얼이라는 특수한 문맥에서 다시 기술되어 있으므로 이 구현 세부 사항은 대체로 무시해도 괜찮습니다. 하지만 익명 사영 표기법이 항상 기대한 대로 동작하지는 않습니다. 예를 들어, 아래 코드 조각에서 Ideal.Quotient.mk I를 I.Quotient.mk로 바꿀 수 없습니다. .이 두 개 있어서 (Ideal.Quotient I).mk로 해석되는데, Ideal.Quotient 자체는 존재하지 않기 때문입니다.

example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
  Ideal.Quotient.mk I

example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
    Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
  Ideal.Quotient.eq_zero_iff_mem

몫환의 보편 성질은 Ideal.Quotient.lift입니다.

example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S)
    (H : I ≤ RingHom.ker f) : R ⧸ I →+* S :=
  Ideal.Quotient.lift I f H

특히 이로부터 환에 대한 제1 동형사상 정리를 얻습니다.

example {R S : Type*} [CommRing R] [CommRing S](f : R →+* S) :
    R ⧸ RingHom.ker f ≃+* f.range :=
  RingHom.quotientKerEquivRange f

아이디얼은 포함 관계에 대해 완비 격자 구조를 이루며, 반환 구조도 이룹니다. 이 두 구조는 서로 잘 맞물려 동작합니다.

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

example : I + J = I ⊔ J := rfl

example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by
  simp [Submodule.mem_sup]

example : I * J ≤ J := Ideal.mul_le_left

example : I * J ≤ I := Ideal.mul_le_right

example : I * J ≤ I ⊓ J := Ideal.mul_le_inf

환 사상을 사용하면 Ideal.map과 Ideal.comap을 이용해 아이디얼을 각각 앞으로 보내거나(푸시포워드) 뒤로 당길 수 있습니다. 늘 그렇듯이 후자는 존재 한정기호를 포함하지 않으므로 사용하기가 더 편리합니다. 몫환 사이의 준동형사상을 만들 수 있게 해 주는 조건을 기술할 때 후자를 사용하는 것도 이 때문입니다.

example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S)
    (H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J :=
  Ideal.quotientMap J f H

미묘한 점 하나는 타입 R ⧸ I가 (정의상 동등성 수준에서) 실제로 I에 의존한다는 것입니다. 따라서 두 아이디얼 I와 J가 같다는 증명이 있더라도 그것만으로는 대응하는 몫 타입들이 정의상 같아지지 않습니다. 하지만 이 경우에도 보편 성질이 동형사상을 제공해 줍니다.

example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
  Ideal.quotEquivOfEq h

이제 예시로 중국인의 나머지 동형사상을 제시할 수 있습니다. 첨자가 붙은 하한 기호 ⨅와 타입의 큰 곱 기호 Π의 차이에 주의하십시오. 사용하는 글꼴에 따라 이 둘을 구별하기가 꽤 어려울 수 있습니다.

example {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] (f : ι → Ideal R)
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
  Ideal.quotientInfRingEquivPiQuotient f hf

중국인의 나머지 정리의 기초적인 버전은 ZMod에 관한 명제로, 앞의 정리로부터 쉽게 유도할 수 있습니다:

open BigOperators PiNotation

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → (a i).Coprime (a j)) :
    ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
  ZMod.prodEquivPi a coprime

일련의 연습 문제를 통해 일반적인 경우의 중국인의 나머지 정리를 다시 증명하겠습니다.

먼저 몫환의 보편 성질을 사용하여, 정리에 나타나는 사상을 환 사상으로 정의해야 합니다.

variable {ι R : Type*} [CommRing R]
open Ideal Quotient Function

#check RingHom.pi
#check ker_Pi_Quotient_mk

/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
  Remainder Theorem. -/
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  sorry

다음 두 보조정리를 rfl로 증명할 수 있는지 확인하십시오.

lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
  sorry

lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
    chineseMap I (mk _ x) i = mk (I i) x :=
  sorry

다음 보조정리는 아이디얼들의 족에 대한 어떠한 가정도 없이 중국인의 나머지 정리의 쉬운 절반을 증명합니다. 이 증명은 한 줄도 채 되지 않습니다.

#check injective_lift_iff

lemma chineseMap_inj (I : ι → Ideal R) : Injective (chineseMap I) := by
  sorry

이제 정리의 핵심으로 들어갈 준비가 되었습니다. 이 부분에서는 chineseMap이 전사임을 보입니다. 먼저 서로소 조건(공극대성 가정이라고도 합니다)을 표현하는 여러 가지 방법을 알아야 합니다. 아래에서는 그중 처음 두 가지만 필요합니다.

#check IsCoprime
#check isCoprime_iff_add
#check isCoprime_iff_exists
#check isCoprime_iff_sup_eq
#check isCoprime_iff_codisjoint

이 기회에 Finset에 대한 귀납법을 사용해 보겠습니다. Finset에 관련된 보조정리는 아래와 같습니다. ring 택틱은 반환(semiring)에서도 작동하며, 환의 아이디얼들은 반환을 이룬다는 점을 기억하십시오.

#check Finset.mem_insert_of_mem
#check Finset.mem_insert_self

theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
  classical
  simp_rw [isCoprime_iff_add] at *
  induction s using Finset.induction with
  | empty =>
      simp
  | @insert i s _ hs =>
      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
      set K := ⨅ j ∈ s, J j
      calc
        1 = I + K                  := sorry
        _ = I + K * (I + J i)      := sorry
        _ = (1 + K) * I + K * J i  := sorry
        _ ≤ I + K ⊓ J i            := sorry

이제 중국인의 나머지 정리에 나오는 사상이 전사임을 증명할 수 있습니다.

lemma chineseMap_surj [Fintype ι] {I : ι → Ideal R}
    (hI : ∀ i j, i ≠ j → IsCoprime (I i) (I j)) : Surjective (chineseMap I) := by
  classical
  intro g
  choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      sorry
    sorry
  choose e he using key
  use mk _ (∑ i, f i * e i)
  sorry

이제 다음에서 모든 조각이 하나로 맞춰집니다:

noncomputable def chineseIso [Fintype ι] (f : ι → Ideal R)
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
  { Equiv.ofBijective _ ⟨chineseMap_inj f, chineseMap_surj hf⟩,
    chineseMap f with }

9.2.3. 대수와 다항식

가환 (반)환 R이 주어졌을 때, R 위의 대수란 R에서 A로 가는 환 사상을 갖추고 그 사상의 상이 A의 모든 원소와 교환되는 반환 A를 말합니다. 이는 타입 클래스 Algebra R A로 인코딩됩니다. R에서 A로 가는 준동형사상을 구조 사상(structure map)이라고 하며, Lean에서는 algebraMap R A : R →+* A로 표기합니다. 어떤 r : R에 대해 a : A에 algebraMap R A r을 곱하는 것을 a의 r에 의한 스칼라 곱셈이라고 하며, r • a로 표기합니다. 이러한 대수의 개념은 더 일반적인 대수 개념이 존재한다는 점을 강조하기 위해 때로 결합법칙을 만족하는 단위적 대수(associative unital algebra)라고 불린다는 점에 유의하십시오.

algebraMap R A가 환 사상이라는 사실에는 다음과 같은 스칼라 곱셈의 여러 성질이 함께 담겨 있습니다:

example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
    (r + r') • a = r • a + r' • a :=
  add_smul r r' a

example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
    (r * r') • a = r • r' • a :=
  mul_smul r r' a

두 R-대수 A와 B 사이의 사상은 R의 원소에 의한 스칼라 곱셈과 교환되는 환 사상입니다. 이들은 AlgHom R A B 타입을 갖는 묶인(bundled) 준동형사상이며, A →ₐ[R] B로 표기합니다.

비가환 대수의 중요한 예로는 자기준동형사상의 대수와 정사각 행렬의 대수가 있으며, 둘 다 선형대수 장에서 다룰 것입니다. 이 장에서는 가환 대수의 가장 중요한 예 중 하나인 다항식 대수를 살펴보겠습니다.

계수가 R에 속하는 일변수 다항식의 대수는 Polynomial R이라고 하며, Polynomial 네임스페이스를 열면 바로 R[X]로 쓸 수 있습니다. R에서 R[X]로 가는 대수 구조 사상은 C로 표기하는데, 대응하는 다항식 함수가 항상 상수이므로 이는 “constant”(상수)를 뜻합니다. 미정원은 X로 표기합니다.

open Polynomial

example {R : Type*} [CommRing R] : R[X] := X

example {R : Type*} [CommRing R] (r : R) := X - C r

위의 첫 번째 예제에서는 기대되는 타입을 정의의 본문으로부터 결정할 수 없으므로 Lean에 그 타입을 알려 주는 것이 매우 중요합니다. 두 번째 예제에서는 r의 타입이 알려져 있으므로 C r을 사용한 것으로부터 대상 다항식 대수를 추론할 수 있습니다.

C는 R에서 R[X]로 가는 환 사상이므로, 환 R[X]에서 계산하기 전에 map_zero, map_one, map_mul, map_pow 같은 모든 환 사상 보조정리를 사용할 수 있습니다. 예를 들면 다음과 같습니다:

example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
  rw [C.map_pow]
  ring

Polynomial.coeff를 사용하여 계수에 접근할 수 있습니다

example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp

example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp

영다항식이라는 특수한 경우 때문에 다항식의 차수를 정의하는 일은 항상 까다롭습니다. Mathlib에는 두 가지 변형이 있습니다. Polynomial.natDegree : R[X] → ℕ은 영다항식에 차수 0을 부여하고, Polynomial.degree : R[X] → WithBot ℕ은 ⊥를 부여합니다. 후자에서 WithBot ℕ은 ℕ ∪ {-∞}로 볼 수 있습니다. 다만 -∞가 완비 격자의 최소 원소와 같은 기호인 ⊥로 표기된다는 점이 다릅니다. 이 특별한 값은 영다항식의 차수로 사용되며, 덧셈에 대해 흡수적입니다. (⊥ * 0 = 0이라는 점을 제외하면 곱셈에 대해서도 거의 흡수적입니다.)

원칙적으로 말하자면 degree 버전이 올바른 쪽입니다. 예를 들어, 이 버전을 사용하면 (기반 환에 영인자가 없다고 가정할 때) 곱의 차수에 대해 기대하는 공식을 서술할 수 있습니다.

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    degree (p * q) = degree p + degree q :=
  Polynomial.degree_mul

반면 natDegree에 대한 버전은 다항식이 0이 아니라고 가정해야 합니다.

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} (hp : p ≠ 0) (hq : q ≠ 0) :
    natDegree (p * q) = natDegree p + natDegree q :=
  Polynomial.natDegree_mul hp hq

하지만 ℕ은 WithBot ℕ보다 훨씬 사용하기 편하므로, Mathlib은 두 버전을 모두 제공하며 둘 사이를 변환하는 보조정리도 제공합니다. 또한 합성의 차수를 계산할 때는 natDegree가 더 편리한 정의입니다. 다항식의 합성은 Polynomial.comp이며, 다음이 성립합니다:

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    natDegree (comp p q) = natDegree p * natDegree q :=
  Polynomial.natDegree_comp

다항식은 다항 함수를 만들어 냅니다. 모든 다항식은 Polynomial.eval을 사용하여 R 위에서 값을 계산할 수 있습니다.

example {R : Type*} [CommRing R] (P: R[X]) (x : R) := P.eval x

example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp

특히 IsRoot라는 술어가 있으며, 이는 다항식이 0이 되는 R의 원소 r에 대해 성립합니다.

example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl

R에 영인자가 없다고 가정할 때, 다항식은 중복도를 포함하여 센 근을 많아야 그 차수만큼 가진다고 말하고 싶습니다. 하지만 이번에도 영다항식의 경우가 골칫거리입니다. 그래서 Mathlib은 Polynomial.roots를 다항식 P를 중복집합으로 보내는 함수로 정의합니다. 즉, P가 0이면 공집합으로 정의되고, 그렇지 않으면 중복도를 포함한 P의 근들로 이루어진 유한 집합입니다. 이 정의는 기반 환이 정역일 때만 주어집니다. 그렇지 않으면 정의가 좋은 성질을 갖지 않기 때문입니다.

example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
  roots_X_sub_C r

example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ):
    ((X - C r) ^ n).roots = n • {r} :=
  by simp

Polynomial.eval과 Polynomial.roots는 모두 계수 환만 고려합니다. 이 함수들로는 X ^ 2 - 2 : ℚ[X]가 ℝ에서 근을 가진다거나 X ^ 2 + 1 : ℝ[X]가 ℂ에서 근을 가진다고 말할 수 없습니다. 이를 위해서는 P : R[X]를 임의의 R-대수에서 평가하는 Polynomial.aeval이 필요합니다. 더 정확히 말하면, 반환 A와 Algebra R A 인스턴스가 주어졌을 때 Polynomial.aeval은 모든 원소 a : A를 X에 a를 대입하여 평가하는 R-대수 준동형사상 R[X] → A로 보냅니다. AlgHom은 함수로의 강제 변환을 가지므로 이를 다항식에 적용할 수 있습니다. 하지만 aeval은 다항식을 인자로 받지 않으므로 위의 P.eval에서처럼 점 표기법을 사용할 수 없습니다.

example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp

이 문맥에서 roots에 대응하는 함수는 aroots로, 다항식과 대수를 차례로 받아 중복집합(multiset)을 출력합니다(영다항식에 관해서는 roots와 같은 주의 사항이 적용됩니다).

open Complex Polynomial

example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
  suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    have key : (C I * C I : ℂ[X]) = -1 := by simp [← C_mul]
    rw [C_neg]
    linear_combination key
  have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
    intro H
    apply_fun eval 0 at H
    simp [eval] at H
  simp only [factored, roots_mul p_ne_zero, roots_X_sub_C]
  rfl

-- Mathlib knows about D'Alembert-Gauss theorem: ``ℂ`` is algebraically closed.
example : IsAlgClosed ℂ := inferInstance

더 일반적으로, 환 사상 f : R →+* S가 주어지면 Polynomial.eval₂를 사용하여 P : R[X]를 S의 한 점에서 평가할 수 있습니다. 이 함수는 Algebra R S 인스턴스의 존재를 가정하지 않으므로 R[X]에서 S로 가는 실제 함수를 만들어 내며, 따라서 점 표기법이 예상대로 작동합니다.

#check (Complex.ofRealHom : ℝ →+* ℂ)

example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofRealHom Complex.I = 0 := by simp

끝으로 다변수 다항식을 간단히 언급하며 마무리합시다. 가환 반환 R이 주어졌을 때, 계수가 R에 속하고 부정원이 타입 σ로 첨자화된 다항식들의 R-대수는 MVPolynomial σ R입니다. i : σ가 주어지면 대응하는 다항식은 MvPolynomial.X i입니다. (평소처럼 MVPolynomial 네임스페이스를 열어 이를 X i로 줄여 쓸 수 있습니다.) 예를 들어 미지수가 두 개 필요하다면 σ로 Fin 2를 사용하여 \(\mathbb{R}^2`\)에서 단위원을 정의하는 다항식을 다음과 같이 쓸 수 있습니다:

open MvPolynomial

def circleEquation : MvPolynomial (Fin 2) ℝ := X 0 ^ 2 + X 1 ^ 2 - 1

함수 적용은 우선순위가 매우 높으므로 위 표현식은 (X 0) ^ 2 + (X 1) ^ 2 - 1로 읽힌다는 점을 기억하십시오. 이 식을 계산하여 좌표가 \((1, 0)\)인 점이 원 위에 있는지 확인할 수 있습니다. ![...] 표기법은 Fin n → X의 원소를 나타낸다는 점을 기억하십시오. 여기서 자연수 n은 인자의 개수로 결정되고, 타입 X는 인자의 타입으로 결정됩니다.

example : MvPolynomial.eval ![1, 0] circleEquation = 0 := by simp [circleEquation]