Lean中定义子群模等价关系函数R的类型类实例错误求解

核心错误 #

变量声明中[K : subgroup G]的写法错误：subgroup G是结构类型而非类型类（type class），方括号[]仅用于声明Lean可自动推导的类型类实例（比如[group G]中的群结构），将K放在方括号里会让Lean误以为需要合成一个subgroup G类型类实例，导致后续无法关联到群G，出现类型模糊的问题。

修正步骤 #

1. 修正变量声明
   将K的声明从方括号改为圆括号（显式参数）或花括号（隐式参数），明确K是群G的一个具体子群：

variables {G : Type} [group G] [fintype G]
variables (K : subgroup G) [fintype K] -- 用圆括号声明K为显式参数

2. 修正关系R的定义
   确保R依赖于子群K，让Lean明确关联到群G：

def R (g h : G) : Prop :=
∃ (k : K), g = k * h

3. 修正辅助引理
   引理需要带上K参数以保证作用域正确：

lemma R_def (g h : G) : R K g h ↔ ∃ (k : K), g = k * h :=
begin
  refl,
end

完整可运行代码示例 #

import tactic
import group_theory.subgroup.basic
import group_theory.coset
import data.fintype.basic
import data.fintype.card

variables {G : Type} [group G] [fintype G]
variables (K : subgroup G) [fintype K]

def R (g h : G) : Prop :=
∃ (k : K), g = k * h

lemma R_def (g h : G) : R K g h ↔ ∃ (k : K), g = k * h :=
begin
  refl,
end

-- 证明自反性
lemma R_refl (g : G) : R K g g :=
begin
  use 1, -- 子群K的单位元属于K
  simp,
end

-- 证明对称性
lemma R_symm {g h : G} (hR : R K g h) : R K h g :=
begin
  rcases hR with ⟨k, h_eq⟩,
  use k⁻¹, -- 子群元素的逆元仍属于K
  rw [group.mul_inv_rev, h_eq, inv_mul_self],
  simp,
end

-- 证明传递性
lemma R_trans {g h l : G} (h1 : R K g h) (h2 : R K h l) : R K g l :=
begin
  rcases h1 with ⟨k1, h1_eq⟩,
  rcases h2 with ⟨k2, h2_eq⟩,
  use k1 * k2, -- 子群对乘法封闭，k1*k2属于K
  rw [h1_eq, h2_eq, mul_assoc],
end

-- 最终确认R是等价关系
instance : equivalence (R K) :=
begin
  refine ⟨R_refl K, R_symm K, R_trans K⟩,
end

内容的提问来源于stack exchange，提问作者dashok