:: Basic Properties of Functor Structures
:: by Claus Zinn and Wolfgang Jaksch
::
:: Received April 24, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

registration
cluster non empty transitive with_units reflexive for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is with_units & b1 is reflexive )
proofend;
end;

registration
let A be non empty reflexive AltCatStr ;
cluster non empty reflexive for SubCatStr of A;
existence
 ex b1 being SubCatStr of A st
( not b1 is empty & b1 is reflexive )
proofend;
end;

registration
let C1, C2 be non empty reflexive AltCatStr ;
let F be feasible FunctorStr over C1,C2;
let A be non empty reflexive SubCatStr of C1;
clusterF | A ->  feasible ;
coherence
 F | A is feasible ;
end;

begin

registration
let X be set ;
cluster id X ->  onto ;
coherence
 id X is onto
proofend;
end;

theorem :: FUNCTOR1:1
for A being non empty set
for B, C being non empty Subset of A
for D being non empty Subset of B st C = D holds
incl C = (incl B) * (incl D)
proofend;

theorem Th2: :: FUNCTOR1:2
for X, Y being set
for f being Function of X,Y st f is bijective holds
f " is Function of Y,X
proofend;

theorem :: FUNCTOR1:3
for X, Y being set
for Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is bijective & g is bijective holds
ex h being Function of X,Z st
( h = g * f & h is bijective )
proofend;

begin

theorem Th4: :: FUNCTOR1:4
for A being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
proofend;

theorem Th5: :: FUNCTOR1:5
for A, B being non empty AltCatStr
for F being FunctorStr over A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
proofend;

:: ===================================================================
:: Lemmata about properties of G*F, where G,F are FunctorStr
:: ===================================================================
theorem Th6: :: FUNCTOR1:6
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds
G * F is one-to-one
proofend;

theorem Th7: :: FUNCTOR1:7
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
proofend;

theorem Th8: :: FUNCTOR1:8
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is onto & G is onto holds
G * F is onto
proofend;

theorem Th9: :: FUNCTOR1:9
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is full & G is full holds
G * F is full
proofend;

theorem Th10: :: FUNCTOR1:10
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is injective & G is injective holds
G * F is injective
proofend;

theorem Th11: :: FUNCTOR1:11
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds
G * F is surjective
proofend;

theorem Th12: :: FUNCTOR1:12
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds
G * F is bijective
proofend;

begin

theorem :: FUNCTOR1:13
for A, I being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
proofend;

theorem :: FUNCTOR1:14
for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff incl B is full )
proofend;

begin

theorem :: FUNCTOR1:15
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto )
proofend;

theorem :: FUNCTOR1:16
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one )
proofend;

begin

theorem :: FUNCTOR1:17
for A being non empty transitive with_units AltCatStr holds (id A) " = id A
proofend;

:: ===================================================================
theorem :: FUNCTOR1:18
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B
proofend;

Lm1:  for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
proofend;

:: ===================================================================
theorem :: FUNCTOR1:19
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
(F ") * F = id A
proofend;

:: ===================================================================
theorem :: FUNCTOR1:20
for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
proofend;

theorem :: FUNCTOR1:21
for A, B, C being non empty transitive with_units reflexive AltCatStr
for G being feasible FunctorStr over A,B
for F being feasible FunctorStr over B,C
for GI being feasible FunctorStr over B,A
for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds
(F * G) " = GI * FI
proofend;