8. 계층 구조

Chapter 7에서 군의 클래스를 정의하고 이 클래스의 인스턴스를 만드는 방법을 살펴보았으며, 이어서 가환환 클래스의 인스턴스를 만드는 방법도 살펴보았습니다. 그러나 물론 여기에는 계층 구조가 있습니다. 가환환은 특히 덧셈군이기도 합니다. 이 장에서는 이러한 계층 구조를 만드는 방법을 공부하겠습니다. 계층 구조는 수학의 모든 분야에 나타나지만, 이 장에서는 대수적인 예제에 중점을 두겠습니다.

기존 계층 구조를 사용하는 방법을 더 논의하기도 전에 계층 구조를 만드는 방법을 논의하는 것은 시기상조로 보일 수 있습니다. 그러나 계층 구조를 사용하려면 그 밑바탕에 있는 기술을 어느 정도 이해해야 합니다. 그러므로 이 장은 읽어 두는 것이 좋지만, 처음 읽을 때 모든 것을 기억하려고 너무 애쓰지는 마시고, 이어지는 장들을 읽은 다음 다시 이곳으로 돌아와 한 번 더 읽으십시오.

이 장에서는 Mathlib에 나오는 여러 가지를 (더 단순한 형태로) 다시 정의하므로, 우리 버전을 구분하기 위해 첨자를 사용하겠습니다. 예를 들어 Ring의 우리 버전으로 Ring₁을 두겠습니다. 구조를 형식화하는 더 강력한 방법을 점차 설명해 나갈 것이므로, 이 첨자가 때로는 1보다 커지기도 합니다.

8.1. 기초

Lean의 모든 계층 구조의 가장 밑바닥에는 데이터를 담는 클래스가 있습니다. 다음 클래스는 주어진 타입 α에 one이라는 특별한 원소가 주어져 있다는 사실을 기록합니다. 이 단계에서는 아무런 성질도 갖지 않습니다.

class One₁ (α : Type) where
  /-- The element one -/
  one : α

이 장에서는 클래스를 훨씬 더 많이 사용할 것이므로, class 명령이 하는 일을 좀 더 자세히 이해할 필요가 있습니다. 먼저, 위의 class 명령은 매개변수 α : Type과 하나의 필드 one을 갖는 구조체 One₁을 정의합니다. 또한 이 구조체를 클래스로 표시하여, 어떤 타입 α에 대해 One₁ α 타입의 인자가 인스턴스 암시적 인자로 표시되어 있는 한, 즉 대괄호 사이에 나타나는 한, 인스턴스 해결 절차를 통해 추론될 수 있도록 합니다. 이 두 가지 효과는 class 속성과 함께 structure 명령을 사용하여, 즉 class 대신 @[class] structure를 작성하여 얻을 수도 있었습니다. 하지만 class 명령은 One₁ α가 자기 자신의 필드에서 인스턴스 암시적 인자로 나타나도록 보장하기도 합니다. 다음을 비교해 보십시오

#check One₁.one -- One₁.one {α : Type} [self : One₁ α] : α

@[class] structure One₂ (α : Type) where
  /-- The element one -/
  one : α

#check One₂.one

두 번째 확인에서 self : One₂ α가 명시적 인자임을 볼 수 있습니다. 첫 번째 버전이 실제로 아무런 명시적 인자 없이 사용될 수 있는지 확인해 봅시다.

example (α : Type) [One₁ α] : α := One₁.one

참고: 위 예제에서 인수 One₁ α는 인스턴스 암시적(instance-implicit)으로 표시되어 있습니다. 하지만 이 표시는 선언을 사용할 때에만 영향을 주고 example 명령으로 만든 선언은 사용할 수 없으므로, 다소 무의미한 일입니다. 그래도 이렇게 하면 그 인수에 이름을 붙이지 않아도 되며, 더 중요하게는 One₁ α 인수를 인스턴스 암시적으로 표시하는 좋은 습관을 들이기 시작할 수 있습니다.

또 하나 참고할 점은, 이 모든 것이 Lean이 α가 무엇인지 알 때에만 작동한다는 것입니다. 위 예제에서 타입 지정 : α를 빼면 typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α)와 같은 오류 메시지가 발생합니다. 여기서 ?m.263 α는 “α에 의존하는 어떤 타입”을 뜻합니다(263은 자동으로 생성된 번호일 뿐이며, 알 수 없는 것이 여러 개일 때 서로 구별하는 데 유용합니다). 이 문제를 피하는 또 다른 방법은 다음과 같이 타입 표기를 사용하는 것입니다:

example (α : Type) [One₁ α] := (One₁.one : α)

제 3.6 절에서 수열의 극한을 다루면서, 예를 들어 이 부등식이 자연수에 관한 것인지 실수에 관한 것인지 Lean에 알려 주지 않고 0 < 1을 서술하려 했다면 이미 이 문제를 겪었을 수도 있습니다.

다음으로 할 일은 One₁.one에 표기법을 부여하는 것입니다. 1에 대한 내장 표기법과 충돌하지 않도록 𝟙을 사용하겠습니다. 이는 다음 명령으로 할 수 있으며, 첫 번째 줄은 One₁.one의 문서를 기호 𝟙의 문서로 사용하라고 Lean에 지시합니다.

@[inherit_doc]
notation "𝟙" => One₁.one

example {α : Type} [One₁ α] : α := 𝟙

example {α : Type} [One₁ α] : (𝟙 : α) = 𝟙 := rfl

이제 이항 연산을 기록하는, 데이터를 담는 클래스가 필요합니다. 지금은 덧셈과 곱셈 중 하나를 고르고 싶지 않으므로 다이아몬드 기호를 사용하겠습니다.

class Dia₁ (α : Type) where
  dia : α → α → α

infixl:70 " ⋄ "   => Dia₁.dia

One₁ 예제에서와 마찬가지로, 이 단계에서 연산은 아무런 성질도 갖지 않습니다. 이제 연산이 ⋄로 표기되는 반군 구조의 클래스를 정의해 봅시다. 일단은 이것을 두 개의 필드, 즉 Dia₁ 인스턴스와 ⋄의 결합법칙을 나타내는 Prop 값 필드 dia_assoc를 가진 구조체로 직접 정의합니다.

class Semigroup₀ (α : Type) where
  toDia₁ : Dia₁ α
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

dia_assoc를 기술하는 동안 앞서 정의한 필드 toDia₁이 지역 문맥에 있으므로, Lean이 a ⋄ b의 의미를 파악하기 위해 Dia₁ α의 인스턴스를 찾을 때 이를 사용할 수 있다는 점에 유의하십시오. 그러나 이 toDia₁ 필드는 타입 클래스 인스턴스 데이터베이스의 일부가 되지 않습니다. 따라서 example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b를 실행하면 failed to synthesize instance Dia₁ α라는 오류 메시지와 함께 실패합니다.

