From ef679a295996c901b8d417330740f8ac1133d772 Mon Sep 17 00:00:00 2001 From: 5HT Date: Mon, 30 Oct 2023 12:11:53 +0200 Subject: [PATCH] iso --- foundations/univalent/iso/index.html | 22 ++- foundations/univalent/iso/index.pug | 17 +- foundations/univalent/path/index.html | 66 +++---- intro/index.html | 44 ++--- mathematics/algebra/algebra/index.html | 86 ++++----- mathematics/algebra/homology/index.html | 140 +++++++------- mathematics/analysis/set/index.html | 18 +- mathematics/categories/category/index.html | 98 +++++----- mathematics/categories/presheaf/index.html | 158 ++++++++-------- mathematics/categories/topos/index.html | 208 ++++++++++----------- mathematics/geometry/bundle/index.html | 32 ++-- mathematics/geometry/derham/index.html | 74 ++++---- mathematics/homotopy/cw/index.html | 44 ++--- mathematics/homotopy/hopf/index.html | 78 ++++---- mathematics/homotopy/pullback/index.html | 18 +- mathematics/homotopy/pushout/index.html | 22 +-- spec/index.html | 30 +-- 17 files changed, 588 insertions(+), 567 deletions(-) diff --git a/foundations/univalent/iso/index.html b/foundations/univalent/iso/index.html index 193047b2..5fe8e7cf 100644 --- a/foundations/univalent/iso/index.html +++ b/foundations/univalent/iso/index.html @@ -8,20 +8,26 @@ ISO

ISOMORPHISM

Just like notion of represents equality -of types and within given universe .

Formation

(Isomorphism Formation).

def iso (A B: U) : U := +of types and within given universe . However instead of Fibration it +uses Section and Retract for its definition and unlike equivalence +isomorphism predicate is not a proposition:

This difference was one of the main drivers for developing +cubical interpretation of equivalence/univalence as +isomorphism/unimorphism is unsatisfactory candidate for basic notion +of multidimensional inequality due to loss of propositional preservation. +

Formation

(Isomorphism Formation).

def iso (A B: U) : U := Σ (f : A -> B) (g : B -> A) (s : section A B f g) - (t : retract A B f g), 𝟏

Introduction

(Isomorphism Introduction).

def iso-intro (A: U) + (t : retract A B f g), 𝟏

Introduction

(Isomorphism Introduction).

def iso-intro (A: U) : iso A A := ( id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), star - )

Elimination

(Isomorphism Induction Principle). -For any -and it's evidence at -there is a function:

def ind-Iso (A B: U) + )

Elimination

(Isomorphism Induction Principle). +For any +and it's evidence at +there is a function:

def ind-Iso (A B: U) (C: Π (A B: U), iso A B → U) (d: C A A (iso-Intro A)) : Π (e: iso A B), P A B e @@ -34,14 +40,14 @@ Retract/Section based Isomorphism could be introduced as forth-back transport between isomorphism and path equality. This notion is somehow cannonical to all -cubical systems and is called Unimorphism or here.

Formation

(Unimorphism Formation).

Introduction

(Unimorphism Introduction).

def iso→Path (A B : U) +cubical systems and is called Unimorphism or here.

Formation

(Unimorphism Formation).

Introduction

(Unimorphism Introduction).

def iso→Path (A B : U) (f : A -> B) (g : B -> A) (s : Π (y : B), Path B (f (g y)) y) (t : Π (x : A), Path A (g (f x)) x) : PathP (<_> U) A B := <i> Glue B (∂ i) [ (i = 0) -> (A,f, isoToEquiv A B f g s t), - (i = 1) -> (B,id B, idIsEquiv B)]

Elimination

(Unimorphism Elimination).

def uni-Elim (A B : U) + (i = 1) -> (B,id B, idIsEquiv B)]

Elimination

(Unimorphism Elimination).

def uni-Elim (A B : U) : PathP (<_> U) A B -> iso A B := λ (p : PathP (<_> U) A B), ( coerce A B p, diff --git a/foundations/univalent/iso/index.pug b/foundations/univalent/iso/index.pug index 287bd318..8e7669ad 100644 --- a/foundations/univalent/iso/index.pug +++ b/foundations/univalent/iso/index.pug @@ -21,7 +21,22 @@ block content time Published: 26 NOV 2017 +tex. Just like $\mathrm{Equiv}$ notion of $\mathrm{Iso}$ represents equality - of types $A$ and $B$ within given universe $U$. + of types $A$ and $B$ within given universe $U$. However instead of Fibration it + uses Section and Retract for its definition and unlike equivalence + isomorphism predicate is not a proposition: + +tex(true). + $$ + \prod_{f : A \rightarrow B}\mathrm{isProp}\ (\mathrm{isEquiv}_f), + $$ + +tex(true). + $$ + \prod_{f : \Pi(x:S^1), x\equiv x} \neg \mathrm{isProp}\ (\mathrm{isIso}_f). + $$ + +tex. + This difference was one of the main drivers for developing + cubical interpretation of equivalence/univalence as + isomorphism/unimorphism is unsatisfactory candidate for basic notion + of multidimensional inequality due to loss of propositional preservation. h2 Formation +tex. $\mathbf{Definition}$ (Isomorphism Formation). diff --git a/foundations/univalent/path/index.html b/foundations/univalent/path/index.html index 3665af2a..e0af3588 100644 --- a/foundations/univalent/path/index.html +++ b/foundations/univalent/path/index.html @@ -7,10 +7,10 @@ use[data-c]{stroke-width:3px} PATH

PATH SPACES

The homotopy identity system defines a -space indexed over type -with elements as functions from interval to values -of that path space . HoTT book +PATH

PATH SPACES

The homotopy identity system defines a +space indexed over type +with elements as functions from interval to values +of that path space . HoTT book defines two induction principles for identity types: path induction and based path induction. The cubical type system CCHM briefly described in [1,2,3,4,5].

1 — Bezem, Coquand, Huber (2014)
@@ -18,33 +18,33 @@ 3 — Pitts, Orton (2016)
4 — Huber (2017)
5 — Vezzosi, Mörtberg , Abel (2019)
-

Formation

(Path Formation).

def Path (A : U) (x y : A) : U +

Formation

(Path Formation).

def Path (A : U) (x y : A) : U := PathP (<_> A) x y def Pathᴵ (A : U) (x y : A) := Π (i : I), A [∂ i |-> [(i = 0) → x , - (i = 1) → y ]]

Introduction

(Path Introduction).

def idp (A: U) (x: A) + (i = 1) → y ]]

Introduction

(Path Introduction).

def idp (A: U) (x: A) : Path A x x := <_> x

Returns a reflexivity path space for a given value of the type. The inhabitant of that path space is the lambda on the homotopy -interval that returns a constant value . Written in -syntax as . -

(Path Application).

def at0 (A: U) (a b: A) +interval that returns a constant value . Written in +syntax as . +

(Path Application).

def at0 (A: U) (a b: A) (p: Path A a b) : A := p @ 0 def at1 (A: U) (a b: A) - (p: Path A a b): A := p @ 1

(Path Connections).

Connections allow you to build a square -with only one element of path: i) ; -ii) . -

-

+ (p: Path A a b): A := p @ 1

(Path Connections).

Connections allow you to build a square +with only one element of path: i) ; +ii) . +

+

def join (A: U) (a b: A) (p: Path A a b) : PathP (<x> Path A (p@x) b) p (<i> b) := <y x> p @ (x \/ y) def meet (A: U) (a b: A) (p: Path A a b) : PathP (<x> Path A a (p@x)) (<i> a) p - := <x y> p @ (x /\ y)

(Path Inversion).

(Congruence).

def ap (A B: U) (f: A -> B) + := <x y> p @ (x /\ y)

(Path Inversion).

(Congruence).

def ap (A B: U) (f: A -> B) (a b: A) (p: Path A a b) : Path B (f a) (f b) @@ -52,56 +52,56 @@ (f: A -> B a) (b: B a) (p: Path A a x) : Path (B a) (f a) (f x)

Maps a given path space between values of one type to path space of another type using an encode function between types. -Implemented as a lambda defined on that returns +Implemented as a lambda defined on that returns application of encode function to path application of -the given path to lamda argument +the given path to lamda argument in both cases. -

(Generalized Transport Kan Operation). +

(Generalized Transport Kan Operation). Transports a value of the left type to the value of the right type -by a given path element of the path space between left and right types.

def transp' (A: U) (x y: A) (p : PathP (<_>A) x y) (i: I) +by a given path element of the path space between left and right types.

def transp' (A: U) (x y: A) (p : PathP (<_>A) x y) (i: I) := transp (<i> (\(_:A),A) (p @ i)) i x def transpᵁ (A B: U) (p : PathP (<_>U) A B) (i: I) - := transp (<i> (\(_:U),U) (p @ i)) i A

(Partial Elements).

def Partial' (A : U) (i : I) - : V := Partial A i

(Cubical Subtypes).

def sub (A : U) (i : I) (u : Partial A i) - : V := A [i ↦ u]

(Cubical Elements).

def inS (A : U) (i : I) (a : A) + := transp (<i> (\(_:U),U) (p @ i)) i A

(Partial Elements).

def Partial' (A : U) (i : I) + : V := Partial A i

(Cubical Subtypes).

def sub (A : U) (i : I) (u : Partial A i) + : V := A [i ↦ u]

(Cubical Elements).

def inS (A : U) (i : I) (a : A) : sub A i [(i = 1) → a] := inc A i a def outS (A : U) (i : I) (u : Partial A i) - : A [i ↦ u] -> A := λ (a: A[i ↦ u]), ouc a

(Heterogeneous Composition Kan Operation).

def compCCHM (A : I → U) (r : I) + : A [i ↦ u] -> A := λ (a: A[i ↦ u]), ouc a

(Heterogeneous Composition Kan Operation).

def compCCHM (A : I → U) (r : I) (u : Π (i : I), Partial (A i) r) (u₀ : (A 0)[r ↦ u 0]) : A 1 := hcomp (A 1) r (λ (i : I), [ (r = 1) → transp (<j> A (i ∨ j)) i (u i 1=>1)]) - (transp (<i> A i) 0 (ouc u₀))

(Homogeneous Composition Kan Operation).

def compCHM (A : U) (r : I) + (transp (<i> A i) 0 (ouc u₀))

(Homogeneous Composition Kan Operation).

