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 대신 @[class] structure를 작성하는 것, 즉 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₁ α는 인스턴스 암묵적으로 표시되어 있는데, 이는 이 선언의 사용에만 영향을 미치고 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 : α)

0 < 1이 자연수에 대한 부등식인지 실수에 대한 부등식인지 Lean에 알려주지 않은 채로 이를 서술하려 한 적이 있다면, 제 3.6 절에서 수열의 극한을 다룰 때 이미 이 문제를 겪어보았을 수 있습니다.

다음 과제는 One₁.one에 표기법을 지정하는 것입니다. 1에 대한 내장 표기법과 충돌하는 것을 원하지 않으므로, 𝟙을 사용하겠습니다. 이는 다음 명령으로 이루어지며, 첫 번째 줄은 Lean에게 One₁.one의 문서를 기호 𝟙의 문서로 사용하도록 지시합니다.

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

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

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

이제 이항 연산을 기록하는 데이터를 담은 클래스를 원합니다. 지금은 덧셈과 곱셈 중 하나를 선택하고 싶지 않으므로 다이아몬드(diamond)를 사용하겠습니다.

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)

이제 다이아몬드 연산과, 이 원소가 양쪽에서 중립임을 말하는 공리를 갖춘 특별한 원소 하나를 결합해 봅시다.

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

다음 예제에서는 Lean에게 α가 DiaOneClass₁ 구조를 가진다고 알려주고, Dia₁ 인스턴스와 One₁ 인스턴스를 모두 사용하는 성질을 서술합니다. Lean이 그 인스턴스들을 어떻게 찾는지 확인하기 위해, 결과를 Infoview에서 볼 수 있는 추적(tracing) 옵션을 설정합니다. 이 결과는 기본적으로 다소 간략하지만, 검은 화살표로 끝나는 줄을 클릭하면 펼칠 수 있습니다. 여기에는 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로 연결됩니다. 반군의 경우처럼 다중 상속이 있는 경우, 자동 생성된 “대칭 복원” 인스턴스에도 표시가 필요합니다. 이는 다소 기술적인 내용이므로, 세부 사항까지 이해할 필요는 없습니다. 중요한 점은 보조정리가 이제 곱셈 표기법 left_inv_eq_right_inv'로만 서술되고 어트리뷰트 to_additive로 표시되어, 자동 생성된 덧셈 버전인 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

두 번째 예시로, 모든 아벨군은 ℤ에 대한 가군입니다(이것이 벡터 공간 이론을 가역이지 않은 스칼라를 허용하도록 일반화하는 이유 중 하나입니다). 먼저 영과 덧셈을 갖춘 임의의 타입에 대해 자연수에 의한 스칼라 곱셈을 정의할 수 있습니다: 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. 사상(Morphisms)

이 장에서 지금까지 수학적 구조의 계층을 만드는 방법에 대해 논의했습니다. 그러나 구조를 정의하는 작업은 사상이 있어야 비로소 완성됩니다. 여기에는 두 가지 주요 접근 방식이 있습니다. 가장 명백한 방법은 함수에 대한 술어를 정의하는 것입니다.

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) 타입을 가지므로, 이를 적용하려 할 때 미지의 타입 M, N, F를 어떤 순서로 추론해야 할지 Lean에게 선험적으로 명확하지 않습니다. 이는 이미 살펴본 것과는 조금 다른 종류의 나쁜 인스턴스이지만, 결국 같은 문제로 귀결됩니다. 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에서 주로 묶이지 않은 형태로 다루어지며, 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이 주어지면 매개변수 (x : N)을 쓸 수 있고, 이는 N에 속하는 M의 원소로 강제 변환될 수 있습니다.

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 인스턴스를 받으므로 carrier 필드가 필요 없고, 필드에서 소속 표기법을 사용할 수 있다는 점에 유의하십시오.

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에서 주어진 대수적 대상의 부분 대상들이 항상 완비 격자를 이룬다는 것을 아는 것도 매우 중요하며, 이 구조는 많이 사용됩니다. 예를 들어, 부분모노이드들의 교집합이 부분모노이드라는 보조정리를 찾아볼 수 있습니다. 하지만 이것은 보조정리가 아니라 하한 구성이 될 것입니다. 두 부분모노이드의 경우를 살펴봅시다.

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

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

이 장의 마지막 주제는 몫(quotient)에 관한 것입니다. 다시 한번, 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