나중에 instance 속성을 추가하여 이를 해결할 수 있습니다(reducible 속성은 신경 쓰지 마십시오. 다음 단락에서 더 나은 방법을 설명하고 나면 필요하지 않습니다).

attribute [reducible, instance] Semigroup₀.toDia₁

example {α : Type} [Semigroup₀ α] (a b : α) : α := a ⋄ b

본격적으로 쌓아 올리기 전에, 이 toDia₁ 필드를 추가하려면 다른 구문을 사용해야 합니다. 이를 통해 Lean에게 Dia₁ α의 필드를 마치 Semigroup₁ 자체의 필드인 것처럼 다루어야 한다고 알려 줍니다. 이렇게 하면 toDia₁ 인스턴스도 자동으로 추가되어 편리합니다. class 명령은 다음과 같이 extends 구문을 사용해 이를 지원합니다:

class Semigroup₁ (α : Type) extends toDia₁ : Dia₁ α where
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b

이 구문은 structure 명령에서도 사용할 수 있습니다. 다만 그 경우에는 정의할 인스턴스가 없으므로 toDia₁과 같은 필드를 작성하는 번거로움만 해결해 줍니다.

필드 이름 toDia₁은 extends 구문에서 생략할 수 있습니다. 생략하면 확장되는 클래스의 이름 앞에 “to”를 붙인 이름이 기본값으로 쓰입니다.

class Semigroup₂ (α : Type) extends Dia₁ α where
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

이제 다이아몬드 연산과 특별한 원소 1을 결합하고, 이 원소가 양쪽 모두에서 중립원이라는 공리를 덧붙여 봅시다.

class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
  /-- One is a left neutral element for diamond. -/
  one_dia : ∀ a : α, 𝟙 ⋄ a = a
  /-- One is a right neutral element for diamond -/
  dia_one : ∀ a : α, a ⋄ 𝟙 = a

다음 예제에서는 α가 DiaOneClass₁ 구조를 가진다는 것을 Lean에 알려 주고, Dia₁ 인스턴스와 One₁ 인스턴스를 모두 사용하는 성질을 서술합니다. Lean이 이러한 인스턴스를 어떻게 찾는지 보기 위해 추적 옵션을 설정하며, 그 결과는 Infoview에서 확인할 수 있습니다. 이 결과는 기본적으로 다소 간결하지만, 검은 화살표로 끝나는 줄을 클릭하면 펼쳐 볼 수 있습니다. 여기에는 Lean이 성공하기에 충분한 타입 정보를 얻기 전에 인스턴스를 찾으려다 실패한 시도도 포함되어 있습니다. 성공한 시도에는 실제로 extends 구문이 생성한 인스턴스가 사용됩니다.

set_option trace.Meta.synthInstance true in
example {α : Type} [DiaOneClass₁ α] (a b : α) : Prop := a ⋄ b = 𝟙

기존 클래스를 결합할 때는 추가 필드를 포함할 필요가 없다는 점에 유의하십시오. 따라서 모노이드를 다음과 같이 정의할 수 있습니다:

class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α

위의 정의는 간단해 보이지만, 중요한 미묘함이 숨어 있습니다. Semigroup₁ α와 DiaOneClass₁ α는 모두 Dia₁ α를 확장하므로, Monoid₁ α 인스턴스가 α 위에 서로 무관한 두 개의 다이아몬드 연산, 즉 Monoid₁.toSemigroup₁ 필드에서 오는 연산과 Monoid₁.toDiaOneClass₁ 필드에서 오는 연산을 제공하지 않을까 우려할 수도 있습니다.

실제로 다음과 같이 모노이드 클래스를 직접 만들어 보면:

class Monoid₂ (α : Type) where
  toSemigroup₁ : Semigroup₁ α
  toDiaOneClass₁ : DiaOneClass₁ α

서로 전혀 관계없는 두 다이아몬드 연산 Monoid₂.toSemigroup₁.toDia₁.dia와 Monoid₂.toDiaOneClass₁.toDia₁.dia가 생깁니다.

extends 구문을 사용하여 생성한 버전에는 이러한 결함이 없습니다.

example {α : Type} [Monoid₁ α] :
  (Monoid₁.toSemigroup₁.toDia₁.dia : α → α → α) = Monoid₁.toDiaOneClass₁.toDia₁.dia := rfl

즉, class 명령이 우리를 위해 일종의 마법을 부린 것입니다(structure 명령도 마찬가지로 그렇게 했을 것입니다). 우리 클래스의 필드가 무엇인지 쉽게 확인하는 방법은 생성자를 살펴보는 것입니다. 다음을 비교해 보십시오:

/- Monoid₂.mk {α : Type} (toSemigroup₁ : Semigroup₁ α) (toDiaOneClass₁ : DiaOneClass₁ α) : Monoid₂ α -/
#check Monoid₂.mk

/- Monoid₁.mk {α : Type} [toSemigroup₁ : Semigroup₁ α] [toOne₁ : One₁ α] (one_dia : ∀ (a : α), 𝟙 ⋄ a = a) (dia_one : ∀ (a : α), a ⋄ 𝟙 = a) : Monoid₁ α -/
#check Monoid₁.mk

이를 통해 Monoid₁은 예상대로 Semigroup₁ α 인수를 받지만, 겹칠 수 있는 DiaOneClass₁ α 인수는 받지 않고 대신 이를 분해하여 겹치지 않는 부분만 포함한다는 것을 알 수 있습니다. 또한 Monoid₁.toDiaOneClass₁ 인스턴스도 자동으로 생성되었습니다. 이 인스턴스는 필드는 아니지만 기대한 시그니처를 가지므로, 최종 사용자의 관점에서 확장된 두 클래스 Semigroup₁과 DiaOneClass₁ 사이의 대칭성을 회복시킵니다.

#check Monoid₁.toSemigroup₁
#check Monoid₁.toDiaOneClass₁

이제 군을 정의하기 직전까지 왔습니다. 모노이드 구조에 모든 원소마다 역원이 존재한다는 필드를 추가할 수도 있습니다. 하지만 그렇게 하면 이 역원들을 사용하려 할 때마다 따로 작업을 해야 합니다. 실제로는 역원을 데이터로 추가하는 편이 더 편리합니다. 재사용성을 높이기 위해, 데이터를 담는 새로운 클래스를 정의한 다음 표기법을 부여합니다.

class Inv₁ (α : Type) where
  /-- The inversion function -/
  inv : α → α

@[inherit_doc]
postfix:max "⁻¹" => Inv₁.inv

class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
  inv_dia : ∀ a : G, a⁻¹ ⋄ a = 𝟙

위의 정의는 너무 약해 보일 수 있습니다. a⁻¹이 a의 왼쪽 역원이라는 것만 요구하기 때문입니다. 하지만 반대쪽은 자동으로 성립합니다. 이를 증명하려면 예비 보조정리가 필요합니다.

