선택 심화: 초기성이 구조적 귀납을 돌려준다🔗

Depth/Algebra.lean의 초기성(IntExp.initial)은 "항 대수가 모든 대수로 유일한 준동형을 갖는다"는 명제였고, 그 유일성은 구조적 귀납법으로 증명했다. 반대 방향도 성립한다 — 초기성 하나만 있으면 구조적 귀납 원리를 되찾을 수 있다.

다음 연습은 그 반대 방향을 일반 정리로 적은 것이다. 특정 대수가 실제로 초기라는 사실은 쓰지 않는다. 대신 "어떤 IntExp V가 초기 대수라면"이라는 가설 hinit에서 결론을 끌어낸다.

@[exercise "심화 A1.5" 3]
theorem IntExp.induction_of_initial {V : Type u}
    (hinit : ∀ A : IntExpAlg.{u, u} V, ∃! h : IntExp V → A.Carrier, IsHom A h)
    (P : IntExp V → Prop)
    (hnum : ∀ n, P (.num n)) (hvar : ∀ v, P (.var v))
    (hneg : ∀ e, P e → P (.neg e))
    (hbin : ∀ op e₀ e₁, P e₀ → P e₁ → P (.bin op e₀ e₁)) :
    ∀ e, P e := byV:Type uhinit:∀ (A : IntExpAlg V), ∃! h, IsHom A hP:IntExp V → Prophnum:∀ (n : ℤ), P (num n)hvar:∀ (v : V), P (var v)hneg:∀ (e : IntExp V), P e → P e.neghbin:∀ (op : IntOp) (e₀ e₁ : IntExp V), P e₀ → P e₁ → P (bin op e₀ e₁)⊢ ∀ (e : IntExp V), P e

증명의 뼈대는 부분 대수 논법(sub-algebra argument)이다. P에 닫힌 부분집합 {x // P x}를 대수로 만들면, 포함 사상 Subtype.val은 그 부분 대수에서 항 대수로 가는 준동형이다. hinit으로 얻은 유일한 사상을 그 포함 사상과 합성하면 항 대수의 자기 자신으로 가는 준동형이 되는데, id도 그런 준동형이고 hinit을 항 대수 자신에 적용하면 그런 준동형이 하나뿐이라고 말해 준다. 그래서 둘이 같고, 그 등식이 바로 "모든 e에서 P e"가 된다.

이 정리는 IntExp.initial(심화 A1.1)을 전혀 몰라도 성립한다. 반대로 IntExp.initial을 hinit에 넣으면 §5의 유일성 증명 없이도 구조적 귀납 원리를 얻는다 — 다만 그 결합을 따로 적지는 않는다. 독자가 "이 연습이 A1.1에 기대는 건가?"라고 헷갈리기 쉬워서다. induction e with … 태틱이 이미 공짜로 주는 것과 같은 결론이지만, 증명 방법이 다르다는 것이 요점이다 — 케이스 분석 없이 보편 성질 하나로 모든 생성자 조건을 동시에 처리한다.