def compCHM (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : A - := hcomp A r u (ouc u₀)

(Substitution).

def subst (A: U) (P: A -> U) (x y: A) (p: Path A x y) + := hcomp A r u (ouc u₀)

(Substitution).

def subst (A: U) (P: A -> U) (x y: A) (p: Path A x y) : P x -> P y - := λ (e: P x), transp (<i> P (p @ i)) 0 e

Other synonyms are and .

(Path Composition).

def pcomp (A: U) (a b c: A) + := λ (e: P x), transp (<i> P (p @ i)) 0 e

Other synonyms are and .

(Path Composition).

def pcomp (A: U) (a b c: A) (p: Path A a b) (q: Path A b c) : Path A a c := subst A (Path A a) b c q p

Composition operation allows building a new path from two given paths in a connected point. The proofterm is -. -

Elimination

(J by Paulin-Mohring).

def J (A: U) +. +

Elimination

(J by Paulin-Mohring).

def J (A: U) (a b: A) (P: singl A a -> U) (u: P (a,refl A a)) : П (p: Path A a b), P (b,p)

J is formulated in a form of Paulin-Mohring and implemented using two facts that singletons are contractible and dependent function transport. -

(Contractability of Singleton).

def singl (A: U) (a: A) : U +

(Contractability of Singleton).

def singl (A: U) (a: A) : U := Σ (x: A), Path A a x def contr (A: U) (a b: A) (p: Path A a b) : Path (singl A a) (a,<_>a) (b,p)

Proof that singleton is contractible space. Implemented as -. -

(HoTT Dependent Eliminator).

def J (A: U) +. +

(HoTT Dependent Eliminator).

def J (A: U) (a: A) (C: (x: A) -> Path A a x -> U) (d: C a (refl A a)) (x: A) : П (p: Path A a x) : C x p

J from HoTT book. -

(Diagonal Path Induction).

def D (A: U) : U +

(Diagonal Path Induction).

def D (A: U) : U := П (x y: A), Path A x y -> U def J (A: U) @@ -109,7 +109,7 @@ (C: D A) (d: C x x (refl A x)) (y: A) - : П (p: Path A x y), C x y p

Computation

(Path Computation).

def trans_comp (A: U) (a: A) + : П (p: Path A x y), C x y p

Computation

(Path Computation).

def trans_comp (A: U) (a: A) : Path A a (trans A A (<_> A) a) def subst_comp (A: U) (P: A -> U) (a: A) (e: P a) diff --git a/intro/index.html b/intro/index.html index 44214649..9412a1e8 100644 --- a/intro/index.html +++ b/intro/index.html @@ -16,29 +16,29 @@ їх рівнянь — бета і ета правил обчислювальності та унікальності. Зазвичай теорія типів, як мова програмування, вже постачається з наступними типами (примітивами-аксіомами) -та коментарями у вигляді окремих лекцій (конспекти, документація):

Простори функцій ()
- Простори пар ()
- Ідентифікаційні простори ()
- Поліноміальні функтори ()
- Простори шляхів ()
- Склейки ()
- Інфінітезимальні околи ()
- Фактор-простори Lean ()
- CW-комплекси ()

Слухачам курсу (10) пропонується застосувати +та коментарями у вигляді окремих лекцій (конспекти, документація):

Простори функцій ()
+ Простори пар ()
+ Ідентифікаційні простори ()
+ Поліноміальні функтори ()
+ Простори шляхів ()
+ Склейки ()
+ Інфінітезимальні околи ()
+ Фактор-простори Lean ()
+ CW-комплекси ()

Слухачам курсу (10) пропонується застосувати теорію типів для доведення початкового але нетривіального результу, який є відкритою проблемою в теорії типів для однєї із -математик, що є курсами на кафедрі чистої математики (КМ-111):

Теорія гомотопій
- Гомологічна алгебра
- Теорія категорій
- Функціональний аналіз
- Диференціальна геометрія

Курс (10) умовно можна розділити на 4 частини, кожна з яких показує +математик, що є курсами на кафедрі чистої математики (КМ-111):

Теорія гомотопій
+ Гомологічна алгебра
+ Теорія категорій
+ Функціональний аналіз
+ Диференціальна геометрія

Курс (10) умовно можна розділити на 4 частини, кожна з яких показує не тільки типи-аксіоми, але і мета-теоретичні спряження в яких вони приймають участь.

Мотивація

Головна мотивація гомотопічної теорії — надати обчислювальну семантику гомотопічним типам та CW-комплексам. Головна ідея гомотопічної теорії [1] полягає в поєднанні -просторів функцій , просторів контекстів і -просторів шляхів таким чином, що вони +просторів функцій , просторів контекстів і +просторів шляхів таким чином, що вони утворюють фібраційну рівність яка збігається (доводиться в самій теорії) з простором шляхів.

def isContr (A: U) : U @@ -84,22 +84,22 @@ ★ )

За цей час були перепробувані глобулярні та сімліціальні моделі, але аксіома унівалентності конструктивно валідується тільки в кубічних множинах, -на рівні теорії типів це відбувається в Кан-операціях та . +на рівні теорії типів це відбувається в Кан-операціях та .


˙

[1]. Pelayo, Warren. Homotopy type theory and Voevodsky's univalent foundations. 2012. -

Фібраційні доведення

Фібраційні доведення моделюються примітивами-аксіомами які є +

Фібраційні доведення

Фібраційні доведення моделюються примітивами-аксіомами які є теоретико-типовими відображеннями категорної мета-теоретичної моделі спряжень трьох функторів Кока-Райта, з яких народжуються простори функцій та простори контекстів: 1) Простір функцій (П); 2) Простір пар (Σ). Ці способи доведення дозволяють безпосреденьо аналізувати розшарування. -

Доведення рівності

В інтенсіональній теорії типів тип рівності вбудований теж +

Доведення рівності

В інтенсіональній теорії типів тип рівності вбудований теж як теоретико-типові примітиви категорної мета-теоретичної моделі спряжень трьох функторів Якобса-Лавіра: 1) Фактор-простору (Q); 2) Ідентифікаційної системи (=); 3) Стягуваного простору (С). Ці способи доведення дозволяють безпосередньо працювати з ідентифікаційними системами: строгою для теорії множин і гомотопічною для теорії гомотопій. -

Індуктивні доведення

В теорії типів індуктивні типи можуть бути вбудованими декількома +

Індуктивні доведення

В теорії типів індуктивні типи можуть бути вбудованими декількома способами: як поліноміальні функтори W і M або загальні схеми ідуктивних типів Полін-Морін (Calculus of Inductive Constructions) з такими властивостями @@ -113,10 +113,10 @@ виступати також простори шляхів, також моделюються поліноміальними функторами, але на відміну F-алгебр Ламбека-Бома тут використовуються монади-алгебри та комонади-коалгебри Люмсдейна-Шульмана-Веццозі. -

Геометричні доведення

Для потреб диференціальної геометрії в теорію типів вбудовують примітиви-аксіоми +

Геометричні доведення

Для потреб диференціальної геометрії в теорію типів вбудовують примітиви-аксіоми категорної мета-теоретичної моделі трьох функторів Шрайбера-Шульмана: 1) Інфінітезімального околу (Im); 2) Редукованої модальності (Re); 3) Інфінітезімального дискретного околу (&). -

Лінійні доведення

+

Лінійні доведення

\ No newline at end of file diff --git a/mathematics/algebra/algebra/index.html b/mathematics/algebra/algebra/index.html index a1620180..986aff63 100644 --- a/mathematics/algebra/algebra/index.html +++ b/mathematics/algebra/algebra/index.html @@ -10,53 +10,53 @@ ALGEBRA

ALGEBRAIC STRUCTURE

Results presented here are formalized in Ground Zero library using Lean Theorem Prover. -

ALGEBRA

Definition. Signature over given types -(called indices) is an element of type . +

ALGEBRA

Definition. Signature over given types +(called indices) is an element of type .
-Where denotes coproduct type. -

Definition. Vector of length over type -(denoted ) is a type: - +Where denotes coproduct type. +

Definition. Vector of length over type +(denoted ) is a type: +
-Where denotes unit type that contains -only . -

Definition. Assume we have types , -function , and a natural number . -Then we define function : - ≔ -

Definition. -ary algebraic operation over given - type is an element of type: - -

Definition. -ary algebraic relation over given - type is an element of type: - +Where denotes unit type that contains +only . +

Definition. Assume we have types , +function , and a natural number . +Then we define function : + ≔ +

Definition. -ary algebraic operation over given + type is an element of type: + +

Definition. -ary algebraic relation over given + type is an element of type: +
-Where denotes type of all propositions, i.e. - ≔ -

Definition. Algebraic structure over signature constists of: +Where denotes type of all propositions, i.e. + ≔ +

Definition. Algebraic structure over signature constists of: (i) 0-Type called carrier, - (ii) -ary algebraic operation for each , - (iii) -ary algebraic relation for each . + (ii) -ary algebraic operation for each , + (iii) -ary algebraic relation for each .
Or, more explicitly: - ≔ - -
We will write for carrier of algebraic structure , - for its algebraic operations, -and for its relations. -

Mappings

(Homomorphism). Given two algebraic structures over signature -and a function between them , -we say that is homomorphism iff holds: -
(i) , -
(ii) , -
for each or and . -

Composition of two homomorphisms is also homomorphism. -

(Isomorphism). We say that + ≔ + +
We will write for carrier of algebraic structure , + for its algebraic operations, +and for its relations. +

Mappings

(Homomorphism). Given two algebraic structures over signature +and a function between them , +we say that is homomorphism iff holds: +
(i) , +
(ii) , +
for each or and . +

Composition of two homomorphisms is also homomorphism. +

(Isomorphism). We say that is an ismorphism iff it is bijective and homomorphism. -Then we can say that and are isomorphic and write . -

Isomorphism is an equivalence relation, i.e. -
(i) , -
(ii) , -
(iii) . -

(Univalence for Algebraic Structures). - +Then we can say that and are isomorphic and write . +

Isomorphism is an equivalence relation, i.e. +
(i) , +
(ii) , +
(iii) . +

(Univalence for Algebraic Structures). +

\ No newline at end of file diff --git a/mathematics/algebra/homology/index.html b/mathematics/algebra/homology/index.html index f12cf114..13cc590b 100644 --- a/mathematics/algebra/homology/index.html +++ b/mathematics/algebra/homology/index.html @@ -10,20 +10,20 @@ HOMOLOGY

HOMOLOGY

Homology package contains basic theorems about general homology theory.

SETS

Definition (Proposition, Set). -Type is a proposition if -all elements of are equal. -Type is a set if -all paths between elements of are equal. -≔ -≔

n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where +Type is a proposition if +all elements of are equal. +Type is a set if +all paths between elements of are equal. +≔ +≔

n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n } isProp (A: U): U = n_grpd A Z -isSet (A: U): U = n_grpd A (S Z)


GROUPS

(Monoid). Monoid is a set equipped +isSet (A: U): U = n_grpd A (S Z)


GROUPS

(Monoid). Monoid is a set equipped with binary associative operation - called multiplication and identity element satisfying -.