lemma left_inv_eq_right_inv₁ {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← DiaOneClass₁.one_dia c, ← hba, Semigroup₁.dia_assoc, hac, DiaOneClass₁.dia_one b]

이 보조정리에서는 전체 이름을 적는 것이 꽤 번거롭습니다. 특히 계층 구조의 어느 부분이 그 사실들을 제공하는지 알아야 하기 때문입니다. 이를 해결하는 한 가지 방법은 export 명령을 사용하여 그 사실들을 루트 이름 공간의 보조정리로 복사하는 것입니다.

export DiaOneClass₁ (one_dia dia_one)
export Semigroup₁ (dia_assoc)
export Group₁ (inv_dia)

그러면 위의 증명을 다음과 같이 다시 쓸 수 있습니다:

example {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← one_dia c, ← hba, dia_assoc, hac, dia_one b]

이제 여러분이 우리가 만든 대수적 구조에 관한 사실들을 증명할 차례입니다.

lemma inv_eq_of_dia [Group₁ G] {a b : G} (h : a ⋄ b = 𝟙) : a⁻¹ = b :=
  sorry

lemma dia_inv [Group₁ G] (a : G) : a ⋄ a⁻¹ = 𝟙 :=
  sorry

이 단계에서 환을 정의하는 단계로 넘어가고 싶지만, 심각한 문제가 하나 있습니다. 어떤 타입 위의 환 구조는 덧셈군 구조와 곱셈 모노이드 구조를 모두 포함하며, 둘 사이의 상호작용에 관한 몇 가지 성질도 포함합니다. 그러나 지금까지 우리는 모든 연산에 ⋄ 표기법을 하드코딩했습니다. 더 근본적으로, 타입 클래스 시스템은 모든 타입이 각 타입 클래스의 인스턴스를 하나만 가진다고 가정합니다. 이 문제를 해결하는 방법은 여러 가지가 있습니다. 놀랍게도 Mathlib은 코드를 생성하는 속성의 도움을 받아 덧셈 이론과 곱셈 이론을 위해 모든 것을 중복해서 만드는 단순한 방법을 사용합니다. 구조체와 클래스는 덧셈 표기법과 곱셈 표기법 양쪽으로 정의되며, to_additive 속성이 둘을 연결합니다. 반군처럼 다중 상속이 있는 경우에는 자동 생성된 “대칭 복원” 인스턴스에도 표시를 해 주어야 합니다. 이는 다소 기술적인 내용이므로 세부 사항까지 이해할 필요는 없습니다. 중요한 점은, 그러면 보조정리를 곱셈 표기법으로만 서술하고 to_additive 속성을 붙여 덧셈 버전을 생성한다는 것입니다. 예를 들어 left_inv_eq_right_inv'로부터 자동 생성된 덧셈 버전 left_neg_eq_right_neg'가 만들어집니다. 이 덧셈 버전의 이름을 확인하기 위해 left_inv_eq_right_inv' 위에 whatsnew in 명령을 사용했습니다.

class AddSemigroup₃ (α : Type) extends Add α where
  /-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
  /-- Multiplication is associative -/
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α

@[to_additive AddMonoid₃]
class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α

export Semigroup₃ (mul_assoc₃)
export AddSemigroup₃ (add_assoc₃)

whatsnew in
@[to_additive]
lemma left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]

#check left_neg_eq_right_neg'

이 기법을 갖추면 가환 반군, 모노이드, 군도 쉽게 정의할 수 있고, 그다음 환을 정의할 수 있습니다.

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
  add_comm : ∀ a b : α, a + b = b + a

@[to_additive AddCommSemigroup₃]
class CommSemigroup₃ (α : Type) extends Semigroup₃ α where
  mul_comm : ∀ a b : α, a * b = b * a

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

@[to_additive AddCommMonoid₃]
class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α

class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
  neg_add : ∀ a : G, -a + a = 0

@[to_additive AddGroup₃]
class Group₃ (G : Type) extends Monoid₃ G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1

적절한 경우에는 보조정리에 simp 태그를 붙이는 것을 잊지 말아야 합니다.

attribute [simp] Group₃.inv_mul AddGroup₃.neg_add

그다음에는 표준 표기법으로 바꾸기 때문에 같은 내용을 조금 반복해야 하지만, 적어도 to_additive가 곱셈 표기법을 덧셈 표기법으로 옮기는 일을 대신해 줍니다.

@[to_additive]
lemma inv_eq_of_mul [Group₃ G] {a b : G} (h : a * b = 1) : a⁻¹ = b :=
  sorry

다음과 같이 to_additive에게 보조정리에 simp 태그를 붙이고 그 속성을 덧셈 버전에도 전파하도록 요청할 수 있다는 점에 유의하십시오.

@[to_additive (attr := simp)]
lemma Group₃.mul_inv {G : Type} [Group₃ G] (a : G) : a * a⁻¹ = 1 := by
  sorry

@[to_additive]
lemma mul_left_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : a * b = a * c) : b = c := by
  sorry

@[to_additive]
lemma mul_right_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : b*a = c*a) : b = c := by
  sorry

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

@[to_additive AddCommGroup₃]
class CommGroup₃ (G : Type) extends Group₃ G, CommMonoid₃ G

이제 환을 다룰 준비가 되었습니다. 시연을 위해 덧셈이 가환이라고 가정하지 않고, 곧바로 AddCommGroup₃의 인스턴스를 제공하겠습니다. Mathlib은 이런 방식을 쓰지 않습니다. 첫째로 실제로는 이렇게 해도 환 인스턴스를 만드는 일이 조금도 쉬워지지 않기 때문이고, 둘째로 Mathlib의 대수적 계층 구조는 반환(semiring)을 거치는데, 반환은 환과 비슷하지만 덧셈 역원이 없어서 아래 증명이 반환에는 통하지 않기 때문입니다. 여기서 얻는 것은, 이를 처음 보는 분께는 좋은 연습 문제가 된다는 점 외에도, 부모 구조를 인스턴스 매개변수로 제공한 다음 추가 필드를 채울 수 있게 해 주는 구문을 사용하여 인스턴스를 구축하는 예시입니다. 여기서 Ring₃ R 인수는 add_comm을 제외하고 AddCommGroup₃ R이 요구하는 모든 것을 제공합니다.

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
  /-- Multiplication is left distributive over addition -/
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  /-- Multiplication is right distributive over addition -/
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
{ add_comm := by
    sorry }

물론 정수 위의 환 구조와 같은 구체적인 인스턴스도 만들 수 있습니다(물론 아래 인스턴스는 모든 작업이 이미 Mathlib에서 끝나 있다는 점을 활용합니다).

instance : Ring₃ ℤ where
  add := (· + ·)
  add_assoc₃ := add_assoc
  zero := 0
  zero_add := by simp
  add_zero := by simp
  neg := (- ·)
  neg_add := by simp
  mul := (· * ·)
  mul_assoc₃ := mul_assoc
  one := 1
  one_mul := by simp
  mul_one := by simp
  zero_mul := by simp
  mul_zero := by simp
  left_distrib := Int.mul_add
  right_distrib := Int.add_mul

