선택 심화: 같은 초기성을 Mathlib으로 읽기🔗

두 정렬 초기성의 ∃!를 이해했다면, 범주론에서 말하는 초기 대상도 읽을 수 있다. 범주(category)는 대상과 대상 사이의 사상, 그리고 사상을 이어 붙이는 합성을 갖춘다. 여기서 대상은 LogicAlg, 사상은 연산을 보존하는 함수 쌍이다. 초기성 정리에서는 사상의 출발점이 늘 구문이었지만, 이제 출발점도 임의의 대수로 둔다.

예를 들어 f : L ⟶ M은 정수 식 반송자의 함수 f.e와 단언 반송자의 함수 f.a를 갖는다. 비교 연산의 보존 조건은 f.a (L.cmp c x y) = M.cmp c (f.e x) (f.e y)다. 입력 둘은 정수 식 성분으로, 결과는 단언 성분으로 옮긴다. 양화사에서는 종류와 변수 이름을 그대로 두고 본문에만 f.a를 적용한다.

항등 사상은 두 반송자의 항등 함수 쌍이다. f ≫ g는 먼저 f, 다음에 g를 적용하므로 정수 식 성분은 g.e ∘ f.e, 단언 성분은 g.a ∘ f.a가 된다. 함수 합성의 항등 법칙과 결합 법칙으로 아래 범주 법칙을 증명한다.

/-- 고정된 우주의 대수와 준동형으로 이루어진 범주. 법칙은 함수 합성의 법칙이다. -/
instance category : Category (LogicAlg.{u, u} V) where
  Hom := Hom
  id := Hom.id
  comp := Hom.comp
  id_comp _ := Hom.ext rfl rfl
  comp_id _ := Hom.ext rfl rfl
  assoc _ _ _ := Hom.ext rfl rfl

여기서는 변수 타입과 두 반송자를 모두 같은 Type u에 둔다. 따라서 서로 다른 우주의 목표 대수도 허용했던 LogicAlg.initial을 이 범주의 대상들에 한정해서 사용한다. syntaxAlg V는 정수 식과 단언 자체를 반송자로 갖는 대수다.

/-- 기존 `LogicAlg.initial`을 적용하면 구문 대수가 이 범주의 초기 대상이 된다. -/
noncomputable def syntaxIsInitial (V : Type u) : IsInitial (syntaxAlg V) :=
  isInitialOfUniqueHom (fun L ↦ L.initial)

IsInitial (syntaxAlg V)는 각 목표로 가는 사상을 고르는 자료와 그 유일성 증명을 포함한다. 그 자료가 주어지면 h.to L로 사상을 얻고, h.hom_ext로 두 사상의 등식을 얻는다. 다음 연습은 이 두 API를 LogicAlg.IsHom의 함수 쌍 언어로 옮기는 문제다. 초기성을 가설로 주므로 A1.3을 아직 풀지 않았어도 시작할 수 있다.

@[exercise "심화 C1.1" 2]
theorem uniqueHom_of_isInitial (h : IsInitial (syntaxAlg V)) (L : LogicAlg.{u, u} V) :
    ∃! f : (IntExp V → L.E) × (Assert V → L.A), L.IsHom f := byV:Type uh:IsInitial (syntaxAlg V)L:LogicAlg V⊢ ∃! f, L.IsHom f

힌트: Hom.pair와 Hom.isHom으로 함수 쌍과 보존 조건을 꺼낸다. 유일성을 보일 때는 다른 함수 쌍을 Hom.ofIsHom으로 사상에 묶은 다음 비교한다. isInitial_iff_uniqueHom은 두 방향을 한 명제로 모은다. 왼쪽의 Nonempty는 IsInitial 자료가 있다는 것을 명제로 표현한다.

이 선택 심화는 이름을 그대로 보존하는 원시 구문의 범주에 머문다. α-동치로 나눈 구문의 초기성, 치환의 법칙, 일반 함자의 대수에 대한 Lambek 정리는 선택 후속 주제다. 본문의 1장 학습은 이 파일 없이도 이어갈 수 있다.