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으로 씁니다. Lean은 그러한 사상을 M의 원소에 적용하면 자동으로 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 example {G H : Type*} [Group G] [Group H]
    (f : G →* H) (h : Function.Bijective f) :
    G ≃* H :=
  MulEquiv.ofBijective f h

9.1.3. 부분군

군 준동형사상이 번들로 묶이는 것과 마찬가지로, 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이라고 부르는 것입니다. 이는 일반적인 수학 용어는 아니지만, “pushforward”나 “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에서의 부분군 소개를 마칩시다. 라그랑주 정리는 유한군의 부분군의 크기가 그 군의 크기를 나눈다는 것을 말합니다. Sylow의 첫 번째 정리는 라그랑주 정리의 유명한 부분적인 역입니다.

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[]는 순환치환을 정의하는 데 사용됩니다. 이 예제에서 결과는 ℕ의 순열입니다. Perm (Fin 5)에서의 계산이 되도록 하려면, 처음 나오는 숫자에 (1 : Fin 5)와 같은 타입 명시(type ascription)를 사용할 수 있습니다.

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

구체적인 군을 다루는 또 다른 방법은 자유군과 군의 표시를 사용하는 것입니다. 타입 α에 대한 자유군은 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 절에서 살펴보겠습니다.) 이를 정의 뒤에 어느 정도 숨겨두었으므로, myGroup에 군 인스턴스 생성을 강제하기 위해 deriving Group을 사용합니다.

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. 군 작용

군론이 나머지 수학과 상호작용하는 중요한 한 가지 방법은 군 작용을 사용하는 것입니다. 어떤 타입 X에 대한 군 G의 작용은 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

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

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

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

전통적으로 환론 입문에서 가르치는 몇몇 개념은 실제로는 바탕이 되는 곱셈 모노이드에 관한 것입니다. 대표적인 예는 환의 단위원의 정의입니다. 모든 (곱셈) 모노이드 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에 대한 대수란 그 상이 A의 모든 원소와 교환하는, R에서 A로 가는 환 준동형사상을 갖춘 반환 A를 말합니다. 이는 타입 클래스 Algebra R A로 인코딩됩니다. R에서 A로 가는 준동형사상은 구조 사상(structure map)이라 불리며, Lean에서는 algebraMap R A : R →+* A로 표기됩니다. 어떤 r : R에 대해 algebraMap R A r로 a : A를 곱하는 것을 r에 의한 a의 스칼라 곱셈이라 하며, r • a로 표기합니다. 이러한 대수 개념은 더 일반적인 대수 개념이 존재함을 강조하기 위해 때때로 결합 단위 대수라고 불린다는 점에 유의하십시오.

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인 번들 준동형사상이며, 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

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

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

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

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로, 이는 다항식과 그 다음 대수를 받아 멀티집합을 출력합니다(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)\)인 점이 원 위에 있는지 확인하기 위해 이를 계산해볼 수 있습니다. ![...] 표기법은 인자의 개수로 결정되는 어떤 자연수 n과 인자의 타입으로 결정되는 어떤 타입 X에 대해 Fin n → X의 원소를 나타낸다는 점을 기억하십시오.

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