:: Extensions of Mappings on Generator Set
:: by Artur Korni{\l}owicz
::
:: Received March 23, 1995
:: Copyright (c) 1995-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MEMBER_1, TARSKI,
REALSET1, FUNCT_1, PZFMISC1, MSUALG_3, FUNCT_6, MSAFREE, LANG1, MCART_1,
TREES_4, SUBSET_1, FUNCOP_1, PRELAMB, MSUALG_2, UNIALG_2, MARGREL1,
CARD_3, NAT_1, PARTFUN1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, XTUPLE_0,
MCART_1, PARTFUN1, FUNCOP_1, FUNCT_6, PZFMISC1, FINSEQ_2, STRUCT_0,
LANG1, FUNCT_2, CARD_3, ORDINAL1, TREES_4, DTCONSTR, PBOOLE, MSUALG_1,
MSUALG_2, MSUALG_3, MSAFREE;
constructors PZFMISC1, MSUALG_3, MSAFREE, RELSET_1, XTUPLE_0;
registrations FUNCT_1, RELSET_1, FUNCOP_1, PBOOLE, STRUCT_0, MSUALG_1,
MSUALG_3, MSAFREE, MSSUBFAM, FINSEQ_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin :: Preliminaries
reserve S for non void non empty ManySortedSign,
U1, U2, U3 for non-empty MSAlgebra over S,
I for set,
A for ManySortedSet of I,
B, C for non-empty ManySortedSet of I;
begin :: Facts about Many Sorted Functions
theorem :: EXTENS_1:1
for F be ManySortedFunction of A, B for X be ManySortedSubset of A st
A c= X holds F || X = F;
theorem :: EXTENS_1:2
for A, B be ManySortedSet of I for M be ManySortedSubset of A for F be
ManySortedFunction of A, B holds F.:.:M c= F.:.:A;
theorem :: EXTENS_1:3
for F be ManySortedFunction of A, B for M1, M2 be ManySortedSubset of
A st M1 c= M2 holds (F||M2).:.:M1 = F.:.:M1;
theorem :: EXTENS_1:4
for F be ManySortedFunction of A, B for G be ManySortedFunction
of B, C for X be ManySortedSubset of A holds (G ** F) || X = G ** (F || X);
theorem :: EXTENS_1:5
for A, B be ManySortedSet of I st A is_transformable_to B for F be
ManySortedFunction of A, B for C be ManySortedSet of I st B is ManySortedSubset
of C holds F is ManySortedFunction of A, C;
theorem :: EXTENS_1:6
for F be ManySortedFunction of A, B for X be ManySortedSubset of A
holds F is "1-1" implies F || X is "1-1";
begin :: doms & rngs of Many Sorted Function
theorem :: EXTENS_1:7
for F be ManySortedFunction of A, B for X be ManySortedSubset of A
holds doms (F || X) c= doms F;
theorem :: EXTENS_1:8
for F be ManySortedFunction of A, B for X be ManySortedSubset of A
holds rngs (F || X) c= rngs F;
theorem :: EXTENS_1:9
for A, B be ManySortedSet of I for F be ManySortedFunction of A, B
holds F is "onto" iff rngs F = B;
theorem :: EXTENS_1:10
for X be non-empty ManySortedSet of the carrier of S holds rngs Reverse X = X
;
theorem :: EXTENS_1:11
for F be ManySortedFunction of A, B for G be ManySortedFunction of B,
C for X be non-empty ManySortedSubset of B st rngs F c= X holds (G || X) ** F =
G ** F;
begin :: Other properties of "onto" & "1-1"
theorem :: EXTENS_1:12
for F be ManySortedFunction of A, B holds F is "onto" iff for C
for G, H be ManySortedFunction of B, C st G**F = H**F holds G = H;
theorem :: EXTENS_1:13
for F be ManySortedFunction of A, B st A is non-empty holds F is
"1-1" iff for C be ManySortedSet of I for G, H be ManySortedFunction of C, A st
F**G = F**H holds G = H;
begin :: Extensions of Mappings on Generator Set
theorem :: EXTENS_1:14
for X be non-empty ManySortedSet of the carrier of S for h1, h2
be ManySortedFunction of FreeMSA X, U1 st h1 is_homomorphism FreeMSA X, U1 & h2
is_homomorphism FreeMSA X, U1 & h1 || FreeGen (X) = h2 || FreeGen (X) holds h1
= h2;
theorem :: EXTENS_1:15
for F be ManySortedFunction of U1, U2 st F is_epimorphism U1, U2 for
U3 be non-empty MSAlgebra over S for h1, h2 be ManySortedFunction of U2, U3 st
h1**F = h2**F holds h1 = h2;
theorem :: EXTENS_1:16
for F be ManySortedFunction of U2, U3 st F is_homomorphism U2, U3
holds F is_monomorphism U2, U3 iff for U1 be non-empty MSAlgebra over S for h1,
h2 be ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2
is_homomorphism U1, U2 holds (F**h1 = F**h2 implies h1 = h2);
registration
let S, U1;
cluster non-empty for GeneratorSet of U1;
end;
theorem :: EXTENS_1:17
for U1 being MSAlgebra over S for A, B being MSSubset of U1 st A is
ManySortedSubset of B holds GenMSAlg A is MSSubAlgebra of GenMSAlg B;
theorem :: EXTENS_1:18
for U1 being MSAlgebra over S, U2 being MSSubAlgebra of U1 for B1
being MSSubset of U1, B2 being MSSubset of U2 st B1 = B2 holds GenMSAlg B1 =
GenMSAlg B2;
theorem :: EXTENS_1:19
for U1 being non-empty MSAlgebra over S for U2 being non-empty
MSAlgebra over S for Gen being GeneratorSet of U1 for h1, h2 being
ManySortedFunction of U1, U2 st h1 is_homomorphism U1, U2 & h2 is_homomorphism
U1, U2 & h1 || Gen = h2 || Gen holds h1 = h2;