| Вопрос про 2-категории |
[01 Jun 2018|08:01pm] |
Начал кодировать (инфинити,1)-категории и сразу же столкнулся с проблемой кодировкаи Hom функтора 3-категории. Кроме категории естественный преобрзований, где морфизмы — это так называемые модификации (следующий уровень после естественных преобразований), надо в 3-категории включить информацию о предыдущих категориях, для предыдущей 2-категории — это объекты двух видов: 1) категории в категории категории; 2) функторы в категории функторов.
Я посмотрел на правила вертикальной и горизонтальной композиции, которые включены уже в категорию категорий и категорию функторов, и мне кажется, что существует изоморфизм между, с одной стороны — декартовым произведением двух категорий: категорией категорий и категорией функторов, и с другой стороны — 2-категорией. Вопрос, так ли это, и если да, то существует ли где-то такая теорема?
Продублировал вопрос тут: https://dxdy.ru/topic127434.html (с более сильной теоремой про бикатегории, которые в сущности более слабые версии 2-категорий).
|
|
| MONADS NEED NOT BE ENDOFUNCTORS |
[12 Aug 2016|09:57pm] |
We will elsewhere comment on the relation of our relative monads to the recent gen- eralization of monads by Spivey [31] that was also motivated by programming examples: he fixes a functor K ∈ C → J (notice the direction) to then look for monad-like structures with an underlying functor J → C. With Paul Levy we have checked that a fair amount of monad theory transfers to his generalized monads, but they are not monoids in [J, C] unless K has a left adjoint, in which case they are equivalent to relative monads. Sam Staton has considered an enriched variant of relative monads.
http://jmchapman.github.io/papers/relmon-lmcs.pdf
|
|
| Duality Theory and Categorical Universal Logic: With Emphasis on Quantum Structures |
[01 Apr 2016|04:55am] |
Yoshihiro Maruyam
Categorical Universal Logic is a theory of monad-relativised hyperdoctrines (or fibred universal al- gebras), which in particular encompasses categorical forms of both first-order and higher-order quan- tum logics as well as classical, intuitionistic, and diverse substructural logics. Here we show there are those dual adjunctions that have inherent hyperdoctrine structures in their predicate functor parts. We systematically investigate into the categorical logics of dual adjunctions by utilising Johnstone- Dimov-Tholen’s duality-theoretic framework. Our set-theoretical duality-based hyperdoctrines for quantum logic have both universal and existential quantifiers (and higher-order structures), giving rise to a universe of Takeuti-Ozawa’s quantum sets via the tripos-to-topos construction by Hyland- Johnstone-Pitts. The set-theoretical hyperdoctrinal models of quantum logic, as well as all quantum hyperdoctrines with cartesian base categories, turn out to give sound and complete semantics for Faggian-Sambin’s first-order quantum sequent calculus over cartesian type theory; in addition, quan- tum hyperdoctrines with monoidal base categories are sound and complete for the calculus over linear type theory. We finally consider how to reconcile Birkhoff-von Neumann’s quantum logic and Abramsky-Coecke’s categorical quantum mechanics (which is modernised quantum logic as an antithesis to the traditional one) via categorical universal logic.
http://arxiv.org/pdf/1412.8526.pdf
|
|
| Техническое |
[28 Mar 2016|09:10pm] |
В это сообщество больше не пишу, поскольку оба модератора мудаки. Остаток учебника скоро выложу у себя в журнале и ещё здесь
http://dxdy.ru/
|
|
| A van Kampen theorem for toposes |
[21 Feb 2016|01:52pm] |
Упорядочивал библиотеку и наткнулся, наверное, на любопытное.
A van Kampen theorem for toposes
Marta Bunge and Stephen Lack
http://maths.mq.edu.au/~slack/papers/vkt.html
In this paper we introduce the notion of an extensive 2-category, to be thought of as "2-category of generalized spaces".
We consider and extensive 2-category K equipped with a binary-product-preserving pseudofunctor C : K_op → Cat, which we think of as specifying the "coverings" of the generalized spaces.
We prove, in this context, a van Kampen theorem which generalizes and refines one of Brown and Janelidze.
The local properties required in this theorem are stated in terms of morphism of effective descent for the pseudofunctor C.
We specialize the general van Kampen theorem to the 2-category Top_S of toposes bounded over an elementary topos S, and to its full sub-2-category LTop_S determined by the locally connected toposes, after showing both of these 2-categories to be extensive.
We then consider three particular notions of coverings on toposes corresponding respectively to local homeomorphisms, covering projections, and unramified morphisms;
in each case we deduce a suitable version of a van Kampen theorem in terms of coverings and, under further hypotheses, also one in terms of fundamental groupoids.
An application is also given to knot groupoids and branched coverings.
Along the way we are led to investigate locally constant objects in a topos bounded over an arbitrary base topos S and to establish some new facts about them.
|
|
| Sylow theorems for ∞-groups |
[16 Feb 2016|06:15am] |
Натолкнулся на забавное —
Sylow theorems for ∞-groups
Matan Prasma, Tomer M. Schlank
(Submitted on 14 Feb 2016)
Viewing Kan complexes as ∞-groupoids implies that pointed and connected Kan complexes are to be viewed as ∞-groups.
A fundamental question is then: to what extent can one "do group theory" with these objects?
In this paper we develop a notion of a finite ∞-group:
an ∞-group with finitely many non-trivial homotopy groups which are all finite.
We prove a homotopical analog of the Sylow theorems for finite ∞-groups.
We derive two corollaries:
the first is a homotopical analog of the Burnside's fixed point lemma for p-groups
and the second is a "group-theoretic" characterization of (finite) nilpotent spaces.
http://arxiv.org/abs/1602.04494
|
|
| Homotopy Type Theory: A synthetic approach to higher equalities |
[20 Jan 2016|03:00pm] |
Не знаю точно, сюда ли это, но наверное, в чём-то поможет понять, вот и...
Homotopy Type Theory: A synthetic approach to higher equalities
Michael Shulman
http://arxiv.org/abs/1601.05035
This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book "Categories for the Working Philosopher."
Ask an average mathematician or philosopher today about the foundations of mathematics, and you are likely
to receive an answer involving set theory: an apparent consensus in marked contrast to the foundational
debates of the early 20th century.
Now, at the turn of the 21st century, a new theory has emerged to challenge the foundational ascendancy of sets.
Arising from a surprising synthesis of constructive intensional type theory and abstract homotopy theory, Homotopy Type Theory and Univalent Foundations (hott/uf) purports to represent more faithfully the everyday practice of mathematics, but also provides powerful new tools and a new paradigm.
So far, its concrete influence has been small, but its potential implications for mathematics and philosophy are profound.
|
|
| Dependent Inductive and Coinductive Types are Fibrational Dialgebras |
[20 Jan 2016|11:28am] |
Dependent Inductive and Coinductive Types are Fibrational Dialgebras
Henning Basold
http://arxiv.org/abs/1508.06779
In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types.
It is well-known that dependent type theories à la Martin-Löf can be interpreted using fibrations.
Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types.
I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors.
This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types.
Finally, I show how dependent data types correspond to algebras and coalgebras, and give the correspondence to dependent polynomial functors.
|
|
| Lawvere theories and Jf-relative monads |
[13 Jan 2016|01:17pm] |
[by oskar_808]
Lawvere theories and Jf-relative monads
Vladimir Voevodsky
http://arxiv.org/abs/1601.02158
In this paper we provide a detailed construction of an equivalence between the category of Lawvere theories and the category of relative monads on the obvious functor
J f : F → Sets
where F is the category with the set of objects N and morphisms being the functions between the standard finite sets of the corresponding cardinalities.
The methods of this paper are fully constructive and it should be formalizable in the Zermelo-Fraenkel theory without the axiom of choice and the excluded middle.
It is also easily formalizable in the UniMath.
|
|
| «Спонтанное нарушение дуальности» |
[08 Jan 2016|02:56pm] |
Дорогие товарищи и товарки! Заметил одну загадочную вещь.
Вот у нас есть терминальный объект — и есть инициальный. Есть уравнители — и коуравнители. Произведение и копроизведение. Ну и вообще принцип двойственности.
Всё хорошо, красиво, симметрично. Т.е. кажется, что привычка искать двойственные конструкции — это знание теории категорий на двоечку (на троечку, по утверждению  nivanych — сопряжённые функторы и умение и везде увидеть). И, если полезна конструкция, то двойственная, вроде бы, тоже всегда полезна.
Наконец, мы приходим к экспонентам и... молчок. Слепое пятно. Заговор молчания.
Т.е., казалось бы, за 60 лет существования теории категорий можно было бы понять, что из себя представляют гипотетические "коэкспоненты" и зачем они нужны.
Ну ладно, допустим, у них нет применений в разработанных на сей момент теориях. Но тогда хотя бы один из авторов учебников должен озвучить: должны быть ещё коэкспоненты, но...
«А нэту». В чём дело? «Переписывание глупостей из учебника в учебник» (в данном случае — виде умолчаний)? Двойственность — более тонкое явление и нам выдают упрощённую версию? Или что?
(то же и с топосами, кстати, про «котопосы», кажется, никто из популярных авторов не упоминает — а казалось бы, это как раз должен быть нетривиальный результат, который трудно получить в рамках не-теоркатного подхода)
|
|
| A Compositional Framework for Passive Linear Networks |
[02 Jan 2016|06:08pm] |
John C. Baez, Brendan Fong
https://golem.ph.utexas.edu/category/2015/12/a_compositional_framework_for_1.html
Passive linear networks are used in a wide variety of engineering applications, but the best studied are electrical circuits made of resistors, inductors and capacitors.
We describe a category where a morphism is a circuit of this sort with marked input and output terminals.
In this category, composition describes the process of attaching the outputs of one circuit to the
inputs of another.
We construct a functor, dubbed the 'black box functor', that takes a circuit, forgets its internal structure, and remembers only its external behavior.
Two circuits have the same external behavior if and only if they impose same relation between currents and potentials at their terminals.
The space of these currents and potentials naturally has the structure of a symplectic vector space, and the relation imposed by a circuit is a Lagrangian linear relation.
Thus, the black box functor goes from our category of circuits to the category of symplectic vector spaces and Lagrangian linear relations.
We prove that this functor is a symmetric monoidal dagger functor between dagger compact categories.
We assume the reader has some familiarity with category theory, but none with circuit theory or symplectic linear algebra.
|
|
| A New Foundation for Representation in Cognitive and Brain Science: Category Theory and the Hippocam |
[29 Dec 2015|03:25pm] |
Наверное, это всё же оффтопик...
Но прошу вас, не ругайтесь сильно ;-)
The thesis establishes correspondences between mathematical structures and brain structures.
The virtue of such a correspondence is that it makes available the powerful tools of the latter for the deduction of hypotheses for structure and function in neuropsychology.
Such an approach is relatively free from the vagaries of purely verbal reasoning and can offer novel insights into the intrinsic nature of cognitive phenomena.
It is unreasonable to think that purely linear mathematics can be the killer tool to model the complex interactions that take place in the brain.
We may indeed, need a new mathematical language for describing brain activity.
It sets the agenda of category theory as the appropriate methodology that provides the necessary theoretical framework in order to understand the structure of complex systems, like the brain, in mathematical terms.
Although category theory at first sight may seem too pure and universal, in contrast with the spurious biological realm, where the particular prevails over the universal;
it may lead to a new and deeper insight into the structure and the representational power of the brain.
The thesis paves the way for a more synthetic methodology in cognitive science, the scale free dynamics hypothesis is studied with a new “categorical” light.
In addition, it provides a theory of hippocampus structure and function based on category theory.
In particular, it demonstrates that the co-operation of the grid fields may give rise to a “colimit” which is a place field.
http://tierra.aslab.upm.es/documents/PhD/PhD-JGomez.pdf
[by zeit_raffer]
|
|
| Ещё одно введение в категории |
[06 Dec 2015|01:46pm] |
[by zeit_raffer]
Якобы для программистов (скорее, для компутерных ученых), но материал очень продвинутый.
Pierre-Louis Curien
Category theory: a programming language-oriented introduction
http://www.pps.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/articles/curien-category-theory.pdf
Нет оглавления, что неудобно, но пролистал.
Довольно много рассказывают про моноидальные диаграммы,
которыми он дальше пользуется для более наглядного изложения темы про (ко)алгебры.
Расширения Кана излагаются идеологически грамотно.
Вроде, всё хорошо и правильно — предварительно, одобряю ;-)
|
|
| Забывающие из категории моноидальных категорий |
[04 Nov 2015|04:20pm] |
Рассмотрим забывающие функторы из, например, категории симметричных замкнутых и просто моноидальных категорий в Cat.
Как должны выглядеть левые сопряжённые к ним?
В случае симметричных замкнутых, получаем просто свободное присоединение декартового произведения и экспоненты?
А в случае просто моноидальных, неужели просто декартовое произведение?
Что-то не то.
Ну и далее, рассуждения про получившуюся монаду и алгебры для неё.
Что это за логики получаются такие универсальные?
Скорее всего, ответ тут должен быть какой-то простой, но что-то я буксую...
|
|
| начать теорию категорий с полиграфов |
[13 Oct 2015|03:31pm] |
получилось зарегистрироваться...
а то что-то с картигками глючило..
сейчас я могу сам завести тему такую - начать теорию категорий с полиграфов -
ваши книги и книгу Георгия туда можно включить тогда... (или наоборот),
делаем попытку построения теории категорий сразу с поликатегорий, начать просто, а как говорят Козловский и Гарнер - мы должны столкнуться с огромными трудностями ... ну давайте дойдем до этих трудностей, зато ясность и естественность строить категории со стрелок имеющих несколько выходов и входов изначально имеется, кстати у программистов такие стрелки наверняка до всяких категорий должны встречатьтся, есть ли ссылки на подобные статьи?
|
|