연습 문제로, 이제 순서 관계를 위한 간단한 계층 구조를 세워 보십시오. 여기에는 순서 가환 모노이드를 위한 클래스도 포함됩니다. 순서 가환 모노이드는 부분 순서와 가환 모노이드 구조를 모두 가지며 ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b를 만족합니다. 물론 다음 클래스들에 필드를 추가해야 하며, 경우에 따라 extends 절도 추가해야 합니다.

class LE₁ (α : Type) where
  /-- The Less-or-Equal relation. -/
  le : α → α → Prop

@[inherit_doc] infix:50 " ≤₁ " => LE₁.le

class Preorder₁ (α : Type)

class PartialOrder₁ (α : Type)

class OrderedCommMonoid₁ (α : Type)

instance : OrderedCommMonoid₁ ℕ where

이제 여러 타입이 관여하는 대수적 구조를 살펴보고자 합니다. 대표적인 예는 환 위의 가군입니다. 가군이 무엇인지 모른다면, 가군을 벡터 공간이라고 생각하고 여기서 다루는 환이 모두 체라고 여겨도 됩니다. 이러한 구조는 어떤 환의 원소에 의한 스칼라 곱셈을 갖춘 가환 덧셈군입니다.

먼저 어떤 타입 α에 의한 어떤 타입 β 위의 스칼라 곱셈을 나타내는, 데이터를 담는 타입 클래스를 정의하고, 여기에 우결합법칙을 따르는 표기를 부여합니다.

class SMul₃ (α : Type) (β : Type) where
  /-- Scalar multiplication -/
  smul : α → β → β

infixr:73 " • " => SMul₃.smul

그런 다음 가군을 정의할 수 있습니다(가군이 무엇인지 모른다면 이번에도 벡터 공간을 떠올리십시오).

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