isMonoid (M: SET): U + called multiplication and identity element satisfying +.

isMonoid (M: SET): U = (op: M.1 -> M.1 -> M.1) * (assoc: isAssociative M.1 op) * (id: M.1) @@ -36,9 +36,9 @@ monoidhom (a b: monoid): U = (f: a.1.1 -> b.1.1) * (ismonoidhom a b f) -

(Group). Group is a monoid -with inversion satisfying -.

isGroup (G: SET): U +

(Group). Group is a monoid +with inversion satisfying +.

isGroup (G: SET): U = (m: isMonoid G) * (inv: G.1 -> G.1) * (hasInverse G.1 m.1 m.2.2.1 inv) @@ -46,7 +46,7 @@ opGroup (g: group): g.1.1 -> g.1.1 -> g.1.1 idGroup (g: group): g.1.1 invGroup (g: group): g.1.1 -> g.1.1 -

(Differential Group).

isDifferentialGroup (G: SET): U +

(Differential Group).

isDifferentialGroup (G: SET): U = (g: isGroup G) * (comm: isCommutative G.1 g.1.1) * (boundary: G.1 -> G.1) @@ -54,98 +54,98 @@ dgroup: U = (X: SET) * isDifferentialGroup X dgrouphom (a b: dgroup): U = monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1) -unitDGroup: dgroup

(Division). -≔ -≔

ldiv (H: group) (g h: H.1.1) : H.1.1 +unitDGroup: dgroup

(Division). +≔ +≔

ldiv (H: group) (g h: H.1.1) : H.1.1 = (opGroup H) ((invGroup H) g) h rdiv (H: group) (g h: H.1.1) : H.1.1 - = (opGroup H) g ((invGroup H) h)

(Conjugation). -Let be a group, the conjugation of two elements of the group - is defined as .

conjugate (G: group) (g1 g2: G.1.1): G.1.1 - = rdiv G ((opGroup G) g1 g2) g1


SUBGROUPS

(Predicate). Type family - is a predicate iff - is a mere proposition for all . -

subtypeProp (A: U): U + = (opGroup H) g ((invGroup H) h)

(Conjugation). +Let be a group, the conjugation of two elements of the group + is defined as .

conjugate (G: group) (g1 g2: G.1.1): G.1.1 + = rdiv G ((opGroup G) g1 g2) g1


SUBGROUPS

(Predicate). Type family + is a predicate iff + is a mere proposition for all . +

subtypeProp (A: U): U = (P : A -> U) - * (a : A) -> isProp (P a)

(Subtype). -Let be a predicate. Then: -≔

subtype (A : U) (P : subtypeProp A): U + * (a : A) -> isProp (P a)

(Subtype). +Let be a predicate. Then: +≔

subtype (A : U) (P : subtypeProp A): U = (x : A) -- prop - * (P.1 x) -- level

(Subgroup). -Predicate is a subgroup iff -1) -2) and -3)

subgroupProp (G: group): U + * (P.1 x) -- level

(Subgroup). +Predicate is a subgroup iff +1) +2) and +3)

subgroupProp (G: group): U = (prop: G.1.1 -> U) * (level: (x: G.1.1) -> isProp (prop x)) * (ident: prop (idGroup G)) * (inv: (g: G.1.1) -> prop g -> prop ((invGroup G) g)) - * ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2))

(Normal Subgroup). -Subgroup is normal iff for every -it contains conjugate of .

isNormal (G: group) (P: subgroupProp G) : U + * ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2))

(Normal Subgroup). +Subgroup is normal iff for every +it contains conjugate of .

isNormal (G: group) (P: subgroupProp G) : U = (X: group) * (g1 g2: G.1.1) -> P.1 g2 -> P.1 (conjugate G g1 g2) normalSubgroupProp (G: group): U = (P: subgroupProp G) - * isNormal G P


KERNEL and IMAGE

(Kernel of Homomorphism). -≔

isGroupKer (G H: group) (f: G.1.1 -> H.1.1) (x: G.1.1): U - = Path H.1.1 (f x) (idGroup H)

(Image of Homomorphism). -≔

isGroupIm (G H: group) (f: G.1.1 -> H.1.1) (g: H.1.1): U - = propTrunc (fiber G.1.1 H.1.1 f g)

(Kernel of Homomorphism is subgroup).

kerProp (G H: group) (phi: grouphom G H) - : subgroupProp G

(Image of Homomorphism is subgroup).

imProp (G H: group) (phi: grouphom G H) - : subgroupProp H

(Set-Quotient). -Assume some type and relation - on it. -We define as following Higher Inductive Type: -≔

data setQuot (A: U) (R: A -> A -> U) + * isNormal G P


KERNEL and IMAGE

(Kernel of Homomorphism). +≔

isGroupKer (G H: group) (f: G.1.1 -> H.1.1) (x: G.1.1): U + = Path H.1.1 (f x) (idGroup H)

(Image of Homomorphism). +≔

isGroupIm (G H: group) (f: G.1.1 -> H.1.1) (g: H.1.1): U + = propTrunc (fiber G.1.1 H.1.1 f g)

(Kernel of Homomorphism is subgroup).

kerProp (G H: group) (phi: grouphom G H) + : subgroupProp G

(Image of Homomorphism is subgroup).

imProp (G H: group) (phi: grouphom G H) + : subgroupProp H

(Set-Quotient). +Assume some type and relation + on it. +We define as following Higher Inductive Type: +≔

data setQuot (A: U) (R: A -> A -> U) = quotient (a: A) | identification (a b: A) (r: R a b) <i>[ (i=0) -> quotient a, (i=1) -> quotient b ] | trunc (a b : setQuot A R) (p q : Path (setQuot A R) a b) <i j> [ (i = 0) -> p @ j , (i = 1) -> q @ j , - (j = 0) -> a , (j = 1) -> b ]

(Factor Group). -Let be a group and his normal subgroup. We define: -≔ -≔ -We can also define by relation . -If is normal subgroup then . + (j = 0) -> a , (j = 1) -> b ]

(Factor Group). +Let be a group and his normal subgroup. We define: +≔ +≔ +We can also define by relation . +If is normal subgroup then . This statement is proven in Lean.

factorProp (G : group) (P : normalSubgroupProp G) : G.1.1 -> G.1.1 -> U = \(x y : G.1.1) -> P.1.1 (rdiv G x y) factor (G : group) (P : normalSubgroupProp G) : U - = setQuot G.1.1 (factorProp G P)

(Factor group of dihedral group ). -As an test of factor group correctness we prove that , where and , -i. e. smallest nontrivial group.

def D₃.iso : Z₂ ≅ D₃\A₃

(Trivial homomorphism). -Trivial homomorphism between two groups (or monoids) and -maps every element of to identity element of :

trivmonoidhom (a b : monoid) : monoidhom a b + = setQuot G.1.1 (factorProp G P)

(Factor group of dihedral group ). +As an test of factor group correctness we prove that , where and , +i. e. smallest nontrivial group.

def D₃.iso : Z₂ ≅ D₃\A₃

(Trivial homomorphism). +Trivial homomorphism between two groups (or monoids) and +maps every element of to identity element of :

trivmonoidhom (a b : monoid) : monoidhom a b = (\(x : a.1.1) -> idMonoid b, \(x y : a.1.1) -> <i> (hasIdMonoid b).1 (idMonoid b) @ -i, <_> idMonoid b) trivabgrouphom (a b : abgroup) : abgrouphom a b - = trivmonoidhom (group' (abgroup' a)) (group' (abgroup' b))

(Chain complex). + = trivmonoidhom (group' (abgroup' a)) (group' (abgroup' b))

(Chain complex). Chain complex consists of: -1) Sequence of abelian groups . -2) Homomorphisms between these groups . -3) Requirement: the composition of two consecutive homomorphisms is trivial: -

chainComplex : U +1) Sequence of abelian groups . +2) Homomorphisms between these groups . +3) Requirement: the composition of two consecutive homomorphisms is trivial: +

chainComplex : U = (K : nat -> abgroup) * (hom : (n : nat) -> abgrouphom (K (succ n)) (K n)) * ((n : nat) -> Path (abgrouphom (K (succ2 n)) (K n)) (abgrouphomcomp (K (succ2 n)) (K (succ n)) (K n) (hom (succ n)) (hom n)) - (trivabgrouphom (K (succ2 n)) (K n)))

(Cycles). ≔

propZ (C : chainComplex) (n : nat) : subgroupProp (K' C (succ n)) + (trivabgrouphom (K (succ2 n)) (K n)))

(Cycles). ≔

propZ (C : chainComplex) (n : nat) : subgroupProp (K' C (succ n)) = kerProp (K' C (succ n)) (K' C n) (hom C n) -Z (C : chainComplex) (n : nat) : group = subgroup (K' C (succ n)) (propZ C n)

(Boundaries). ≔

B (C : chainComplex) (n : nat) : normalSubgroupProp (Z C n) +Z (C : chainComplex) (n : nat) : group = subgroup (K' C (succ n)) (propZ C n)

(Boundaries). ≔

B (C : chainComplex) (n : nat) : normalSubgroupProp (Z C n) = abelianSubgroupIsNormal (abelianSubgroupIsAbelian (K C (succ n)) (propZ C n)) (subgroupSubgroup (K' C (succ n)) - (imProp (K' C (succ (succ n))) (K' C (succ n)) (hom C (succ n))) (propZ C n))

(Homology Group). ≔

H (C : chainComplex) (n : nat) : group = factorGroup (Z C n) (B C n)

(First Group Isomorphism Theorem). Let and be groups, -and let be a homomorphism. Then: -1) The kernel of is normal subgroup of G. -2) The image of is a subgroup of . -3) The image of is isomorphic to the quotient group .


By composition of and we obtain -a path . -Therefore, contains every conjugation of


kernelIsNormalSubgroup (G H : group) (phi : grouphom G H) + (imProp (K' C (succ (succ n))) (K' C (succ n)) (hom C (succ n))) (propZ C n))

(Homology Group). ≔

H (C : chainComplex) (n : nat) : group = factorGroup (Z C n) (B C n)

(First Group Isomorphism Theorem). Let and be groups, +and let be a homomorphism. Then: +1) The kernel of is normal subgroup of G. +2) The image of is a subgroup of . +3) The image of is isomorphic to the quotient group .


By composition of and we obtain +a path . +Therefore, contains every conjugation of


kernelIsNormalSubgroup (G H : group) (phi : grouphom G H) : normalSubgroupProp G


\ No newline at end of file diff --git a/mathematics/analysis/set/index.html b/mathematics/analysis/set/index.html index 77ae69b4..52c23fc9 100644 --- a/mathematics/analysis/set/index.html +++ b/mathematics/analysis/set/index.html @@ -10,11 +10,11 @@ SET

Set Theory

