【LEAN4】Isom

同型写像

同型写像 $f: S \to T$ とは逆写像 $g:T \to S$ が存在し、$f\circ g = id_T$ と $g\circ f = id_S$ が成り立つもののことを言います。

ここで、$S, T$ はどの圏のオブジェクトでも構いません。

同型写像は圏によって姿を変え、もし、集合ならば全単射、位相空間なら同相写像に対応します。

同型写像の定義

leanの上で同型写像を定義するには

1. 同型写像 $f: S \to T$
2. 逆写像写像 $g:T \to S$
3. 右消去 $f\circ g = id_T$
4. 左消去 $g\circ f = id_S$

の4つの情報を持っておきます。

      class Isom (α β : Type) where
  to_fun    : α → β
  inv_fun   : β → α
  left_inv  : ∀ x, to_fun (inv_fun x) = x
  right_inv : ∀ x, inv_fun (to_fun x) = x
infix:25 " ≃ " => Isom
    

これを使って、leanで同型写像を定義する場合は以下のようにして定義します：

      def func_name (variables) : α ≃ β := ⟨
    {to_fun},
    {inv_fun},
    {left_inv},
    {right_inv}
⟩
    

同値関係であること

反射律

      def Isom.refl (α : Type) : α ≃ α := ⟨id, id, λ x => rfl, λ x => rfl⟩
    

対称律

      def Isom.symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩
    

推移律

      def Isom.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := by {
  let to_fun    := (fun x => e₂.to_fun (e₁.to_fun x));
  let inv_fun   := (fun x => e₁.inv_fun (e₂.inv_fun x));
  have left_inv : ∀ x, to_fun (inv_fun x) = x := by {
    intro x;
    simp [e₁.left_inv (e₂.inv_fun x),
          e₂.left_inv];
  };
  have right_inv :∀ x, inv_fun (to_fun x) = x := by {
    intro x;
    simp [e₂.right_inv (e₁.to_fun x),
          e₁.right_inv];
  };
  exact ⟨to_fun,inv_fun,left_inv,right_inv⟩;
}
    

全体コード

      class Isom (α β : Type) where
  to_fun    : α → β
  inv_fun   : β → α
  left_inv  : ∀ x, to_fun (inv_fun x) = x
  right_inv : ∀ x, inv_fun (to_fun x) = x
infix:25 " ≃ " => Isom

def Isom.refl (α : Type) : α ≃ α := ⟨id, id, λ x => rfl, λ x => rfl⟩
def Isom.symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩
def Isom.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := by {
  let to_fun    := (fun x => e₂.to_fun (e₁.to_fun x));
  let inv_fun   := (fun x => e₁.inv_fun (e₂.inv_fun x));
  have left_inv : ∀ x, to_fun (inv_fun x) = x := by {
    intro x;
    simp [e₁.left_inv (e₂.inv_fun x),
          e₂.left_inv];
  };
  have right_inv :∀ x, inv_fun (to_fun x) = x := by {
    intro x;
    simp [e₂.right_inv (e₁.to_fun x),
          e₁.right_inv];
  };
  exact ⟨to_fun,inv_fun,left_inv,right_inv⟩;
}