:: FUNCTOR1 semantic presentation

registration

cluster non empty transitive with_units reflexive AltCatStr ;
existence

proof end;

end;

registration

let c₁ be non empty reflexive AltCatStr ;
cluster non empty reflexive SubCatStr of a₁;
existence

proof end;

end;

registration

let c₁, c₂ be non empty reflexive AltCatStr ;
let c₃ be feasible FunctorStr of c₁,c₂;
let c₄ be non empty reflexive SubCatStr of c₁;
cluster a₃ | a₄ -> feasible ;
coherence ;

end;

theorem Th1: :: FUNCTOR1:1

for b₁ being set holds id b₁ is onto

proof end;

theorem Th2: :: FUNCTOR1:2

for b₁ being non empty set
for b₂, b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st b₃ = b₄ holds
incl b₃ = (incl b₂) * (incl b₄)

proof end;

theorem Th3: :: FUNCTOR1:3

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st b₃ is bijective holds
b₃ " is Function of b₂,b₁

proof end;

theorem Th4: :: FUNCTOR1:4

for b₁, b₂ being set
for b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is bijective & b₅ is bijective holds
ex b₆ being Function of b₁,b₃ st
( b₆ = b₅ * b₄ & b₆ is bijective )

proof end;

theorem Th5: :: FUNCTOR1:5

for b₁ being non empty reflexive AltCatStr
for b₂ being non empty reflexive SubCatStr of b₁
for b₃ being non empty SubCatStr of b₁
for b₄ being non empty SubCatStr of b₂ st b₃ = b₄ holds
incl b₃ = (incl b₂) * (incl b₄)

proof end;

theorem Th6: :: FUNCTOR1:6

for b₁, b₂ being non empty AltCatStr
for b₃ being FunctorStr of b₁,b₂ st b₃ is bijective holds
( the ObjectMap of b₃ is bijective & the MorphMap of b₃ is "1-1" )

proof end;

theorem Th7: :: FUNCTOR1:7

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is one-to-one & b₅ is one-to-one holds
b₅ * b₄ is one-to-one

proof end;

theorem Th8: :: FUNCTOR1:8

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is faithful & b₅ is faithful holds
b₅ * b₄ is faithful

proof end;

theorem Th9: :: FUNCTOR1:9

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is onto & b₅ is onto holds
b₅ * b₄ is onto

proof end;

theorem Th10: :: FUNCTOR1:10

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is full & b₅ is full holds
b₅ * b₄ is full

proof end;

theorem Th11: :: FUNCTOR1:11

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is injective & b₅ is injective holds
b₅ * b₄ is injective

proof end;

theorem Th12: :: FUNCTOR1:12

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is surjective & b₅ is surjective holds
b₅ * b₄ is surjective

proof end;

theorem Th13: :: FUNCTOR1:13

for b₁ being non empty AltGraph
for b₂, b₃ being non empty reflexive AltGraph
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃ st b₄ is bijective & b₅ is bijective holds
b₅ * b₄ is bijective

proof end;

theorem Th14: :: FUNCTOR1:14

for b₁, b₂ being non empty reflexive AltCatStr
for b₃ being non empty reflexive SubCatStr of b₁
for b₄ being non empty SubCatStr of b₁
for b₅ being non empty SubCatStr of b₃ st b₄ = b₅ holds
for b₆ being FunctorStr of b₁,b₂ holds b₆ | b₄ = (b₆ | b₃) | b₅

proof end;

theorem Th15: :: FUNCTOR1:15

for b₁, b₂, b₃ being non empty reflexive AltCatStr
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being FunctorStr of b₂,b₃
for b₆ being non empty reflexive SubCatStr of b₁ holds (b₅ * b₄) | b₆ = b₅ * (b₄ | b₆) by FUNCTOR0:33;

theorem Th16: :: FUNCTOR1:16

canceled;

theorem Th17: :: FUNCTOR1:17

for b₁ being non empty AltCatStr
for b₂ being non empty SubCatStr of b₁ holds
( b₂ is full iff incl b₂ is full )

proof end;

theorem Th18: :: FUNCTOR1:18

for b₁, b₂ being non empty AltCatStr
for b₃ being Covariant FunctorStr of b₁,b₂ holds
( b₃ is full iff for b₄, b₅ being object of b₁ holds Morph-Map b₃,b₄,b₅ is onto )

proof end;

theorem Th19: :: FUNCTOR1:19

for b₁, b₂ being non empty AltCatStr
for b₃ being Covariant FunctorStr of b₁,b₂ holds
( b₃ is faithful iff for b₄, b₅ being object of b₁ holds Morph-Map b₃,b₄,b₅ is one-to-one )

proof end;

theorem Th20: :: FUNCTOR1:20

for b₁ being non empty transitive with_units AltCatStr holds (id b₁) " = id b₁

proof end;

theorem Th21: :: FUNCTOR1:21

for b₁, b₂ being non empty transitive with_units reflexive AltCatStr
for b₃ being feasible FunctorStr of b₁,b₂ st b₃ is bijective holds
for b₄ being feasible FunctorStr of b₂,b₁ st FunctorStr(# the ObjectMap of b₄,the MorphMap of b₄ #) = b₃ " holds
b₃ * b₄ = id b₂

proof end;

Lemma11: for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ holds
for b₄ being ManySortedFunction of b₂,b₃
for b₅ being ManySortedFunction of b₃,b₂ st b₄ is "1-1" & b₄ is "onto" & b₅ = b₄ "" holds
( b₄ ** b₅ = id b₃ & b₅ ** b₄ = id b₂ )

proof end;

theorem Th22: :: FUNCTOR1:22

for b₁, b₂ being non empty transitive with_units reflexive AltCatStr
for b₃ being feasible FunctorStr of b₁,b₂ st b₃ is bijective holds
(b₃ " ) * b₃ = id b₁

proof end;

theorem Th23: :: FUNCTOR1:23

for b₁, b₂ being non empty transitive with_units reflexive AltCatStr
for b₃ being feasible FunctorStr of b₁,b₂ st b₃ is bijective holds
(b₃ " ) " = FunctorStr(# the ObjectMap of b₃,the MorphMap of b₃ #)

proof end;

theorem Th24: :: FUNCTOR1:24

for b₁, b₂, b₃ being non empty transitive with_units reflexive AltCatStr
for b₄ being feasible FunctorStr of b₁,b₂
for b₅ being feasible FunctorStr of b₂,b₃
for b₆ being feasible FunctorStr of b₂,b₁
for b₇ being feasible FunctorStr of b₃,b₂ st b₅ is bijective & b₄ is bijective & b₇ is bijective & b₆ is bijective & FunctorStr(# the ObjectMap of b₆,the MorphMap of b₆ #) = b₄ " & FunctorStr(# the ObjectMap of b₇,the MorphMap of b₇ #) = b₅ " holds
(b₅ * b₄) " = b₆ * b₇

proof end;