Other disputed foundations for set theory could be taken as: ZFC, NBG, ETCS. We will disctinct syntetically: i) category theory; ii) set theory in univalent foundations; iii) topos theory, grothendieck topos, -elementary topos.

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition -if for all we have :

(0-type). A type A is a 0-type is for all - and we have .

(1-type). A type A is a 1-type if for all - and and , we have .

(A set of elements, ). -A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) +elementary topos.

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition +if for all we have :

(0-type). A type A is a 0-type is for all + and we have .

(1-type). A type A is a 1-type if for all + and and , we have .

(A set of elements, ). +A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U @@ -25,11 +25,11 @@ isSet (A: U): U = n_grpd A (S Z) PROP : U = (X:U) * isProp X -SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then +SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then path space between any sections is contractible.

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) (p q: Path (Pi A B) f g) - : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) - (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt + : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) + (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt unitRec (C: U) (x: C): unit -> C = split tt -> x -unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit +unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit
\ No newline at end of file diff --git a/mathematics/categories/category/index.html b/mathematics/categories/category/index.html index fe87eed1..645ca401 100644 --- a/mathematics/categories/category/index.html +++ b/mathematics/categories/category/index.html @@ -8,28 +8,28 @@ CATEGORY

category

Category package contains basic notion of categories, constructions and examples. -

Basics

Monoidal Structure

(Category Signature). The signature of category is -a where could be any universe. -The projection is called and projection is -called , where . +

Basics

Monoidal Structure

(Category Signature). The signature of category is +a where could be any universe. +The projection is called and projection is +called , where .

cat: U = (A: U) * (A -> A -> U) -

Precategory

Precategory defined as set of where - are objects defined by its arrows . +

Precategory

Precategory defined as set of where + are objects defined by its arrows . Properfies of left and right units included with composition c and its associativity. -

(Precategory). More formal, precategory consists of the following. -(i) A type , whose elements are called objects; -(ii) for each , a set , whose elements are called arrows or morphisms. -(iii) For each , a morphism , called the identity morphism. -(iv) For each , a function - -called composition, and denoted . -(v) For each and , - and . -(vi) For each and -, , , -. -

(Small Category). If for all the forms a Set, then +

(Precategory). More formal, precategory consists of the following. +(i) A type , whose elements are called objects; +(ii) for each , a set , whose elements are called arrows or morphisms. +(iii) For each , a morphism , called the identity morphism. +(iv) For each , a function + +called composition, and denoted . +(v) For each and , + and . +(vi) For each and +, , , +. +

(Small Category). If for all the forms a Set, then such category is called small category.

isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) @@ -41,25 +41,25 @@ Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h))) precategory: U = (C: cat) * isPrecategory C

Accessors of the precategory structure. -For is carrier and for is hom. +For is carrier and for is hom.

carrier (C: precategory): U = C.1.1 hom (C: precategory) (a b: carrier C): U = C.1.2 a b path (C: precategory) (x: carrier C): hom C x x = C.2.1 x compose (C: precategory) (x y z: carrier C) (f: hom C x y) (g: hom C y z): hom C x z = C.2.2.1 x y z f g -

(Co)-Terminal Objects

(Initial Object). Is such object , -that . -

(Terminal Object). Is such object , -that . +

(Co)-Terminal Objects

(Initial Object). Is such object , +that . +

(Terminal Object). Is such object , +that .

isInitial (C: precategory) (x: carrier C): U = (y: carrier C) -> isContr (hom C x y) isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) initial (C: precategory): U = (x: carrier C) * isInitial C x terminal (C: precategory): U = (y: carrier C) * isTerminal C y -

Functor

(Category Functor). Let and be precategories. -A functor consists of: (i) A function ; -(ii) for each , a function ; -(iii) for each , ; -(iv) for and and , . +

Functor

(Category Functor). Let and be precategories. +A functor consists of: (i) A function ; +(ii) for each , a function ; +(iii) for each , ; +(iv) for and and , .

catfunctor (A B: precategory): U = (ob: carrier A -> carrier B) * (mor: (x y: carrier A) -> hom A x y -> hom B (ob x) (ob y)) @@ -67,10 +67,10 @@ * ((x y z: carrier A) -> (f: hom A x y) -> (g: hom A y z) -> Path (hom B (ob x) (ob z)) (mor x z (compose A x y z f g)) (compose B (ob x) (ob y) (ob z) (mor x y f) (mor y z g))) -

Natural Transformation

(Natural Transformation). For functors , -a nagtural transformation consists of: -(i) for each , a morphism ; -(ii) for each and , . +

Natural Transformation

(Natural Transformation). For functors , +a nagtural transformation consists of: +(i) for each , a morphism ; +(ii) for each and , .

isNaturalTrans (C D: precategory) (F G: catfunctor C D) (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)): U @@ -82,17 +82,17 @@ ntrans (C D: precategory) (F G: catfunctor C D): U = (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)) * (isNaturalTrans C D F G eta) -

Kan Extensions

(Kan Extension). +

Kan Extensions

(Kan Extension).

extension (C C' D: precategory) (K: catfunctor C C') (G: catfunctor C D) : U = (F: catfunctor C' D) * (ntrans C D (compFunctor C C' D K F) G) -

Category Isomorphism

Definition (Category Isomorphism). A morphism is an iso -if there is a morphism such that - and -. "f is iso" is +

Category Isomorphism

Definition (Category Isomorphism). A morphism is an iso +if there is a morphism such that + and +. "f is iso" is a mere proposition. -

If A is a precategory and , -then (idtoiso).

iso (C: precategory) (A B: carrier C): U +

If A is a precategory and , +then (idtoiso).

iso (C: precategory) (A B: carrier C): U = (f: hom C A B) * (g: hom C B A) * (eta: Path (hom C A A) (compose C A B A f g) (path C A)) @@ -100,11 +100,11 @@

Rezk-completion

Definition (Category). A category is a precategory such that for all $a:Ob_C$, the $\Pi_{A:Ob_C} isContr \Sigma_{B:Ob_C} iso_C(A,B)$.

isCategory (C: precategory): U = (A: carrier C) -> isContr ((B: carrier C) * iso C A B) -category: U = (C: precategory) * isCategory C

Constructions

(Co)-Product of Categories

(Category Product). +category: U = (C: precategory) * isCategory C

Constructions

(Co)-Product of Categories

(Category Product).

Product (X Y: precategory) : precategory Coproduct (X Y: precategory) : precategory -

Opposite Category

(Opposite Category). The opposite category to category -is a category with same structure, except all arrows are inverted. +

Opposite Category

(Opposite Category). The opposite category to category +is a category with same structure, except all arrows are inverted.

opCat (P: precategory): precategory

(Co)-Slice Category

Definition (Slice Category).

Definition (Coslice Category). @@ -117,7 +117,7 @@ cosliceCat (C D: precategory) (a: carrier C) (F: catfunctor D C) : precategory -

Universal Mapping Property

(Universal Mapping Property). +

Universal Mapping Property

(Universal Mapping Property).

initArr (C D: precategory) (a: carrier C) (F: catfunctor D C): U = initial (cosliceCat C D a F) @@ -125,9 +125,9 @@ termArr (C D: precategory) (a: carrier (opCat C)) (F: catfunctor D (opCat C)): U = terminal (sliceCat C D a F) -

Unit Category

(Unit Category). In unit category both and . +

Unit Category

(Unit Category). In unit category both and .

unitCat: precategory -

Examples

Category of Sets

(Category of Sets). +

Examples

Category of Sets

(Category of Sets).

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = SET Hom (A B: Ob): U = A.1 -> B.1 @@ -139,7 +139,7 @@ Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = refl (Hom A D) (c A B D f (c B C D g h)) -

Category of Functions

(Category of Functions over Sets). +

Category of Functions

(Category of Functions over Sets).

Functions (X Y: U) (Z: isSet Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = X -> Y Hom (A B: Ob): U = id (X -> Y) @@ -150,7 +150,7 @@ R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined -

Category of Categories

(Category of Categories). +

Category of Categories

(Category of Categories).

Cat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = precategory Hom (A B: Ob): U = catfunctor A B @@ -161,7 +161,7 @@ R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D) : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined -

Category of Functors

(Category of Functors). +

Category of Functors

(Category of Functors).

Func (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = catfunctor X Y Hom (A B: Ob): U = ntrans X Y A B diff --git a/mathematics/categories/presheaf/index.html b/mathematics/categories/presheaf/index.html index 04bdb0b8..b7576bb6 100644 --- a/mathematics/categories/presheaf/index.html +++ b/mathematics/categories/presheaf/index.html @@ -12,97 +12,97 @@ Formal Set Topos. Presheaf model of type theory could be seen as generalization of the notion of Kripke model. -

INTRO

(Presheaf over ). -A presheaf over a category is a functor -from to the category of . -We denote as and as , -identity morphisms , -composition for , . -This means a presheaf is given by a family of sets -and restriction maps , for - satisfying the laws and for -. The family of sets is called right action.

By the nature of the rescription maps we could classify presheaves: +

INTRO

(Presheaf over ). +A presheaf over a category is a functor +from to the category of . +We denote as and as , +identity morphisms , +composition for , . +This means a presheaf is given by a family of sets +and restriction maps , for + satisfying the laws and for +. The family of sets is called right action.

By the nature of the rescription maps we could classify presheaves: i) if the restriction map forms a boundary operator (degeneracy map) -, such that +, such that then this is cohomology presheaf; ii) if the restriction map is a process action - then this is process presheaf; + then this is process presheaf; iii) if the restriction map actually restricts the domain the such presheaf is -called topological (default meaning).

(Yoneda presheaf ). -Any object of base category defines a -presheaf represented by . -This presheaf assigns to each object in -the set of arrows . Given anarrow -composition with f maps an arrow to an arrow . -In other words -then a set of maps and the restriction maps defined by composition.

(Seive). -A sieve on is a set of maps with codomain such that -is in whenever is in and .

(Subpresheaf ). -Subpresheaf of a presheaf A is a map , which -for each selects a subset of of shape defined by polyhedron A. - is a presheaf where is a set of decidable seives, -so that we can decide if is a member of . -

DEPENDENT TYPES

(Type). -A type is interpreted as a presheaf , a family of sets with restriction maps - for . A dependent type -B on A is interpreted by a presheaf on category of elements of : the objects -are pairs with and morphisms are -maps such that . A dependent type B is thus given -by a family of sets and restriction maps . -

We think of as a type and as a family of presheves varying . -The operation generalizes the semantics of +called topological (default meaning).

(Yoneda presheaf ). +Any object of base category defines a +presheaf represented by . +This presheaf assigns to each object in +the set of arrows . Given anarrow +composition with f maps an arrow to an arrow . +In other words +then a set of maps and the restriction maps defined by composition.