여기서 흥미로운 일이 일어나고 있습니다. R 위의 환 구조가 이 정의의 매개변수라는 점은 그리 놀랍지 않지만, SMul₃ R M과 마찬가지로 AddCommGroup₃ M도 extends 절에 들어갈 것이라고 예상하셨을 것입니다. 그렇게 하려고 하면 인스턴스로 표시된 Module₃.toAddCommGroup₃ 필드가 생기게 됩니다. 이 인스턴스는 다음과 같은 시그니처를 갖게 됩니다: (R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M. 타입 클래스 데이터베이스에 이러한 인스턴스가 있으면, Lean은 어떤 M에 대해 AddCommGroup₃ M 인스턴스를 찾을 때마다 Module₁ R M 인스턴스를 찾는 본 임무에 나서기 전에 전혀 지정되지 않은 타입 R과 Ring₃ R 인스턴스를 찾아 헤매야 합니다. 이 두 부수 임무는 오류 메시지에 언급된 메타변수로 나타나며, 거기서는 ?R과 ?inst✝로 표기됩니다. 따라서 이러한 Module₃.toAddCommGroup₃ 인스턴스는 인스턴스 해결 절차에 커다란 함정이 됩니다.

그렇다면 extends SMul₃ R M은 어떻습니까? 이것은 Module₁.toSMul₃ : {R : Type} →  [inst : Ring₃ R] → {M : Type} → [inst_1 : AddCommGroup₃ M] → [self : Module₁ R M] → SMul₃ R M 필드를 만드는데, 그 최종 결과인 SMul₃ R M이 R과 M을 모두 언급하므로 이 필드는 인스턴스로 안전하게 사용할 수 있습니다. 규칙은 기억하기 쉽습니다: extends 절에 나타나는 각 클래스는 매개변수에 나타나는 모든 타입을 언급해야 합니다.

첫 번째 가군 인스턴스를 만들어 봅시다: 환은 자신의 곱셈을 스칼라 곱셈으로 사용하여 자기 자신 위의 가군이 됩니다.

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
  smul := fun r s ↦ r*s
  zero_smul := zero_mul
  one_smul := one_mul
  mul_smul := mul_assoc₃
  add_smul := Ring₃.right_distrib
  smul_add := Ring₃.left_distrib

두 번째 예로, 모든 아벨 군은 ℤ 위의 가군입니다(이는 역원이 없는 스칼라를 허용하여 벡터 공간 이론을 일반화하는 이유 중 하나입니다). 먼저 0과 덧셈을 갖춘 임의의 타입에 대해 자연수에 의한 스칼라 곱셈을 정의할 수 있습니다. n • a는 a가 n 번 나타나는 a + ⋯ + a로 정의됩니다. 그런 다음 (-1) • a = -a가 성립하도록 하여 이를 정수에 의한 스칼라 곱셈으로 확장합니다.

def nsmul₁ {M : Type*} [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | n + 1, a => a + nsmul₁ n a

def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M
  | Int.ofNat n, a => nsmul₁ n a
  | Int.negSucc n, a => -nsmul₁ n.succ a

이것이 가군 구조를 이룬다는 것을 증명하는 일은 다소 지루하고 지금의 논의에서는 흥미롭지 않으므로, 모든 공리를 sorry로 처리하겠습니다. 이 sorry들을 증명으로 바꾸라고 요구하는 것은 아닙니다. 굳이 그렇게 하겠다면 nsmul₁과 zsmul₁에 관한 몇 가지 중간 보조정리를 세우고 증명하는 것이 좋을 것입니다.

instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
  smul := zsmul₁
  zero_smul := sorry
  one_smul := sorry
  mul_smul := sorry
  add_smul := sorry
  smul_add := sorry

훨씬 더 중요한 문제는 이제 ℤ 자신에 대해 환 ℤ 위의 가군 구조가 두 개 있다는 점입니다. ℤ가 아벨 군이므로 abGrpModule ℤ가 있고, ℤ가 환이므로 selfModule ℤ가 있습니다. 이 두 가군 구조는 같은 아벨 군 구조에 대응하지만, 두 구조의 스칼라 곱셈이 같은지는 분명하지 않습니다. 실제로 같기는 하지만 이는 정의에 의해 참인 것이 아니며, 증명이 필요합니다. 이는 타입 클래스 인스턴스 해결 절차에 매우 나쁜 소식이며, 이 계층의 사용자는 매우 답답한 실패를 겪게 됩니다. 인스턴스를 찾으라고 직접 요청하면 Lean은 그중 하나를 고르며, 다음을 사용하여 어느 것을 골랐는지 확인할 수 있습니다:

#synth Module₁ ℤ ℤ -- abGrpModule ℤ

하지만 더 간접적인 문맥에서는 Lean이 다른 쪽을 추론하여 혼란에 빠지는 일이 생길 수 있습니다. 이러한 상황을 나쁜 다이아몬드(bad diamond)라고 합니다. 이는 위에서 사용한 다이아몬드 연산과는 아무 관련이 없으며, ℤ에서 그 Module₁ ℤ로 가는 경로를 AddCommGroup₃ ℤ 또는 Ring₃ ℤ 중 하나를 거쳐 그릴 수 있다는 점을 가리킵니다.

모든 다이아몬드가 나쁜 것은 아니라는 점을 이해하는 것이 중요합니다. 실제로 Mathlib 곳곳에 다이아몬드가 있으며, 이 장에도 있습니다. 이미 맨 처음에 Monoid₁ α에서 Dia₁ α로 Semigroup₁ α 또는 DiaOneClass₁ α 중 하나를 거쳐 갈 수 있음을 보았으며, class 명령이 수행하는 작업 덕분에 그 결과로 얻는 두 Dia₁ α 인스턴스는 정의상 같습니다. 특히 맨 아래에 Prop 값을 갖는 클래스가 있는 다이아몬드는 나쁠 수 없습니다. 같은 명제에 대한 어떤 두 증명이든 정의상 같기 때문입니다.

하지만 가군으로 만든 이 다이아몬드는 확실히 나쁩니다. 문제가 되는 부분은 증명이 아니라 데이터인 smul 필드이며, 정의상 같지 않은 두 가지 구성이 존재합니다. 이 문제를 견고하게 해결하는 방법은 풍부한 구조에서 빈약한 구조로 가는 과정이 항상 데이터를 정의하는 방식이 아니라 데이터를 잊는 방식으로 이루어지도록 하는 것입니다. 이 잘 알려진 패턴은 “망각 상속(forgetful inheritance)”이라는 이름으로 불리며, https://inria.hal.science/hal-02463336v2 에서 폭넓게 논의되었습니다.

이 구체적인 경우에는 AddMonoid₃의 정의를 수정하여 nsmul 데이터 필드와, 이 연산이 위에서 구성한 연산과 같음을 증명할 수 있도록 보장하는 몇 가지 Prop 값 필드를 포함시킬 수 있습니다. 아래 정의에서는 이 필드들의 타입 뒤에 :=를 사용하여 기본값을 지정합니다. 이 기본값 덕분에 대부분의 인스턴스는 이전 정의에서와 똑같이 구성됩니다. 하지만 ℤ라는 특수한 경우에는 특정한 값을 제공할 수 있습니다.

class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M where
  /-- Multiplication by a natural number. -/
  nsmul : ℕ → M → M := nsmul₁
  /-- Multiplication by `(0 : ℕ)` gives `0`. -/
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
  nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl

instance mySMul {M : Type} [AddMonoid₄ M] : SMul ℕ M := ⟨AddMonoid₄.nsmul⟩

nsmul 관련 필드를 제공하지 않고도 여전히 곱 모노이드 인스턴스를 구성할 수 있는지 확인해 봅시다.

instance (M N : Type) [AddMonoid₄ M] [AddMonoid₄ N] : AddMonoid₄ (M × N) where
  add := fun p q ↦ (p.1 + q.1, p.2 + q.2)
  add_assoc₃ := fun a b c ↦ by ext <;> apply add_assoc₃
  zero := (0, 0)
  zero_add := fun a ↦ by ext <;> apply zero_add
  add_zero := fun a ↦ by ext <;> apply add_zero

이제 ℤ라는 특수한 경우를 다루어 봅시다. 여기서는 ℕ에서 ℤ로의 강제 변환과 ℤ 위의 곱셈을 사용하여 nsmul을 만들고자 합니다. 특히 증명 필드에 위의 기본값에서보다 더 많은 작업이 들어간다는 점에 주목하십시오.

instance : AddMonoid₄ ℤ where
  add := (· + ·)
  add_assoc₃ := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  nsmul := fun n m ↦ (n : ℤ) * m
  nsmul_zero := Int.zero_mul
  nsmul_succ := fun n m ↦ show (n + 1 : ℤ) * m = m + n * m
    by rw [Int.add_mul, Int.add_comm, Int.one_mul]

문제를 해결했는지 확인해 봅시다. Lean에는 이미 자연수와 정수의 스칼라 곱셈에 대한 정의가 있고 우리는 우리가 만든 인스턴스가 확실히 사용되도록 하고 싶으므로, • 표기법을 사용하지 않고 SMul.mul을 호출하면서 위에서 정의한 인스턴스를 명시적으로 제공하겠습니다.

example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl

이야기는 이어서 군의 정의에 zsmul 필드를 포함시키는 것과 이와 비슷한 기법들로 계속됩니다. 이제 Mathlib에 있는 모노이드, 군, 환, 가군의 정의를 읽을 준비가 되었습니다. 이 정의들은 거대한 계층 구조의 일부이기 때문에 여기서 본 것보다 더 복잡하지만, 모든 원리는 위에서 설명했습니다.

연습 삼아 위에서 만든 순서 관계 계층으로 돌아가, 미만 표기법 <₁을 담은 타입 클래스 LT₁을 추가해 보십시오. 그리고 모든 준순서에 ≤₁로부터 만든 기본값을 갖는 <₁와, 이 두 비교 연산자 사이의 자연스러운 관계를 명시하는 Prop 값 필드가 함께 제공되도록 하십시오.

8.2. 사상

이 장에서는 지금까지 수학적 구조의 계층을 만드는 방법을 살펴보았습니다. 하지만 사상을 갖추기 전까지는 구조를 정의하는 일이 온전히 끝났다고 할 수 없습니다. 여기에는 크게 두 가지 접근 방식이 있습니다. 가장 먼저 떠오르는 방법은 함수에 대한 술어를 정의하는 것입니다.

def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop :=
  f 1 = 1 ∧ ∀ g g', f (g * g') = f g * f g'

이 정의에서는 논리곱(conjunction)을 사용하는 점이 조금 불편합니다. 특히 사용자는 두 조건에 접근하려고 할 때 우리가 정한 순서를 기억해야 합니다. 그래서 대신 구조체를 사용할 수 있습니다.

structure isMonoidHom₂ [Monoid G] [Monoid H] (f : G → H) : Prop where
  map_one : f 1 = 1
  map_mul : ∀ g g', f (g * g') = f g * f g'

여기까지 오면, 이것을 클래스로 만들고 타입 클래스 인스턴스 해결 절차를 사용하여 더 단순한 함수에 대한 인스턴스로부터 복잡한 함수에 대한 isMonoidHom₂를 자동으로 추론하고 싶은 유혹마저 듭니다. 예를 들어 모노이드 준동형사상의 합성은 모노이드 준동형사상이며, 이는 유용한 인스턴스처럼 보입니다. 그러나 이러한 인스턴스는 모든 곳에서 g ∘ f를 찾아내야 하므로 해소 절차에 매우 까다로울 것입니다. 이 인스턴스가 g (f x)에서 실패하는 것을 보면 매우 답답할 것입니다. 더 일반적으로, 주어진 표현식에서 어떤 함수가 적용되었는지 알아내는 것은 “고차 단일화 문제(higher-order unification problem)”라고 불리는 매우 어려운 문제라는 점을 항상 염두에 두어야 합니다. 그래서 Mathlib은 이러한 클래스 접근 방식을 사용하지 않습니다.

