Information Technology Reference
In-Depth Information
Lemma 2.
Let
D
(degree 1) a homomor-
phism of graded groups, satisfying
hh
=0
and
hd
D
∗
h
=
h
.Let
p
=
d
D
∗
h
+
hd
D
∗
(from the reduction properties in
Definition 2
follows that
id
D
∗
−
be a chain complex,
h
:
D
∗
→
D
∗
∗
p
=
gf
). Then
(
id
D
∗
−
to
ker(
p
)
.
Lemma 2 is used to give a (very easy) constructive proof of the following result.
p,
inc
ker(
p
)
,h
)
is a reduction from
D
∗
Lemma 3.
Assuming the conditions of the BPL,
and the equalities of Part
1
, there exists a canonical and explicit reduction
D
ker(
p
)
,where
p
∗
⇒
=
h
+
h
d
D
∗
d
D
∗
.
Lemma 4.
Assuming the conditions of the BPL,
and the equalities of Part 1
,
there exists a canonical and explicit isomorphism
of graded groups
between
ker(
p
)
and
ker(
p
)
,where
p
=
d
D
∗
h
+
hd
D
∗
and
p
=
d
D
∗
h
+
h
d
D
∗
.
Lemma 5.
Let
A
be a chain complex,
B
a graded group and
F
:
A
∗
→
B
,
∗
∗
∗
F
−
1
:
B
inverse isomorphisms
between graded groups
. Then, the graded
group homomorphism (degree -1)
d
B
∗
:=
Fd
A
∗
F
−
1
is a differential on
B
∗
→
A
∗
such
∗
that
F
and
F
−
1
become inverse isomorphisms
between chain complexes
.
Lemma 6.
Let
(
f, g, h
):
A
∗
⇒
B
be a reduction and
F
:
B
∗
→
C
a chain
∗
∗
complex isomorphism. Then
(
Ff,gF
−
1
,h
)
is a reduction from
A
to
C
.
∗
∗
Sketch of the BPL proof
- By applying Lemma 3, a reduction
D
ker(
p
)
is obtained. Then, by Lemma 4, a graded group isomorphism between ker(
p
)and
ker(
p
) is built. Now, from Lemma 1, one can conclude that ker(
p
)=ker(
id
D
∗
−
gf
)=im(
gf
)
=
C
∗
⇒
, and an explicit isomorphism
of graded groups
between
∗
ker(
p
)and
C
is defined (by composition). The differential of ker(
p
)hastobe
transferred to
C
∗
by applying Lemma 5, giving a new chain complex
C
,with
∗
∗
the property that ker(
p
)
=
C
as chain complexes. By applying Lemma 6 to
∗
ker(
p
)andker(
p
)
=
C
D
, an explicit reduction from
D
to
C
is obtained.
When the homomorphisms obtained in the different lemmas are consecutively
composed, the equalities in the BPL statement are exactly produced.
∗
⇒
∗
∗
∗
3
A Symbolic Approach
Our first approach consists in considering the objects in the statements (the
homomorphisms) as generic elements of an algebraic structure where equational
reasoning can be carried out. The idea is to identify, for instance, the elements of
a ring of homomorphisms with the elements of a generic ring. Then, calculations
in this ring are identified with proof steps in the reasoning domain (homomor-
phisms in the example). We call this a
symbolic approach
since homomorphisms
are represented simply by symbols (as elements of a generic ring) without refer-
ence to their nature as functions. In our case, one of the additional diculties of
the proofs we intend to implement is that most of them require the properties of
the various domains (with also elements of different nature and type) involved
in the proof; but when trying to implement mathematics in computers, an ab-
straction process is always needed to produce the translation of elements of the
Search WWH ::
Custom Search