(Seive). +A sieve on is a set of maps with codomain such that +is in whenever is in and .

(Subpresheaf ). +Subpresheaf of a presheaf A is a map , which +for each selects a subset of of shape defined by polyhedron A. + is a presheaf where is a set of decidable seives, +so that we can decide if is a member of . +

DEPENDENT TYPES

(Type). +A type is interpreted as a presheaf , a family of sets with restriction maps + for . A dependent type +B on A is interpreted by a presheaf on category of elements of : the objects +are pairs with and morphisms are +maps such that . A dependent type B is thus given +by a family of sets and restriction maps . +

We think of as a type and as a family of presheves varying . +The operation generalizes the semantics of implication in a Kripke model. -

(Pi). An element is a family -of functions for such -that when and . -

(Sigma). The set is the set -of pairs when and restriction map . -

SIMPLICIAL TYPES

(Simplicial Types). +

(Pi). An element is a family +of functions for such +that when and . +

(Sigma). The set is the set +of pairs when and restriction map . +

SIMPLICIAL TYPES

(Simplicial Types). The simplicial type is defined as a presheaf on category of -finite linear posets and monotone maps. Let's write a presheaf -as . In a sense that this +finite linear posets and monotone maps. Let's write a presheaf +as . In a sense that this is a category on a shapes, the notion of subpolyhedras is then represented by subpresheaves. -

(). -The category of simplicial types denoted . -

CUBICAL TYPES

(Cubical Presheaf ). +

(). +The category of simplicial types denoted . +

CUBICAL TYPES

(Cubical Presheaf ). The identity types modeled with another presheaf, the presheaf on Lawvere category of distributive lattices (theory of de Morgan algebras) denoted -with . -

. The presheaf : -i) has to distinct global elements and (B); -ii) (I) has a decidable equality for each (B); -iii) is tiny so the path functor has right adjoint (B).; -iv) has meet and join (connections, B). -

NOTE: In the simplicial model B condition is underivable. -

(Cofibrations Subpresheaf ). -The subpresheaf corresponds to a map - so that can -be seen internally as the subpresheaf of propositions in - satisfying the property (which -reads ‘ is cofibrant’). In other words +with . +

. The presheaf : +i) has to distinct global elements and (B); +ii) (I) has a decidable equality for each (B); +iii) is tiny so the path functor has right adjoint (B).; +iv) has meet and join (connections, B). +

NOTE: In the simplicial model B condition is underivable. +

(Cofibrations Subpresheaf ). +The subpresheaf corresponds to a map + so that can +be seen internally as the subpresheaf of propositions in + satisfying the property (which +reads ‘ is cofibrant’). In other words classified cofibrant maps. -

: -i) cofibrant maps should contain isomorphisms and be closed under composition (A); -ii) is closed under disjunction: -(A). -

. This properties defined how we can mix the +

: +i) cofibrant maps should contain isomorphisms and be closed under composition (A); +ii) is closed under disjunction: +(A). +

. This properties defined how we can mix the contexts of depedent types and cubical types: -i) wedge (C); -ii) cofibrations (C). -

NOTE: B could be replaced with strengthened -C. -

: -i) — free monoidal category on interval ; -ii) — free monoidal category on interval with connections and ; -iii) — free symmetric monoidal category on interval; -iv) — free cartesian category on interval; -v) — free cartesian category on distributive lattice. -

NOTE: the cartesian cube category is the opposite of -the category of finite, strictly bipointed sets: . +i) wedge (C); +ii) cofibrations (C). +

NOTE: B could be replaced with strengthened +C. +

: +i) — free monoidal category on interval ; +ii) — free monoidal category on interval with connections and ; +iii) — free symmetric monoidal category on interval; +iv) — free cartesian category on interval; +v) — free cartesian category on distributive lattice. +

NOTE: the cartesian cube category is the opposite of +the category of finite, strictly bipointed sets: .

Theorem (Awodey). -The category of cubical types (presheaves on ) is the -classifying topos of strictly bipointed objects . Geometric -realisation preserves finite products. +The category of cubical types (presheaves on ) is the +classifying topos of strictly bipointed objects . Geometric +realisation preserves finite products.

SIMPLIFICATION

What if we take not a category as the underlying objects for sheaves diff --git a/mathematics/categories/topos/index.html b/mathematics/categories/topos/index.html index de0a4308..5435ae05 100644 --- a/mathematics/categories/topos/index.html +++ b/mathematics/categories/topos/index.html @@ -26,11 +26,11 @@ Myles Tierney. The main contribution is the reformulation of Grothendieck topology using subobject classifier.

Category Theory

First of all, a very simple category theory up to pullbacks is provided. We provide here -all definitions only to keep the context valid.

(Category Signature). The signature of category is -a where could be any universe. -The projection is called and projection is -called , where .

cat: U = (A: U) * (A -> A -> U)

Precategory defined as set of where -are objects defined by its arrows . +all definitions only to keep the context valid.

(Category Signature). The signature of category is +a where could be any universe. +The projection is called and projection is +called , where .

cat: U = (A: U) * (A -> A -> U)

Precategory defined as set of where +are objects defined by its arrows . Properfies of left and right units included with composition and its associativity.

isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) @@ -39,28 +39,28 @@ * (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f) * (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f) * ( (x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) -> - Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))

(Precategory). More formally, precategory consists of the following. -(i) A type , whose elements are called objects; -(ii) for each , a set , whose elements are called arrows or morphisms. -(iii) For each , a morphism , called the identity morphism. -(iv) For each , a function - -called composition, and denoted . -(v) For each and , - and . -(vi) For each and -, , , -.

carrier (C: precategory) : U + Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))

(Precategory). More formally, precategory consists of the following. +(i) A type , whose elements are called objects; +(ii) for each , a set , whose elements are called arrows or morphisms. +(iii) For each , a morphism , called the identity morphism. +(iv) For each , a function + +called composition, and denoted . +(v) For each and , + and . +(vi) For each and +, , , +.

carrier (C: precategory) : U hom (C: precategory) (a b: carrier C) : U compose (C: precategory) (x y z: carrier C) - (f: hom C x y) (g: hom C y z) : hom C x z

(Terminal Object). Is such object , -that .

isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) -terminal (C: precategory): U = (y: carrier C) * isTerminal C y

(Categorical Pullback). -The pullback of the cospan is a object with -morphisms , , such that -diagram commutes:

Pullback must be universal, meaning that for any -for which diagram also commutes there must exist a unique , -such that and .

homTo (C: precategory) (X: carrier C): U = (Y: carrier C) * hom C Y X + (f: hom C x y) (g: hom C y z) : hom C x z

(Terminal Object). Is such object , +that .

isTerminal (C: precategory) (y: carrier C): U = (x: carrier C) -> isContr (hom C x y) +terminal (C: precategory): U = (y: carrier C) * isTerminal C y

(Categorical Pullback). +The pullback of the cospan is a object with +morphisms , , such that +diagram commutes:

Pullback must be universal, meaning that for any +for which diagram also commutes there must exist a unique , +such that and .

homTo (C: precategory) (X: carrier C): U = (Y: carrier C) * hom C Y X cospan (C: precategory): U = (X: carrier C) * (_: homTo C X) * homTo C X hasCospanCone (C: precategory) (D: cospan C) (W: carrier C) : U @@ -81,11 +81,11 @@ = (h: cospanCone C D) -> isContr (cospanConeHom C D h E) hasPullback (C: precategory) (D: cospan C) : U = (E: cospanCone C D) * isPullback C D E -

Set Theory

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition -if for all we have :

(0-type). A type A is a 0-type is for all - and we have .

(1-type). A type A is a 1-type if for all - and and , we have .

(A set of elements, ). -A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) +

Set Theory

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition +if for all we have :

(0-type). A type A is a 0-type is for all + and we have .

(1-type). A type A is a 1-type if for all + and and , we have .

(A set of elements, ). +A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z | S (n: N) n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U @@ -96,15 +96,15 @@ isSet (A: U): U = n_grpd A (S Z) PROP : U = (X:U) * isProp X -SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then +SET : U = (X:U) * isSet X

(-Contractability). if fiber is set then path space between any sections is contractible.

setPi (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B) (p q: Path (Pi A B) f g) - : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) - (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt + : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A) + (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt unitRec (C: U) (x: C): unit -> C = split tt -> x -unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit

(Category of Sets, ). Sets forms a Category. +unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit

(Category of Sets, ). Sets forms a Category. All compositional theorems are proved using reflection rule of internal language. -The proof that forms a set is taken through -contractability.

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where +The proof that forms a set is taken through -contractability.

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where Ob: U = SET Hom (A B: Ob): U = A.1 -> B.1 id (A: Ob): Hom A A = idfun A.1 @@ -119,11 +119,11 @@ structure reformulated in a categorical way as a category of sheaves on a site or as one that has cartesian closure and subobject classifier. We provide two definitions here. -

Topological Structure

(Topology). The topological structure on -(or topology) is a subset with following properties: -i) any finite union of subsets of belongs to ; -ii) any finite intersection of subsets of belongs to . -Subets of are called open sets of family .

Here is a code snippet in Coq for this classical definition.

Structure topology (A : Type) := { +

Topological Structure

(Topology). The topological structure on +(or topology) is a subset with following properties: +i) any finite union of subsets of belongs to ; +ii) any finite intersection of subsets of belongs to . +Subets of are called open sets of family .

Here is a code snippet in Coq for this classical definition.

Structure topology (A : Type) := { open :> (A -> Prop) -> Prop; empty_open: open (empty _); full_open: open (full _); @@ -149,15 +149,15 @@ where topos is defined as category of sheaves on a Grothendieck site with geometric moriphisms as adjoint pairs of functors between topoi, that satisfy exactness properties.

As this flavour of topos theory uses category of sets as a prerequisite, -the formal construction of set topos is cricual in doing sheaf topos theory.

(Sieves). Sieves are a family of subfunctors

such that following axioms hold: i) (base change) If is covering -and is a morphism of , then the subfuntor

is covering for ; ii) (local character) Suppose that are -subfunctors and R is covering. If is covering for -all in , then is covering; iii) - is covering for all .

(Coverage). A coverage is a function assigning -to each the family of morphisms called -covering families, such that for any exist -a covering family such that -each composite factors some :

Co (C: precategory) (cod: carrier C) : U +the formal construction of set topos is cricual in doing sheaf topos theory.

(Sieves). Sieves are a family of subfunctors

such that following axioms hold: i) (base change) If is covering +and is a morphism of , then the subfuntor

is covering for ; ii) (local character) Suppose that are +subfunctors and R is covering. If is covering for +all in , then is covering; iii) + is covering for all .

(Coverage). A coverage is a function assigning +to each the family of morphisms called +covering families, such that for any exist +a covering family such that +each composite factors some :