더 근본적인 질문은 위와 같이 (def나 structure를 사용하여) 술어를 사용할 것인지, 아니면 함수와 술어를 한데 묶은 구조체를 사용할 것인지입니다. 이는 어느 정도 심리적인 문제입니다. 모노이드 사이의 함수 중에서 준동형사상이 아닌 것을 다루는 경우는 극히 드뭅니다. “모노이드 준동형사상”은 그냥 함수에 붙일 수 있는 형용사가 아니라 명사라는 느낌이 강하게 듭니다. 반면 위상 공간 사이의 연속 함수는 실제로는 마침 연속인 함수일 뿐이라고 주장할 수도 있습니다. 이것이 Mathlib에 Continuous 술어가 있는 이유 중 하나입니다. 예를 들어 다음과 같이 쓸 수 있습니다.

example : Continuous (id : ℝ → ℝ) := continuous_id

연속 함수를 묶은 구조도 여전히 있으며, 이는 예를 들어 연속 함수들의 공간에 위상을 부여할 때 편리하지만, 연속성을 다루는 주된 도구는 아닙니다.

이와 대조적으로 모노이드(또는 다른 대수적 구조) 사이의 준동형사상은 다음과 같이 묶여 있습니다.

@[ext]
structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H]  where
  toFun : G → H
  map_one : toFun 1 = 1
  map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

물론 toFun을 모든 곳에 입력하고 싶지는 않으므로 CoeFun 타입 클래스를 사용하여 강제 변환을 등록합니다. 첫 번째 인자는 함수로 강제 변환하려는 타입입니다. 두 번째 인자는 대상 함수 타입을 기술합니다. 우리의 경우 이는 모든 f : MonoidHom₁ G H에 대해 항상 G → H입니다. 또한 MonoidHom₁.toFun에 coe 속성을 붙여서 택틱 상태에서 단지 ↑ 접두사로만 거의 보이지 않게 표시되도록 합니다.

instance [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := MonoidHom₁.toFun

attribute [coe] MonoidHom₁.toFun

묶음 모노이드 준동형사상을 원소에 실제로 적용할 수 있는지 확인해 봅시다.

example [Monoid G] [Monoid H] (f : MonoidHom₁ G H) : f 1 = 1 :=  f.map_one

환 사상에 이를 때까지 다른 종류의 사상에 대해서도 같은 작업을 할 수 있습니다.

@[ext]
structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H]  where
  toFun : G → H
  map_zero : toFun 0 = 0
  map_add : ∀ g g', toFun (g + g') = toFun g + toFun g'

