-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy path类同态定理文字证明.lean
85 lines (77 loc) · 4.16 KB
/
类同态定理文字证明.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
w(gh) := w(g) + σ(g)^(-1)·w(h)
v(gh) := v(g) + ρ(g)^(-1)·v(h)
证明：（思路是一般化某个任意分量来做变化，是否成立。再推广到所有分量。）
已知g：{
方向过程量：w(g)= (p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12)
位置过程量：σ(g)
}
已知h：{
方向过程量：w(h)= (q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12)
位置过程量：σ(h)
}
1.先证明第一条公式：
对于某个状态Sta1：
方向绝对量：Sta1 = (j1,j2,j3,j4,j5,j6,j7,j8,j9,j10,j11,j12)
位置绝对量：(k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12)
1.经过g作用后：{
方向绝对量错误：(j1+p1,j2+p2,j3+p3,j4+p4,j5+p5,j6+p6,j7+p7,j8+p8,j9+p9,j10+p10,j11+p11,j12+p12)
方向过程量：Sta1 → (Sta1作用g以后) = w(g)
位置：σ(g)·(k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12)= ?
方向绝对量 : σ(g)·(j1+p1,j2+p2,j3+p3,j4+p4,j5+p5,j6+p6,j7+p7,j8+p8,j9+p9,j10+p10,j11+p11,j12+p12)
}
2.再经过h作用后：{
方向绝对量：σ(h)( σ(g)·(j1+p1,j2+p2,j3+p3,j4+p4,j5+p5,j6+p6,j7+p7,j8+p8,j9+p9,j10+p10,j11+p11,j12+p12) + (q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12) )
方向过程量：（Sta1作用g以后）→ (Sta1作用g以后,再作用h以后) = ？
位置：σ(h)·σ(g)·(k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12)= ？
}
小引理：绝对方向量A1 经过x→, 绝对方向量为A2， 和w(x)有什么关系，如何表达w(x):
σ(x)·(A1 + w(x)) = A2
所以,w(x) = (σ(x))^(-1)·A2 - A1
分析初始方向绝对量和最后2次作用后的方向绝对量,后者是按定义算出来的值。
(j1,j2,j3,j4,j5,j6,j7,j8,j9,j10,j11,j12) = "A1"
→
σ(h)( σ(g)·(j1+p1,j2+p2,j3+p3,j4+p4,j5+p5,j6+p6,j7+p7,j8+p8,j9+p9,j10+p10,j11+p11,j12+p12) + (q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12) )
= σ(h)·σ(g)·(j1+p1,j2+p2,j3+p3,j4+p4,j5+p5,j6+p6,j7+p7,j8+p8,j9+p9,j10+p10,j11+p11,j12+p12) + σ(h)·(q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12)
= "A2"
所以复合的方向过程量：
w(gh) := (σ(gh))^(-1)·A2 - A1 = (σ(g))^(-1)·σ(h)^(-1) · A2 - A1
= (j1+p1,j2+p2,j3+p3,j4+p4,j5+p5,j6+p6,j7+p7,j8+p8,j9+p9,j10+p10,j11+p11,j12+p12) +
(σ(g))^(-1)·(q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12) - (j1,j2,j3,j4,j5,j6,j7,j8,j9,j10,j11,j12)
= (p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12) + (σ(g))^(-1)·(q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12)
试着列举一下：
w(g) = (p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12)
σ(g)·w(h) = σ(g)·(q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12)
w(g) + σ(g)^(-1)·w(h)
= (p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12) + (σ(g))^(-1)·(q1,q2,q3,q4,q5,q6,q7,q8,q9,q10,q11,q12)
举例说明：
g=F,h=R,
经过gh后，
已知：
因为g换位效果ρ(g)是:
{a,b,c,d,e,f,g,h}
{e,a,c,d,f,b,g,h}
因为h换位效果ρ(h)是:
{a,b,c,d,e,f,g,h}
{a,f,b,d,e,g,c,h}
gh复合换位：
{a,b,c,d,e,f,g,h}
{e,b,a,d,f,g,c,h}
v(g) = {2, 1, 0, 0, 1, 2, 0, 0} = Og
v(h) = {0, 2, 1, 0, 0, 1, 2, 0} = Oh
-- v(gh) = v(g) + ρ(g)^(-1)·v(h)
-- 首先根据等式左边算一下，也就是根据定义算一下：
gh变换后绝对方向数 =(0先经过g操作：加v(g),然后被ρ(g)作用) => 0 + {2, 1, 0, 0, 1, 2, 0, 0} => ρ(g)·Og
=(经过h操作：加v(h),然后被ρ(h)作用) => (ρ(g)·Og+Oh) => ρ(h)·(ρ(g)·Og+Oh)
{小引理：绝对方向量A1， 经过x, 绝对方向量为A2， 和w(x)有什么关系，如何表达w(x):
σ(x)·(A1 + w(x)) = A2
左右2个向量同时作用(σ(x))^(-1)： (A1 + w(x)) = (σ(x))^(-1)·A2
所以,w(x) = (σ(x))^(-1)·A2 - A1}
v(gh) = (σ(gh))^(-1)·A2 - A1 = ?
这里A1 = 0, A2 = ρ(h)(ρ(g)·Og+Oh) ,
v(gh) = (ρ(gh))^(-1)·(ρ(h)·(ρ(g)·Og+Oh)) - 0
σ(gh)^(-1) = ρ(g)^(-1) · ρ(h)^(-1)
v(gh) => ρ(h)^(-1)·ρ(h)·(ρ(g)·Og+Oh)
=> (ρ(g)·Og+Oh)
=> ρ(g)^(-1) · (ρ(g)·Og+Oh)
=> ρ(g)^(-1)·Og + Oh
-- 这个过程其实就是单纯由定义简化而来的一个表达式。