Co (C: precategory) (cod: carrier C) : U = (dom: carrier C) * (hom C dom cod) @@ -169,55 +169,55 @@ = (cod: carrier C) * (fam: Delta C cod) * (coverings: carrier C -> Delta C cod -> U) - * (coverings cod fam)

(Grothendieck Topology). Suppose category has all pullbacks. -Since is small, a pretopology on consists of families of sets of -morphisms

called covering families, such that following axioms hold: -i) suppose that is a covering family -and that is a morphism of . -Then the collection is a cvering family for . -ii) If is covering, -and -is covering for all , then the family of composites

is covering; -iii) The family is covering for all .

(Site). Site is a category having either a coverage, + * (coverings cod fam)

(Grothendieck Topology). Suppose category has all pullbacks. +Since is small, a pretopology on consists of families of sets of +morphisms

called covering families, such that following axioms hold: +i) suppose that is a covering family +and that is a morphism of . +Then the collection is a cvering family for . +ii) If is covering, +and +is covering for all , then the family of composites

is covering; +iii) The family is covering for all .

(Site). Site is a category having either a coverage, grothendieck topology, or sieves.

site (C: precategory): U = (C: precategory) - * Coverage C

(Presheaf). Presheaf of a category + * Coverage C

(Presheaf). Presheaf of a category is a functor from opposite category to category of sets: -.

presheaf (C: precategory): U - = catfunctor (opCat C) Set

(Presheaf Category, ). -Presheaf category for a site is category +.

presheaf (C: precategory): U + = catfunctor (opCat C) Set

(Presheaf Category, ). +Presheaf category for a site is category were objects are presheaves and morphisms are natural transformations -of presheaf functors.

(Sheaf). Sheaf is a presheaf on a site. In other words -a presheaf such that the -cannonical map of inverse limit

is an isomorphism for each covering sieve . -Equivalently, all induced functions

should be bijections.

sheaf (C: precategory): U +of presheaf functors.

(Sheaf). Sheaf is a presheaf on a site. In other words +a presheaf such that the +cannonical map of inverse limit

is an isomorphism for each covering sieve . +Equivalently, all induced functions

should be bijections.

sheaf (C: precategory): U = (S: site C) - * presheaf S.1

(Sheaf Category, ). Sheaf category + * presheaf S.1

(Sheaf Category, ). Sheaf category is a category where objects are sheaves and morphisms are natural transformation of sheves. Sheaf category is a full subcategory -of category of presheaves .

(Grothendieck Topos). Topos is the category -of sheaves on a site with topology .

(Giraud). A category is a Grothiendieck topos if +of category of presheaves .

(Grothendieck Topos). Topos is the category +of sheaves on a site with topology .

(Giraud). A category is a Grothiendieck topos if it has following properties: i) has all finite limits; ii) has small disjoint coproducts stable under pullbacks; iii) any epimorphism is coequalizer; -iv) any equivalence relation is a kernel pair and has a quotient; -v) any coequalizer is stably exact; -vi) there is a set of objects that generates .

(Geometric Morphism). Suppose that and -are Grothendieck sites. A geometric morphism

consists of functors and - such that is -left adjoint to and preserves finite limits. The left adjoint is called -the inverse image functor, while is called the direct image. The inverse image functor - is left and right exact in the sense that it preserves all finite -colimits and limits, respectively.

(Point of a Topos). -A point of a topos is a geometric morphism: .

(Stalk). -The stalk at of an object is the image of under +iv) any equivalence relation is a kernel pair and has a quotient; +v) any coequalizer is stably exact; +vi) there is a set of objects that generates .

(Geometric Morphism). Suppose that and +are Grothendieck sites. A geometric morphism

consists of functors and + such that is +left adjoint to and preserves finite limits. The left adjoint is called +the inverse image functor, while is called the direct image. The inverse image functor + is left and right exact in the sense that it preserves all finite +colimits and limits, respectively.

(Point of a Topos). +A point of a topos is a geometric morphism: .

(Stalk). +The stalk at of an object is the image of under corresponding inverse image morphism -.

(Étale space é). -Let a topological space, a category and is a -valued presheaf on . -Then, the étalé space is a a pair É where: -i) É is a disjoin union of stalks of ; -ii) É is the canonical projection. +.

(Étale space é). +Let a topological space, a category and is a -valued presheaf on . +Then, the étalé space is a a pair É where: +i) É is a disjoin union of stalks of ; +ii) É is the canonical projection.

Elementary Topos

Giraud theorem was a synonymical topos definition that involved only topos properties but not site properties. That was a step forward in predicative definition. The other step was made by Lawvere and Tierney, @@ -231,15 +231,15 @@ theory is more suited for logic needs rather than for geometry, as its set properties are hidden under predicative pullback definition of subobject classifier rather than functorial notation of presheaf functor. So we can simplify proofs -at the homotopy levels, not to lift everything to 2-categorical model.

(Monomorphism). A morphism is a monic or mono -if for any object and every pair of parralel morphisms the

More abstractly, f is mono if for any the takes it to an injective -function between hom sets .

mono (P: precategory) (Y Z: carrier P) (f: hom P Y Z): U +at the homotopy levels, not to lift everything to 2-categorical model.

(Monomorphism). A morphism is a monic or mono +if for any object and every pair of parralel morphisms the

More abstractly, f is mono if for any the takes it to an injective +function between hom sets .

mono (P: precategory) (Y Z: carrier P) (f: hom P Y Z): U = (X: carrier P) (g1 g2: hom P X Y) -> Path (hom P X Z) (compose P X Y Z g1 f) (compose P X Y Z g2 f) - -> Path (hom P X Y) g1 g2

(Subobject Classifier). In category with finite limits, -a subobject classifier is a monomorphism out of terminal -object , such that for any mono there is a unique -morphism and a pullback diagram:

subobjectClassifier (C: precategory): U + -> Path (hom P X Y) g1 g2

(Subobject Classifier). In category with finite limits, +a subobject classifier is a monomorphism out of terminal +object , such that for any mono there is a unique +morphism and a pullback diagram:

subobjectClassifier (C: precategory): U = (omega: carrier C) * (end: terminal C) * (trueHom: hom C end.1 omega) @@ -249,21 +249,21 @@ * ((V X: carrier C) (j: hom C V X) (k: hom C X omega) -> mono C V X j -> hasPullback C (omega,(end.1,trueHom),(X,k)) - -> Path (hom C X omega) (chi V X j) k)

(Category of Sets has Subobject Classifier).

(Cartesian Closed Categories). -The category is called cartesian closed if exists all: + -> Path (hom C X omega) (chi V X j) k)

(Category of Sets has Subobject Classifier).

(Cartesian Closed Categories). +The category is called cartesian closed if exists all: i) terminals; ii) products; iii) exponentials. Note that this definition -lacks beta and eta rules which could be found in embedding .

isCCC (C: precategory): U +lacks beta and eta rules which could be found in embedding .

isCCC (C: precategory): U = (Exp: (A B: carrier C) -> carrier C) * (Prod: (A B: carrier C) -> carrier C) * (Apply: (A B: carrier C) -> hom C (Prod (Exp A B) A) B) * (P1: (A B: carrier C) -> hom C (Prod A B) A) * (P2: (A B: carrier C) -> hom C (Prod A B) B) * (Term: terminal C) - * unit

(Category of Sets has Cartesian Closure). As you can see -from exp and pro we internalize and types as instances, -the predicates are provided with contractability. -Exitense of terminals is proved by . The same technique you -can find in embedding.

cartesianClosure : isCCC Set + * unit

(Category of Sets has Cartesian Closure). As you can see +from exp and pro we internalize and types as instances, +the predicates are provided with contractability. +Exitense of terminals is proved by . The same technique you +can find in embedding.

cartesianClosure : isCCC Set = (expo,prod,appli,proj1,proj2,term,tt) where exp (A B: SET): SET = (A.1 -> B.1, setFun A.1 B.1 B.2) pro (A B: SET): SET = (prod A.1 B.1, @@ -277,12 +277,12 @@ unitContr (x: SET) (f: x.1 -> unit) : isContr (x.1 -> unit) = (f, \(z: x.1 -> unit) -> propPi x.1 (\(_:x.1)->unit) (\(x:x.1) ->propUnit) f z) term: terminal Set = ((unit,setUnit),\(x: SET) -> unitContr x (\(z: x.1) -> tt))

Note that rules of cartesian closure form a type theoretical language -called lambda calculus.

elementary Topos). Topos is a precategory which is +called lambda calculus.

elementary Topos). Topos is a precategory which is cartesian closed and has subobject classifier.

Topos (cat: precategory) : U = (cartesianClosure: isCCC cat) - * subobjectClassifier cat

(Topos Definitions). Any Grothendieck topos is an elementary topos too. -The proof is sligthly based on results of Giraud theorem.

(Category of Sets forms a Topos). There is a + * subobjectClassifier cat

(Topos Definitions). Any Grothendieck topos is an elementary topos too. +The proof is sligthly based on results of Giraud theorem.

(Category of Sets forms a Topos). There is a cartesian closure and subobject classifier for a categoty of sets.

internal : Topos Set = (cartesianClosure,hasSubobject)

Literature

[70]. P.T. Johnstone. Topos Theory. 2014, diff --git a/mathematics/geometry/bundle/index.html b/mathematics/geometry/bundle/index.html index 65d02966..8bd85bcb 100644 --- a/mathematics/geometry/bundle/index.html +++ b/mathematics/geometry/bundle/index.html @@ -11,31 +11,31 @@ Bundle package contains basic information about fibers (needed for weak-equivalence) and fiber bundles, constructions from algebraic topology. -

Fiber

(Fiber). The fiber of the map in a point -is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U +

Fiber

(Fiber). The fiber of the map in a point +is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U = (x: E) * Path B y (p x) -

Fiber Bundle

(Fiber Bundle). The fiber bundle on a -total space with fiber layer and base is a -structure where is a surjective +

Fiber Bundle

(Fiber Bundle). The fiber bundle on a +total space with fiber layer and base is a +structure where is a surjective map with following property: -for any point exists a neighborhood for which a -homeomorphism -making the following diagram commute.

-

Trivial Fiber Bundle

(Trivial Fiber Bundle). -When total space is cartesian product -and then such bundle is called trivial .

Family (B: U): U = B -> U +for any point exists a neighborhood for which a +homeomorphism +making the following diagram commute.

+

Trivial Fiber Bundle

(Trivial Fiber Bundle). +When total space is cartesian product +and then such bundle is called trivial .

Family (B: U): U = B -> U total (B: U) (F: Family B): U = Sigma B F trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1 homeo (B E: U) (F: Family B) (p: E -> B) (y: B) : fiber E B p y -> total B F -

Fiber is a Dependent Family

