선택 심화: 초기성이 Lambek 보조정리를 돌려준다🔗

Depth/SignatureFunctor.lean의 IntExp.lambek은 cases로 끝난다. inductive가 이미 만들어 둔 roll/unroll을 확인할 뿐이지, 초기 대수의 구조 사상이 왜 항상 동형인지는 아직 보이지 않는다. 다음 정리가 그 이유다 — 특정 구문을 전혀 쓰지 않고 "초기 Sig V-대수의 구조 사상은 동형이다"를 추상적으로 보인다.

def IsSigHom {V : Type u} {C D : Type v} (s : Sig V C → C) (t : Sig V D → D) (h : C → D) :
    Prop :=
  ∀ x, h (s x) = t (Sig.map h x)

h가 "자식에 h를 입힌 뒤 구조 사상을 적용한 것"과 "h를 적용한 뒤 구조 사상을 적용한 것"을 같게 만든다는 한 줄이다. Depth/Algebra.lean의 IsHom은 이 조건을 IntExpAlg의 생성자별 필드로 풀어 쓴 것과 같다.

theorem isIso_of_initial {V : Type u} {C : Type u} (s : Sig V C → C)
    (hinit : ∀ {D : Type u} (t : Sig V D → D), ∃! h : C → D, IsSigHom s t h) :
    Function.Bijective s := byV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t h⊢ Function.Bijective s
  obtain ⟨φ, hφ, _⟩ := hinit (Sig.map s)V:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φ⊢ Function.Bijective s
  have hψ : IsSigHom s s (s ∘ φ) := by
    intro xV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φx:Sig V C⊢ (s ∘ φ) (s x) = s (Sig.map (s ∘ φ) x)
    change s (φ (s x)) = s (Sig.map (s ∘ φ) x)V:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φx:Sig V C⊢ s (φ (s x)) = s (Sig.map (s ∘ φ) x)
    rw [hφ x,V:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φx:Sig V C⊢ s (Sig.map s (Sig.map φ x)) = s (Sig.map (s ∘ φ) x) Sig.map_compV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φx:Sig V C⊢ s (Sig.map (s ∘ φ) x) = s (Sig.map (s ∘ φ) x)]V:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)⊢ Function.Bijective s
  obtain ⟨_, _, huniq⟩ := hinit sV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝⊢ Function.Bijective s
  have hidHom : IsSigHom s s (id : C → C) := fun x => byV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝x:Sig V C⊢ id (s x) = s (Sig.map id x) rw [Sig.map_idV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝x:Sig V C⊢ id (s x) = s x]V:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝x:Sig V C⊢ id (s x) = s x; rflV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s id⊢ Function.Bijective s
  have hcomp : s ∘ φ = id := (huniq _ hψ).trans (huniq id hidHom).symmV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s idhcomp:s ∘ φ = id⊢ Function.Bijective s
  have hleft : φ ∘ s = id := by
    funext xV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s idhcomp:s ∘ φ = idx:Sig V C⊢ (φ ∘ s) x = id x
    change φ (s x) = xV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s idhcomp:s ∘ φ = idx:Sig V C⊢ φ (s x) = x
    calc φ (s x) = Sig.map s (Sig.map φ x) := hφ x
      _ = Sig.map (s ∘ φ) x := Sig.map_comp φ s x
      _ = Sig.map id x := byV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s idhcomp:s ∘ φ = idx:Sig V C⊢ Sig.map (s ∘ φ) x = Sig.map id x rw [hcompV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s idhcomp:s ∘ φ = idx:Sig V C⊢ Sig.map id x = Sig.map id x]All goals completed! 🐙
      _ = x := Sig.map_id xV:Type uC:Type us:Sig V C → Chinit:∀ {D : Type u} (t : Sig V D → D), ∃! h, IsSigHom s t hφ:C → Sig V Chφ:IsSigHom s (Sig.map s) φright✝:∀ (y : C → Sig V C), (fun h => IsSigHom s (Sig.map s) h) y → y = φhψ:IsSigHom s s (s ∘ φ)w✝:C → Cleft✝:IsSigHom s s w✝huniq:∀ (y : C → C), (fun h => IsSigHom s s h) y → y = w✝hidHom:IsSigHom s s idhcomp:s ∘ φ = idhleft:φ ∘ s = id⊢ Function.Bijective s
  exact Function.bijective_iff_has_inverse.mpr ⟨φ, congrFun hleft, congrFun hcomp⟩All goals completed! 🐙

초기성을 가설 hinit으로 받는다 — 다른 모든 Sig V-대수로 가는 준동형이 (C, s)에서 정확히 하나 있다는 뜻이다. 증명은 범주론의 표준 논증이다. 자식 자리에 s를 한 번 더 입힌 대수 (Sig V C, Sig.map s)로 가는 유일한 준동형 φ를 얻고, s ∘ φ와 id가 둘 다 (C, s)의 자기 준동형임을 보여 s ∘ φ = id를 얻는다. 그 등식을 φ의 준동형 조건에 다시 넣고 함자 법칙(map_id)을 쓰면 φ ∘ s = id도 나온다.

이 정리는 비채점 심화 B1.2로 분류하되 완성본으로 둔다. IntExp.lambek(심화 B1.1)이 C := IntExp V, s := IntExp.roll로 놓은 한 사례이지만, 그 사례를 따로 선언하지는 않는다 — 같은 결론을 복제하면 B1.1을 자명하게 만든다.