instance [AddMonoid G] [AddMonoid H] : CoeFun (AddMonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := AddMonoidHom₁.toFun

attribute [coe] AddMonoidHom₁.toFun

@[ext]
structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S

이 접근 방식에는 몇 가지 문제가 있습니다. 사소한 문제는 RingHom₁.toFun이 존재하지 않아서 coe 속성을 어디에 붙여야 할지 분명하지 않다는 점입니다. 관련 함수는 MonoidHom₁.toFun ∘ RingHom₁.toMonoidHom₁인데, 이는 속성을 붙일 수 있는 선언이 아닙니다(그래도 CoeFun  (RingHom₁ R S) (fun _ ↦ R → S) 인스턴스는 정의할 수 있습니다). 훨씬 더 중요한 문제는 모노이드 준동형사상에 대한 보조정리가 환 사상에 바로 적용되지 않는다는 점입니다. 그러면 모노이드 준동형사상에 대한 보조정리를 적용하려 할 때마다 RingHom₁.toMonoidHom₁를 이리저리 다루거나, 그러한 보조정리를 모두 환 사상에 대해 다시 진술하는 선택지만 남습니다. 어느 쪽도 매력적이지 않으므로 Mathlib은 여기서 새로운 계층 구조 기법을 사용합니다. 아이디어는 적어도 모노이드 준동형사상인 대상들을 위한 타입 클래스를 정의하고, 모노이드 준동형사상과 환 사상 모두로 그 클래스의 인스턴스를 만든 다음, 이를 사용하여 모든 보조정리를 진술하는 것입니다. 아래 정의에서 F는 MonoidHom₁ M N일 수도 있고, M과 N이 환 구조를 가진다면 RingHom₁ M N일 수도 있습니다.

class MonoidHomClass₁ (F : Type) (M N : Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

그러나 위 구현에는 문제가 있습니다. 아직 함수로의 강제 변환 인스턴스를 등록하지 않았습니다. 이제 이를 시도해 봅시다(여기서 무언가 위험하다고 알려 주는 Lean의 경고는 무시합니다. 실제로 좋지 않은 일을 하고 있다는 것을 알고 있기 때문입니다).

def badInst [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₁.toFun

이것을 인스턴스로 만드는 것은 좋지 않습니다. f의 타입이 함수 타입이 아닌데 f x 같은 표현을 만나면, Lean은 f를 함수로 강제 변환하기 위해 CoeFun 인스턴스를 찾으려고 시도합니다. 위 함수의 타입은 {M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N)이므로, Lean이 이를 적용하려고 할 때 미지의 타입 M, N, F를 어떤 순서로 추론해야 하는지 사전에 분명하지 않습니다. 이것은 앞에서 이미 본 것과는 조금 다른 종류의 나쁜 인스턴스이지만, 결국 같은 문제로 귀결됩니다. M을 모르는 상태에서 Lean은 미지의 타입에 대한 모노이드 인스턴스를 찾아야 하므로, 데이터베이스에 있는 모든 모노이드 인스턴스를 가망 없이 시도하게 됩니다. 이러한 인스턴스가 어떤 영향을 미치는지 궁금하다면, 위 선언 앞에 set_option synthInstance.checkSynthOrder false in을 입력하고 def badInst를 instance로 바꾼 다음, 이 파일에서 무작위로 발생하는 실패를 살펴보십시오.

여기서 해결책은 간단합니다. Lean에게 먼저 F가 무엇인지 찾은 다음 M과 N을 추론하라고 알려 주면 됩니다. 이는 outParam 함수를 사용하여 할 수 있습니다. 이 함수는 항등 함수로 정의되어 있지만, 타입 클래스 메커니즘은 여전히 이를 인식하여 원하는 동작을 일으킵니다. 따라서 outParam 함수에 주의하면서 클래스를 다시 정의해 볼 수 있습니다:

class MonoidHomClass₂ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

instance [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₂.toFun

attribute [coe] MonoidHomClass₂.toFun

이제 이 클래스의 인스턴스를 만드는 계획을 진행할 수 있습니다.

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N where
  toFun := MonoidHom₁.toFun
  map_one := fun f ↦ f.map_one
  map_mul := fun f ↦ f.map_mul

instance (R S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S where
  toFun := fun f ↦ f.toMonoidHom₁.toFun
  map_one := fun f ↦ f.toMonoidHom₁.map_one
  map_mul := fun f ↦ f.toMonoidHom₁.map_mul

약속한 대로, MonoidHomClass₁ F의 인스턴스를 가정하고 f : F에 대해 증명하는 모든 보조정리는 모노이드 준동형사상과 환 사상 모두에 적용됩니다. 보조정리 예시를 하나 살펴보고 두 경우 모두에 적용되는지 확인해 봅시다.

lemma map_inv_of_inv [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] (f : F) {m m' : M} (h : m*m' = 1) :
    f m * f m' = 1 := by
  rw [← MonoidHomClass₂.map_mul, h, MonoidHomClass₂.map_one]

example [Monoid M] [Monoid N] (f : MonoidHom₁ M N) {m m' : M} (h : m*m' = 1) : f m * f m' = 1 :=
map_inv_of_inv f h

example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r*r' = 1) : f r * f r' = 1 :=
map_inv_of_inv f h

언뜻 보면 MonoidHom₁을 클래스로 만들었던 예전의 나쁜 발상으로 되돌아간 것처럼 보일 수 있습니다. 하지만 그렇지 않습니다. 모든 것이 추상화 수준 한 단계 위로 옮겨졌습니다. 타입 클래스 해소 절차는 함수를 찾는 것이 아니라 MonoidHom₁ 또는 RingHom₁을 찾게 됩니다.

우리 접근 방식에 남아 있는 한 가지 문제는 toFun 필드와 이에 대응하는 CoeFun 인스턴스 및 coe 속성 주변에 반복적인 코드가 존재한다는 점입니다. 또한 이 패턴이 추가 성질을 가진 함수에만 사용된다는 사실, 즉 함수로의 강제 변환이 단사여야 한다는 사실을 기록해 두는 편이 더 좋을 것입니다. 그래서 Mathlib은 기반 클래스 DFunLike로 추상화 계층을 하나 더 추가합니다(여기서 “DFun”은 의존 함수(dependent function)를 뜻합니다). 이 기반 계층 위에 MonoidHomClass를 다시 정의해 봅시다.

class MonoidHomClass₃ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] extends
    DFunLike F M (fun _ ↦ N) where
  map_one : ∀ f : F, f 1 = 1
  map_mul : ∀ (f : F) g g', f (g * g') = f g * f g'

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₃ (MonoidHom₁ M N) M N where
  coe := MonoidHom₁.toFun
  coe_injective _ _ := MonoidHom₁.ext
  map_one := MonoidHom₁.map_one
  map_mul := MonoidHom₁.map_mul

물론 사상의 계층 구조는 여기서 끝나지 않습니다. 계속해서 MonoidHomClass₃을 확장하는 클래스 RingHomClass₃을 정의하고, 이를 RingHom에 대해, 그리고 나중에는 AlgebraHom에 대해 인스턴스화할 수도 있습니다(대수는 추가 구조를 가진 환입니다). 하지만 Mathlib에서 사상에 사용되는 주요 형식화 아이디어는 다루었으므로, 이제 Mathlib에서 사상이 어떻게 정의되는지 이해할 준비가 되었을 것입니다.

연습 문제로, 순서가 주어진 타입 사이의 순서를 보존하는 묶인 함수의 클래스를 정의하고, 이어서 순서를 보존하는 모노이드 준동형사상의 클래스를 정의해 보십시오. 이는 순전히 연습을 위한 것입니다. 연속 함수와 마찬가지로 순서 보존 함수도 Mathlib에서는 주로 묶이지 않은(unbundled) 형태로 다루어지며, Monotone 술어로 정의됩니다. 물론 아래의 클래스 정의를 완성해야 합니다.

@[ext]
structure OrderPresHom (α β : Type) [LE α] [LE β] where
  toFun : α → β
  le_of_le : ∀ a a', a ≤ a' → toFun a ≤ toFun a'

@[ext]
structure OrderPresMonoidHom (M N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends
MonoidHom₁ M N, OrderPresHom M N

class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β]

instance (α β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    OrderPresHomClass (OrderPresMonoidHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    MonoidHomClass₃ (OrderPresMonoidHom α β) α β
  := sorry

8.3. 부분 대상

어떤 대수적 구조와 그 사상을 정의했다면, 다음 단계는 이 대수적 구조를 물려받는 집합, 예를 들어 부분군이나 부분환을 살펴보는 것입니다. 이는 앞서 다룬 주제와 상당 부분 겹칩니다. 실제로 X의 집합은 X에서 Prop으로 가는 함수로 구현되므로, 부분 대상은 특정 술어를 만족하는 함수입니다. 따라서 DFunLike 클래스와 그 하위 클래스들을 만들 때 쓴 아이디어의 상당 부분을 재사용할 수 있습니다. 하지만 DFunLike 자체는 재사용하지 않습니다. 그렇게 하면 Set X에서 X → Prop으로 가는 추상화 경계가 깨지기 때문입니다. 대신 SetLike 클래스가 있습니다. 이 클래스는 함수 타입으로 가는 단사 함수를 감싸는 대신 Set 타입으로 가는 단사 함수를 감싸고, 그에 대응하는 강제 변환과 Membership 인스턴스를 정의합니다.

@[ext]
structure Submonoid₁ (M : Type) [Monoid M] where
  /-- The carrier of a submonoid. -/
  carrier : Set M
  /-- The product of two elements of a submonoid belongs to the submonoid. -/
  mul_mem {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
  /-- The unit element belongs to the submonoid. -/
  one_mem : 1 ∈ carrier

/-- Submonoids in `M` can be seen as sets in `M`. -/
instance [Monoid M] : SetLike (Submonoid₁ M) M where
  coe := Submonoid₁.carrier
  coe_injective _ _ := Submonoid₁.ext

위의 SetLike 인스턴스를 갖추면, N.carrier를 사용하지 않고도 부분 모노이드 N이 1을 포함한다는 것을 이미 자연스럽게 서술할 수 있습니다. 또한 N을 암묵적으로 M 안의 집합으로 다루고, 어떤 사상에 의한 그 직상을 취할 수도 있습니다.

example [Monoid M] (N : Submonoid₁ M) : 1 ∈ N := N.one_mem

example [Monoid M] (N : Submonoid₁ M) (α : Type) (f : M → α) := f '' N

또한 Subtype을 사용하는 Type으로의 강제 변환도 있으므로, 부분 모노이드 N이 주어지면 N에 속하는 M의 원소로 강제 변환될 수 있는 매개변수 (x : N)을 쓸 수 있습니다.

example [Monoid M] (N : Submonoid₁ M) (x : N) : (x : M) ∈ N := x.property

이 Type으로의 강제 변환을 사용하면 부분 모노이드에 모노이드 구조를 부여하는 작업도 다룰 수 있습니다. 위에서와 같이 N에 연관된 타입으로부터의 강제 변환과, 이 강제 변환이 단사임을 나타내는 보조정리 SetCoe.ext를 사용하겠습니다. 둘 다 SetLike 인스턴스가 제공합니다.

instance SubMonoid₁Monoid [Monoid M] (N : Submonoid₁ M) : Monoid N where
  mul := fun x y ↦ ⟨x*y, N.mul_mem x.property y.property⟩
  mul_assoc := fun x y z ↦ SetCoe.ext (mul_assoc (x : M) y z)
  one := ⟨1, N.one_mem⟩
  one_mul := fun x ↦ SetCoe.ext (one_mul (x : M))
  mul_one := fun x ↦ SetCoe.ext (mul_one (x : M))

위 인스턴스에서 M으로의 강제 변환을 사용하고 property 필드를 호출하는 대신, 다음과 같이 구조 분해 바인더를 사용할 수도 있었다는 점에 유의하십시오.

example [Monoid M] (N : Submonoid₁ M) : Monoid N where
  mul := fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x*y, N.mul_mem hx hy⟩
  mul_assoc := fun ⟨x, _⟩ ⟨y, _⟩ ⟨z, _⟩ ↦ SetCoe.ext (mul_assoc x y z)
  one := ⟨1, N.one_mem⟩
  one_mul := fun ⟨x, _⟩ ↦ SetCoe.ext (one_mul x)
  mul_one := fun ⟨x, _⟩ ↦ SetCoe.ext (mul_one x)

부분 모노이드에 관한 보조정리를 부분군이나 부분환에 적용하려면, 사상의 경우와 마찬가지로 클래스가 필요합니다. 이 클래스는 SetLike 인스턴스를 매개변수로 받으므로 바탕 집합 필드가 필요 없고, 필드 안에서 멤버십 표기를 사용할 수 있다는 점에 유의하십시오.

class SubmonoidClass₁ (S : Type) (M : Type) [Monoid M] [SetLike S M] : Prop where
  mul_mem : ∀ (s : S) {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
  one_mem : ∀ s : S, 1 ∈ s

instance [Monoid M] : SubmonoidClass₁ (Submonoid₁ M) M where
  mul_mem := Submonoid₁.mul_mem
  one_mem := Submonoid₁.one_mem

연습 문제로 Subgroup₁ 구조체를 정의하고, 여기에 SetLike 인스턴스와 SubmonoidClass₁ 인스턴스를 부여하고, Subgroup₁에 연관된 부분타입에 Group 인스턴스를 넣은 다음, SubgroupClass₁ 클래스를 정의해 보십시오.

Mathlib에서 주어진 대수적 대상의 부분 대상들에 관해 알아두어야 할 또 다른 매우 중요한 점은 이들이 항상 완비 격자를 이룬다는 것이며, 이 구조는 매우 많이 사용됩니다. 예를 들어 부분 모노이드들의 교집합이 부분 모노이드라는 보조정리를 찾아볼 수도 있습니다. 하지만 이것은 보조정리가 아니라 하한(infimum) 구성이 됩니다. 두 부분 모노이드의 경우를 해 봅시다.

instance [Monoid M] : Min (Submonoid₁ M) :=
  ⟨fun S₁ S₂ ↦
    { carrier := S₁ ∩ S₂
      one_mem := ⟨S₁.one_mem, S₂.one_mem⟩
      mul_mem := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ ↦ ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

이를 통해 두 부분 모노이드의 교집합을 부분 모노이드로 얻을 수 있습니다.

example [Monoid M] (N P : Submonoid₁ M) : Submonoid₁ M := N ⊓ P

위 예제에서 교집합 기호 ∩ 대신 하한 기호 ⊓를 사용해야 했던 것이 아쉽다고 생각할 수도 있습니다. 하지만 상한(supremum)을 생각해 보십시오. 두 부분 모노이드의 합집합은 부분 모노이드가 아닙니다. 그러나 부분 모노이드는 여전히 격자(심지어 완비 격자)를 이룹니다. 사실 N ⊔ P는 N과 P의 합집합으로 생성된 부분 모노이드이며, 이를 N ∪ P로 표기한다면 당연히 매우 혼란스러울 것입니다. 따라서 N ⊓ P를 사용하는 것이 훨씬 더 일관적이라고 볼 수 있습니다. 이는 여러 종류의 대수적 구조 전반에 걸쳐서도 훨씬 더 일관적입니다. 두 벡터 부분공간 E와 F의 합이 E + F 대신 E ⊔ F로 표기된 것을 처음 보면 조금 이상해 보일 수 있습니다. 하지만 곧 익숙해질 것입니다. 그리고 머지않아 E + F 표기법은 E ⊔ F가 E와 F를 모두 포함하는 가장 작은 벡터 부분공간이라는 근본적인 사실 대신 E ⊔ F의 원소를 E의 원소와 F의 원소의 합으로 쓸 수 있다는 부수적인 사실을 강조하여 주의를 흐트러뜨리는 표기라고 여기게 될 것입니다.

이 장의 마지막 주제는 몫입니다. 이번에도 Mathlib에서 편리한 표기법을 어떻게 만들고 코드 중복을 어떻게 피하는지 설명하고자 합니다. 여기서 핵심 장치는 M ⧸ N과 같은 표기법을 가능하게 하는 HasQuotient 클래스입니다. 몫 기호 ⧸는 일반 ASCII 나눗셈 기호가 아니라 특수한 유니코드 문자라는 점에 주의하십시오.

예시로 가환 모노이드를 부분 모노이드로 나눈 몫을 만들어 보겠으며, 증명은 여러분께 맡기겠습니다. 마지막 예시에서는 Setoid.refl을 사용할 수 있지만, 관련된 Setoid 구조를 자동으로 찾아내지는 못합니다. @Setoid.refl M N.Setoid처럼 @ 구문을 사용하여 모든 인자를 제공하면 이 문제를 해결할 수 있습니다.

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where
  r := fun x y ↦ ∃ w ∈ N, ∃ z ∈ N, x*w = y*z
  iseqv := {
    refl := fun x ↦ ⟨1, N.one_mem, 1, N.one_mem, rfl⟩
    symm := fun ⟨w, hw, z, hz, h⟩ ↦ ⟨z, hz, w, hw, h.symm⟩
    trans := by
      sorry
  }

instance [CommMonoid M] : HasQuotient M (Submonoid M) where
  Quotient := fun N ↦ Quotient N.Setoid

def QuotientMonoid.mk [CommMonoid M] (N : Submonoid M) : M → M ⧸ N := Quotient.mk N.Setoid

instance [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N) where
  mul := Quotient.map₂ (· * ·) (by
      sorry
        )
  mul_assoc := by
      sorry
  one := QuotientMonoid.mk N 1
  one_mul := by
      sorry
  mul_one := by
      sorry