(Fiber in a trivial total space is a family over base). -Inverse image (fiber) of fiber bundle in point equals . +

Fiber is a Dependent Family

(Fiber in a trivial total space is a family over base). +Inverse image (fiber) of fiber bundle in point equals . Thre proof sketch is following:

F y = (_: isContr B) * (F y) = (x y: B) * (_: Path B x y) * (F y) = (z: B) * (k: F z) * Path B z y = (z: E) * Path B z.1 y - = fiber (total B F) B (trivial B F) y

The equality is proven by lemma and functions.

encode (B: U) (F: B -> U) (y: B) + = fiber (total B F) B (trivial B F) y

The equality is proven by lemma and functions.

encode (B: U) (F: B -> U) (y: B) : fiber (total B F) B (trivial B F) y -> F y = \ (x: fiber (total B F) B (trivial B F) y) -> subst B F x.1.1 y (<i>x.2@-i) x.1.2 @@ -61,6 +61,6 @@ g: A -> T = decode B F y s (x: A): Path A (f (g x)) x = lem2 B F y x t (x: T): Path T (g (f x)) x = lem3 B F y x -

G-structure

The structure group of an -fiber bundle is just , -the loop space of . +

G-structure

The structure group of an -fiber bundle is just , +the loop space of .

\ No newline at end of file diff --git a/mathematics/geometry/derham/index.html b/mathematics/geometry/derham/index.html index 266499fa..1f3034a3 100644 --- a/mathematics/geometry/derham/index.html +++ b/mathematics/geometry/derham/index.html @@ -7,53 +7,53 @@ use[data-c]{stroke-width:3px} DE RHAM

DE RHAM

(Cohesive -Topos). -An -Topos which is local and -connected is called cohesive. +DERHAM

DE RHAM

(Cohesive -Topos). +An -Topos which is local and -connected is called cohesive. Here is very short intro to de Rham cohesion built on -top of and modalities. -

(Cohesive -Topos). -An -Topos which is local and -connected is called cohesive. -

(de Rham shape modality). +top of and modalities. +

(Cohesive -Topos). +An -Topos which is local and -connected is called cohesive. +

(de Rham shape modality). de Rham cohesive homotopy type of A is defined as a homotopy cofiber of the unit of the shape modality: -

+

or the (looping opetaion of) the cokernel of the unit of the shape modality. It is also called de Rham shape modality. -

-

(de Rham flat modality). +

+

(de Rham flat modality). de Rham complex with coefficients in A is defined as the homotopy fiber of the counit of the flat modality: -

+

or the (delooping opetaion of) the cokernel of the unit of the shape modality. It is also called de Rham flat modality. -

-

The object A is called de Rham coefficient object of . -

(Loop Space Object). -Loop space objects are defined in any -category -with homotopy pullbacks: for any pointed object of -with point , its loop space object is the homotopy pullback - of this point along itself: -

-

(Delooping). -if is given and a homotopy pullback diagram -

-

exists, with the point -being essentially unique, by the above has been -realized as the loop space object of . - is called delooping of X: -

-

(Milnor–Lurie). +

+

The object A is called de Rham coefficient object of . +

(Loop Space Object). +Loop space objects are defined in any -category +with homotopy pullbacks: for any pointed object of +with point , its loop space object is the homotopy pullback + of this point along itself: +

+

(Delooping). +if is given and a homotopy pullback diagram +

+

exists, with the point +being essentially unique, by the above has been +realized as the loop space object of . + is called delooping of X: +

+

(Milnor–Lurie). There is an adjoint functor -

-

between -groups of and uniquely pointed -connected objects in which are doneted . -Where is a looping and is a delooping operations. -

(Maurer-Cartan form). -For and -group in the cohesive --topos Maurer-Cartan form is defines as -

-

for the -valued de Rham cocycle on induced by pullback pasting: -

+

+

between -groups of and uniquely pointed +connected objects in which are doneted . +Where is a looping and is a delooping operations. +

(Maurer-Cartan form). +For and -group in the cohesive +-topos Maurer-Cartan form is defines as +

+

for the -valued de Rham cocycle on induced by pullback pasting: +

LITERATURE

[1]. Urs Schreiber. Differential cohomology in a cohesive ∞-topos

\ No newline at end of file diff --git a/mathematics/homotopy/cw/index.html b/mathematics/homotopy/cw/index.html index b289eb83..555e06ed 100644 --- a/mathematics/homotopy/cw/index.html +++ b/mathematics/homotopy/cw/index.html @@ -17,22 +17,22 @@ higher inductive types could be described as CW-complexes. Defining HIT means to define some CW-complex directly using cubical homogeneous composition structure as an -element of initial algebra inside cubical model.

(HIT). With a given context variables +element of initial algebra inside cubical model.

(HIT). With a given context variables Δ,K ⊢ (Γ,Ξ,Ψ,𝜑,𝑒) and telescope (𝛿 : Δ) (𝑖 : 𝕀) (𝜑 : 𝔽) (𝑢₀: H 𝛿 [𝜑 ↦ 𝑢[0/𝑖]]) every HIT is defines as: 1) ctorⁱ (𝛾: Γⁱ [𝛿]) (𝑥: Ξⁱ [𝛿,𝛾] → H 𝛿) (s: Ψₓ) : H 𝛿 [𝜑ₛ ↦ 𝑒[𝛾,𝑥]]; 2) hcompⁱ [𝜑 ↦ 𝑢] 𝑢₀ : H 𝛿 [𝜑 ↦ 𝑢[1/𝑖]]; -3) transpⁱ 𝜑 𝑢₀ : H 𝛿 [1] [𝜑 ↦ 𝑢₀].

. One of the notables is pushout as it's used +3) transpⁱ 𝜑 𝑢₀ : H 𝛿 [1] [𝜑 ↦ 𝑢₀].

. One of the notables is pushout as it's used to define the cell attachment formally, as others cofibrant objects.

data pushout (A B C: U) (f: C -> A) (g: C -> B) = po1 (_: A) | po2 (_: B) | po3 (c: C) <i> [ (i = 0) -> po1 (f c) , - (i = 1) -> po2 (g c) ]

. Here are some examples of using + (i = 1) -> po2 (g c) ]

. Here are some examples of using dimensions to construct spherical shapes.

data S1 = base | loop <i> [ (i = 0) -> base, (i = 1) -> base ]
data S2 = point | surf <i j> [ (i = 0) -> point, (i = 1) -> point, (j = 0) -> point, (j = 1) -> point ]
data D3 (x: S2) = border (x: S2) | space <i j k> [ ( i = 0) -> border x, (i = 1) -> border x , ( j = 0) -> border x, (j = 1) -> border x , - ( k = 0) -> border x, (k = 1) -> border x ]

. Structure of same as of . ASCII proof + ( k = 0) -> border x, (k = 1) -> border x ]

. Structure of same as of . ASCII proof that comp parameters are the same as in surf constructor:

I2 (A: U) (a0 a1 b0 b1: A) (u: Path A a0 a1) (v: Path A b0 b1) (r0: Path A a0 b0) (r1: Path A a1 b1) : U = PathP (<i> (PathP (<j> A) (u@i) (v@i))) r0 r1 @@ -52,25 +52,25 @@ This decomposition is intended to solve the problem of interpretation of higher inductive types with parameters.

MATHEMATICS

In definition of homotopy groups, a special role belongs -to inclusions . We study spaces -obtained through iterated attachments of along . -

(Attachment). Attaching n-cell to a space -along a map means taking a pushout -

-

where the notation means that the result depends -on homotopy class of . -

(CW-Complex). Inductively. The only -CW-complex of dimention is . -A CW-complex of dimension on is a -space obtained by attaching a collection of n-cells -to a CW-complex of dimension . -

A CW-complex is a space which is the colimit(X_i) of a -sequence of -CW-complexes of dimension , with -obtained from by i-cell attachments. +to inclusions . We study spaces +obtained through iterated attachments of along . +

(Attachment). Attaching n-cell to a space +along a map means taking a pushout +

+

where the notation means that the result depends +on homotopy class of . +

(CW-Complex). Inductively. The only +CW-complex of dimention is . +A CW-complex of dimension on is a +space obtained by attaching a collection of n-cells +to a CW-complex of dimension . +

A CW-complex is a space which is the colimit(X_i) of a +sequence of +CW-complexes of dimension , with +obtained from by i-cell attachments. Thus if X is a CW-complex, it comes with a filtration - -where is a CW-complex of dimension called + +where is a CW-complex of dimension called the i-skeleton, and hence the filtration is called the skeletal filtration.

\ No newline at end of file diff --git a/mathematics/homotopy/hopf/index.html b/mathematics/homotopy/hopf/index.html index e615b577..06346e1b 100644 --- a/mathematics/homotopy/hopf/index.html +++ b/mathematics/homotopy/hopf/index.html @@ -6,28 +6,28 @@ .mjx-dotted{stroke-linecap:round;stroke-dasharray:0,140} use[data-c]{stroke-width:3px} HOPF

Hopf Fibrations

The geometric and topological interpretation

HOPF

This article defines the Hopf Fibration (HF), the concept -of splitting the sphere onto the twisted cartesian product -of spheres and . +of splitting the sphere onto the twisted cartesian product +of spheres and . Basic HF applications are: 1) HF is a Fiber Bundle structure of Dirac Monopole; -2) HF is a map from the in H to the Bloch sphere; -3) If HF is a vector field in then there exists a solution +2) HF is a map from the in H to the Bloch sphere; +3) If HF is a vector field in then there exists a solution to compressible non-viscous Navier-Stokes equations. It was figured out that there are only 4 dimensions of fibers with Hopf invariant 1, namely -, , , .

This article consists of two parts: -1) geometric visualization of projection of to (frontend); +, , , .

This article consists of two parts: +1) geometric visualization of projection of to (frontend); 2) formal topological version of HF in cubical type theory (backend). Consider this a basic intro and a summary of results or companion guide to the chapter 8.5 from HoTT. -

Geometry

Let’s imagine as smooth differentiable manifold and build +

Geometry

Let’s imagine as smooth differentiable manifold and build a projection onto the display as if demoscene is still alive. -

Equations

Definition (Sphere ). Like a little baby in :after math classes in quaternions : -

Definition (Locus). The is realized as a disjoint -union of circular fibers in Hopf coordinates , -where and :

Definition (Mapping on ). -A mapping of the Locus to the has points on the circles -parametrized by :

Code in three.js:

var fiber = new THREE.Curve(), +

Equations

Definition (Sphere ). Like a little baby in :after math classes in quaternions : +

Definition (Locus). The is realized as a disjoint +union of circular fibers in Hopf coordinates , +where and :

Definition (Mapping on ). +A mapping of the Locus to the has points on the circles +parametrized by :

Code in three.js:

