0

【LEAN4】Isom

38
0
$$$$

同型写像

同型写像 $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⟩;
}
    
投稿日:202157

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。

投稿者

furea2
furea2
2
668
昔数学を少しだけやってました

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中