Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: bireflective subcategory

Bottom of Page

1 to 11 of 11

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2023
    • (edited Mar 24th 2023)

    added pointer to

    and rewrote the Idea-section to make it clear that these authors require not just existence of left and right adjoints, but in fact an ambidextrous adjoint and satisfying an extract coherence condition.

    diff, v6, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2023

    added pointer to:

    diff, v6, current

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 25th 2023

    have spelled out (here) the definition and some properties

    diff, v7, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2023
    • (edited Mar 26th 2023)

    Started a section “Modal type theory” (here) meant to show and explain the type theoretic rules for bireflective modalities proposed by Riley, Finster & Licata (2021).

    For the moment the section just contains a table of the main inference rules paired with their categorical semantics. The inference rules are those of RFL21, whereas the rendering of the semantics is mine.

    I do believe this semantics is equivalent to what they show in their Fig. 6, but unwinding their CwF-rules is tedious (for me, anyways, which is the reason I set out to develop the semantics from scratch). But I have checked in detail that our ♮\natural-elim interpretations coincide, which is the main subtlety.

    Moreover, in the categorical semantics I show (now in the entry) the respect of the computation rules is manifestly verified (as shown by the diagrams now in the entry), which is really what matters.

    Aside from the detailed syntax/semantics tables, the section remains a little telegraphic for the moment. Will expand tomorrow.

    diff, v8, current

    • CommentRowNumber5.
    • CommentAuthorThomas Holder
    • CommentTimeMar 26th 2023

    Added a reference to

    • {#JS96}P. Johnstone, Remarks on Quintessential and Persistent Localizations , TAC 2 no.8 (1996) pp.90-99. (pdf)

    diff, v9, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2023
    • (edited Mar 27th 2023)

    Thanks! I have added also pointer to

    • G. M. Kelly, F. W. Lawvere, On the complete lattice of essential localizations, Bull. Soc. Math. Belg. Sér. A 41 (1989) 289–319

    and then I further expanded the Idea-section to make it clear that there are three concepts here

    essential localizations ⊃\supset quintessential localizations ⊃\supset bireflective subcategories.

    diff, v10, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2023

    added the observation (here) that a model 1-category theoretic presentation of the “bireflective sub-∞\infty-category” Grpd ∞↪TGrpd ∞Grpd_\infty \hookrightarrow T Grpd_\infty may be recognized in Hebestreit, Sagave & Schlichtkrull (2020), Lem. 3.19

    diff, v13, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2023
    • (edited Apr 3rd 2023)

    added (here) the observation/derivation that the categorical semantics for (a↦a̲ ♮):A→♮A̲(a \mapsto \underline{a}^\natural) \colon A \to \natural \underline{A} is given simply by postcomposition with the naturality square of the unit η ♮\eta^\natural

    diff, v17, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeApr 4th 2023

    added a remark (here) making explicit some possibly unexpected conventions in the RFL-syntax

    diff, v19, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 4th 2023

    added (here) semantic verification for the rule of ♮\natural respecting dependent pairs

    diff, v20, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 4th 2023
    • (edited Apr 4th 2023)

    added (here) syntax and semantics for the decomposition of any type AA as the sum over its linear fiber types A x̲A_{\underline{x}}

    diff, v21, current

1 to 11 of 11

  1.