var fiber = new THREE.Curve(), color = sphericalCoords.color; fiber.getPoint = function(t) { @@ -44,49 +44,49 @@ };

Topology

Can we reason about spheres without a metric? Yes! But can we do this in a constructive way? Also yes. -

Fiber

Definition (Fiber). The fiber of the map in a point -is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U +

Fiber

Definition (Fiber). The fiber of the map in a point +is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U = (x: E) * Path B y (p x) -

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle on a -total space with fiber layer and base is a -structure where is a surjective +

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle on a +total space with fiber layer and base is a +structure where is a surjective map with following property: -for any point exists a neighborhood for which a -homeomorphism +for any point exists a neighborhood for which a +homeomorphism making the following diagram commute. - +

Trivial Fiber Bundle

Definition (Trivial Fiber Bundle). -When total space is cartesian product -and then such bundle is called trivial .

Family (B: U): U = B -> U +When total space is cartesian product +and then such bundle is called trivial .

Family (B: U): U = B -> U total (B: U) (F: Family B): U = Sigma B F trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1

Theorem (Fiber Bundle is a Type Family). -Inverse image (fiber) of fiber bundle in point equals .

FiberPi (B: U) (F: B -> U) (y: B) +Inverse image (fiber) of fiber bundle in point equals .

FiberPi (B: U) (F: B -> U) (y: B) : Path U (fiber (total B F) B (trivial B F) y) (F y)

Definition (Structure Group). The structure group of -an -fiber bundle is just Aut(F), the loop space of BAut(F). -

Higher Spheres

Definition (2-points, Bool, Sphere ).

data bool = false | true +an -fiber bundle is just Aut(F), the loop space of BAut(F). +

Higher Spheres

Definition (2-points, Bool, Sphere ).

data bool = false | true

Definition (Suspension).

data susp (A: U) = north | south | merid (a: A) <i> [ (i = 0) -> north, - (i = 1) -> south ]

Definition (Sphere ). Direct definition.

data S1 + (i = 1) -> south ]

Definition (Sphere ). Direct definition.

data S1 = base | loop <i> [ (i = 0) -> base, (i = 1) -> base ] -

Definition (Sphere ). Recursive definition.

S: nat -> U = split +

Definition (Sphere ). Recursive definition.

S: nat -> U = split zero -> bool succ x -> susp (S x) S2: U = susp S1 S3: U = susp S2 S4: U = susp S3 -

Hopf Fibrations

Theorem (Hopf Fibrations). There are fiber bundles:

Definition (H-space). H-space over a carrier is a tuple.

Example ( Hopf Fiber ). Mobius fiber. +

Hopf Fibrations

Theorem (Hopf Fibrations). There are fiber bundles:

Definition (H-space). H-space over a carrier is a tuple.

Example ( Hopf Fiber ). Mobius fiber. In cubicaltt type checker.

moebius : S1 -> U = split base -> bool loop @ i -> ua bool bool negBoolEquiv @ i -H0 : U = (c : S1) * moebius c

Example ( Hopf Fiber ). Guillaume Brunerie. +H0 : U = (c : S1) * moebius c

Example ( Hopf Fiber ). Guillaume Brunerie. In cubicaltt type checker.

rot: (x : S1) -> Path S1 x x = split base -> loop1 loop @ i -> constSquare S1 base loop1 @ i @@ -101,7 +101,7 @@ south -> S1 merid x @ i -> ua S1 S1 (mu x) @ i -total : U = (c : S2) * H c

Example ( Hopf Fiber ). By Egbert Rijke and Ulrik Buchholtz. +total : U = (c : S2) * H c

Example ( Hopf Fiber ). By Egbert Rijke and Ulrik Buchholtz. In Lean prover.

definition pfiber_quaternionic_phopf : pfiber quaternionic_phopf ≃* S* 3 := begin @@ -113,13 +113,13 @@ refine fiber.equiv_precompose _ (hopf.total (S 3))− 1 e _ ·e _, apply fiber_pr1 }, { reflexivity } -end

Definition (Hopf Invariant). Let a continuous map. -Then homotopy pushout (cofiber) of is has -ordinary cohomologyHence for generators of the cohomology groups in -degree and , respectively, there exists an integer -that expresses the cup product square of -as a multiple of — . -This integer is called Hopf invariant of .

Theorem (Adams, Atiyah). Hopf Fibrations are only -maps that have Hopf invariant . +end

Definition (Hopf Invariant). Let a continuous map. +Then homotopy pushout (cofiber) of is has +ordinary cohomologyHence for generators of the cohomology groups in +degree and , respectively, there exists an integer +that expresses the cup product square of +as a multiple of — . +This integer is called Hopf invariant of .

Theorem (Adams, Atiyah). Hopf Fibrations are only +maps that have Hopf invariant .

Literature

[1]. Ulrik Buchholtz, Egbert Rijke. The Cayley-Dickson Construction in Homotopy Type Theory


\ No newline at end of file diff --git a/mathematics/homotopy/pullback/index.html b/mathematics/homotopy/pullback/index.html index 05282bad..b757caa4 100644 --- a/mathematics/homotopy/pullback/index.html +++ b/mathematics/homotopy/pullback/index.html @@ -9,10 +9,10 @@ LIB LIMIT

PULLBACK

Pullback package contains basic information about Homotopy Limits known as Pullbacks. -

Definitions

(Homotopy Pullback). -The pullback of the first diagram (which is called cospan)

is a -together with the projection maps making the second -diagram commute up to homotopy .

pullback (A B C:U) (f: A -> C) (g: B -> C): U +

Definitions

(Homotopy Pullback). +The pullback of the first diagram (which is called cospan)

is a +together with the projection maps making the second +diagram commute up to homotopy .

pullback (A B C:U) (f: A -> C) (g: B -> C): U = (a: A) * (b: B) * Path C (f a) (g b) pb1 (A B C: U) (f: A -> C) (g: B -> C) @@ -22,11 +22,11 @@ pb3 (A B C: U) (f: A -> C) (g: B -> C) : (x: pullback A B C f g) -> Path C (f x.1) (g x.2.1) = \(x: pullback A B C f g) -> x.2.2 -

> (Homotopy Pullback Square). A homotopy pullback or cospan +

> (Homotopy Pullback Square). A homotopy pullback or cospan is called a homotopy pullback square if there exists a homotopy -equivalence satisfying - -and . Map is called induced map.

induced (Z A B C: U) (f: A -> C) (g: B -> C) +equivalence satisfying + +and . Map is called induced map.

induced (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B) (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)) : Z -> pullback A B C f g @@ -38,7 +38,7 @@ isPullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B) (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)): U - = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

(Existence of Pullback Square). + = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

(Existence of Pullback Square). Pullback Square exists and equals Pullback, where induced map is identity. Given as 2.11 Exercise in HoTT Chapter 2.

completePullback (A B C: U) (f: A -> C) (g: B -> C) : pullbackSq (pullback A B C f g) A B C f g (pb1 A B C f g) (pb2 A B C f g) diff --git a/mathematics/homotopy/pushout/index.html b/mathematics/homotopy/pushout/index.html index 57f8d93a..c7a13ed2 100644 --- a/mathematics/homotopy/pushout/index.html +++ b/mathematics/homotopy/pushout/index.html @@ -7,23 +7,23 @@ use[data-c]{stroke-width:3px} PUSHOUT

PUSHOUT

(Span). -The two maps with the same domain are called span:

(Homotopy Pushout). -The homotopy pushout or homotopy colimit (denoted as ) -of the span diagram:

where is an equivalence relation and -for . If is a based space with basepoint , we -add the relation for all .

data pushout (A B C: U) (f: C -> A) (g: C -> B) +COLIMIT

PUSHOUT

(Span). +The two maps with the same domain are called span:

(Homotopy Pushout). +The homotopy pushout or homotopy colimit (denoted as ) +of the span diagram:

where is an equivalence relation and +for . If is a based space with basepoint , we +add the relation for all .

data pushout (A B C: U) (f: C -> A) (g: C -> B) = po1 (_: A) | po2 (_: B) | po3 (c: C) <i> [ (i = 0) -> po1 (f c) , - (i = 1) -> po2 (g c) ]

EXAMPLES

(Homotopy Fibers).

hofiber (A B: U) (f: A -> B) (y: B): U + (i = 1) -> po2 (g c) ]

EXAMPLES

(Homotopy Fibers).

hofiber (A B: U) (f: A -> B) (y: B): U = pullback A unit B f (\(x: unit) -> y) -

(Fiber Pullback).

fiberPullback (A B: U) (f: A -> B) (y: B) +

(Fiber Pullback).

fiberPullback (A B: U) (f: A -> B) (y: B) : pullbackSq (hofiber A B f y) -

(Homotopy Cofiber).

cofiber (A B: U) (f: B -> A): U +

(Homotopy Cofiber).

cofiber (A B: U) (f: B -> A): U = pushout A unit B f (\(x: B) -> tt) -

(Kernel).

kernel (A B: U) (f: A -> B): U +

(Kernel).

kernel (A B: U) (f: A -> B): U = pullback A A B f f -

(Cokernel).

cokernel (A B: U) (f: B -> A): U +

(Cokernel).

cokernel (A B: U) (f: B -> A): U = pushout A A B f f

LITERATURE

[1]. Brian Munson and Ismar Volić. Cubical Homotopy Theory

\ No newline at end of file diff --git a/spec/index.html b/spec/index.html index 3dbb154f..c5f6458b 100644 --- a/spec/index.html +++ b/spec/index.html @@ -7,20 +7,20 @@ use[data-c]{stroke-width:3px} SPECIFICATION

BINARY FORMAT

Here is given a preliminary specification on Anders external term format.

is a byte.
- (from qword) is a 64-bit little-endian integer constisting of 4 bytes.
- is a UTF-8 string encoded as its length followed by the string itself. - In a BNF-like notation this written as
- represents here string (given by Z.to_bits function) that encodes Zarith integer.
- is a ident, - where first part represents ignored variable (like in ).
- represents interval elements ( and respectively).
- is a face.
- is a language expression.
- is a cubical system. -

COSMOS

-

ΠΣ

-

INTERVAL

-

KAN

+SPEC

BINARY FORMAT

Here is given a preliminary specification on Anders external term format.

is a byte.
+ (from qword) is a 64-bit little-endian integer constisting of 4 bytes.
+ is a UTF-8 string encoded as its length followed by the string itself. + In a BNF-like notation this written as
+ represents here string (given by Z.to_bits function) that encodes Zarith integer.
+ is a ident, + where first part represents ignored variable (like in ).
+ represents interval elements ( and respectively).
+ is a face.
+ is a language expression.
+ is a cubical system. +

COSMOS

+

ΠΣ

+

INTERVAL

+

KAN

\ No newline at end of file