CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

GAP 4.8.9 installation with standard packages -- copy to your CoCalc project to get it

Views: 418346
Tweet
Share
Share
1
\begin{sequent}

2
\begin{align*}

3
  &t, \alpha:\Mor\\

4
  |~ &\IsZero\big( \PreCompose( t, \alpha ) \big)\\

5
  \vdash &\PreCompose\big(\KernelLift( \alpha , t ), \KernelEmbedding( \alpha ) \big) =_{\Mor} t

6
\end{align*}

7
\end{sequent}

8


9
\begin{sequent}

10
\begin{align*}

11
  &t, \alpha:\Mor\\

12
  |~  &\IsZero\big(\PreCompose(\alpha, t)\big)\\

13
  \vdash &\PreCompose\big(\CokernelProjection( \alpha ), \CokernelColift( \alpha, t )\big) =_{\Mor} t

14
\end{align*}

15
\end{sequent}

16


17
\begin{sequent}

18
\begin{align*}

19
  &L:\ListObj, T:\ListMor, i:\Int\\

20
  | ~& \forall j \in [ 1, \dots, \Length( L ) ]: \IsEqualForObjects\big(\Source( T[1] ), \Source( T[j] ) \big) \\

21
  \vdash &\PreCompose\big(\UniversalMorphismIntoDirectProduct( L, T ), \\

22
  &\ProjectionInFactorOfDirectProduct( L, i ) \big) =_{\Mor} T[i]

23
\end{align*}

24
\end{sequent}

25


26
\begin{sequent}

27
\begin{align*}

28
  &L:\ListObj, T:\ListMor, i:\Int\\

29
  |~ &()\\

30
  \vdash &\PreCompose\big(\InjectionOfCofactorOfCoproduct( L, i ),\\

31
  &\UniversalMorphismFromCoproduct( L, T ) \big) =_{\Mor} T[i]

32
\end{align*}

33
\end{sequent}

34


35
\begin{sequent}

36
\begin{align*}

37
  &A, B:\Obj, \tau_A, \tau_B:\Mor \\

38
  |~ &()\\

39
  \vdash &\PreCompose\big(\InjectionOfCofactorOfCoproduct( [A, B], 2 ),\\

40
  &\UniversalMorphismFromCoproduct( [A,B], [\tau_A, \tau_B] ) \big) =_{\Mor} \tau_B 

41
\end{align*}

42
\end{sequent}

43


44


45
\begin{sequent}

46
\begin{align*}

47
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\

48
  |~ &\IsEqualForMorphisms\big( \PreCompose( \tau_A, \alpha ), \PreCompose( \tau_B, \beta ) \big)\\

49
  \vdash &\PreCompose\big( \UniversalMorphismIntoFiberProduct( [\alpha, \beta], [\tau_A, \tau_B] ), \\

50
  &\ProjectionInFactorOfFiberProduct( [\alpha, \beta], 1 ) \big) =_{\Mor} \tau_A

51
\end{align*}

52
\end{sequent}

53


54
\begin{sequent}

55
\begin{align*}

56
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\

57
  |~ &\IsEqualForMorphisms\big( \PreCompose( \tau_A, \alpha ), \PreCompose( \tau_B, \beta ) \big)\\

58
  \vdash &\PreCompose\big( \UniversalMorphismIntoFiberProduct( [\alpha, \beta], [\tau_A, \tau_B] ), \\

59
  &\ProjectionInFactorOfFiberProduct( [\alpha, \beta], 2 ) \big) =_{\Mor} \tau_B

60
\end{align*}

61
\end{sequent}

62


63
\begin{sequent}

64
\begin{align*}

65
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\

66
  |~ &\IsEqualForMorphisms\big( \PreCompose( \alpha, \tau_A ), \PreCompose( \beta, \tau_B) \big)\\

67
  \vdash &\PreCompose\big( \InjectionOfCofactorOfPushout( [\alpha, \beta], 1 ), \\

68
  &\UniversalMorphismFromPushout( [\alpha, \beta], [\tau_A, \tau_B] )\big) =_{\Mor} \tau_A

69
\end{align*}

70
\end{sequent}

71


72
\begin{sequent}

73
\begin{align*}

74
  &\alpha, \beta, \tau_A, \tau_B:\Mor \\

75
  |~ &\IsEqualForMorphisms\big( \PreCompose( \alpha, \tau_A ), \PreCompose( \beta, \tau_B) \big)\\

76
  \vdash &\PreCompose\big( \InjectionOfCofactorOfPushout( [\alpha, \beta], 2 ), \\

77
  &\UniversalMorphismFromPushout( [\alpha, \beta], [\tau_A, \tau_B] )\big) =_{\Mor} \tau_B

78
\end{align*}

79
\end{sequent}

80


81