Generalized cohomology, spectra and orientations

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionThe homotopy fibre of the fibre inclusion is the loop space of the base#

For a Hurewicz fibration p, the space of paths in E from the fibre through e₀ to e₀ is homotopy equivalent to the loop space Ω B (p e₀), by composing the paths with p.

TauCeti.FiberInclusionPathFiber.loopHomotopyEquiv.{u, v} {E : Type u} {B : Type v}
  [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E)
  (hp : TauCeti.IsHurewiczFibration ⇑p) :
  ContinuousMap.HomotopyEquiv (TauCeti.FiberInclusionPathFiber p e₀) (LoopSpace B (p e₀))
Lean

Formalized in Tau Ceti as TauCeti.FiberInclusionPathFiber.loopHomotopyEquiv.

Sources
LeanTauCeti.FiberInclusionPathFiber.loopHomotopyEquiv

TheoremTauCeti.isHurewiczFibration_iff_nonempty_liftingFunction#

A map is a Hurewicz fibration for test spaces in Type (max u v) if and only if it has a lifting function.

TauCeti.isHurewiczFibration_iff_nonempty_liftingFunction.{u, v} {E : Type u} {B : Type v}
  [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} :
  TauCeti.IsHurewiczFibration ⇑p ↔ Nonempty (TauCeti.LiftingFunction p)
Lean

Formalized in Tau Ceti as TauCeti.isHurewiczFibration_iff_nonempty_liftingFunction.

Sources
LeanTauCeti.isHurewiczFibration_iff_nonempty_liftingFunction

TheoremTauCeti.MappingPathSpace.isHurewiczFibration_endpoint#

The endpoint map of a mapping-path replacement is a Hurewicz fibration, for test spaces in every universe.

TauCeti.MappingPathSpace.isHurewiczFibration_endpoint.{w, u', v'} {B : Type u'} {K : Type v'}
  [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) :
  TauCeti.IsHurewiczFibration ⇑(TauCeti.MappingPathSpace.endpoint f)
Lean

Formalized in Tau Ceti as TauCeti.MappingPathSpace.isHurewiczFibration_endpoint.

Sources
LeanTauCeti.MappingPathSpace.isHurewiczFibration_endpoint

DefinitionTauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace#

A reference path α from f b to k makes the fibre of the source projection over b homotopy equivalent to the loop space Ω K k. A path γ from f b to k is sent to the loop α.symm.trans γ, and the homotopy inverse sends a loop ℓ to the path α.trans ℓ.

TauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace.{u, v} {B : Type u} {K : Type v}
  [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) (α : Path (f b) k) :
  ContinuousMap.HomotopyEquiv { p // (TauCeti.MappingPathFiber.proj f k) p = b } (LoopSpace K k)
Lean

Formalized in Tau Ceti as TauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace.

Sources
LeanTauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace

TheoremCategoryTheory.MonoidalCategory.DayFunctor.isCommMonObj#

The Day convolution monoid of a lax braided functor out of a symmetric monoidal category is commutative.

CategoryTheory.MonoidalCategory.DayFunctor.isCommMonObj.{v₁, v₂, u₁, u₂} {C : Type u₁}
  [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V]
  [∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [(CategoryTheory.Functor.fromPUnit
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [CategoryTheory.SymmetricCategory C] [CategoryTheory.BraidedCategory V]
  (F : CategoryTheory.MonoidalCategory.DayFunctor C V) [F.functor.LaxBraided] :
  CategoryTheory.IsCommMonObj F
Lean

Formalized in Tau Ceti as CategoryTheory.MonoidalCategory.DayFunctor.isCommMonObj.

Sources
LeanCategoryTheory.MonoidalCategory.DayFunctor.isCommMonObj

AbbreviationTauCeti.PointedSSet.suspensionLoopAdjunction#

Smash with the simplicial circle is left adjoint to the pointed mapping simplicial set out of the circle.

TauCeti.PointedSSet.suspensionLoopAdjunction :
  TauCeti.PointedSSet.suspension ⊣ TauCeti.PointedSSet.loops
Lean

Formalized in Tau Ceti as TauCeti.PointedSSet.suspensionLoopAdjunction.

Sources
LeanTauCeti.PointedSSet.suspensionLoopAdjunction
Uses 1
Statement usesTauCeti.PointedSSet.monoidalClosed

AbbreviationTauCeti.SymmetricSpectrum#

Symmetric spectra of pointed simplicial sets: the modules over the commutative monoid SymmetricSequence.sphere of symmetric sequences. A symmetric spectrum is a symmetric sequence X with an action S ⊗ X ⟶ X for the Day convolution product, satisfying the unit and associativity laws.

TauCeti.SymmetricSpectrum : Type 1
Lean

Formalized in Tau Ceti as TauCeti.SymmetricSpectrum.

Sources
LeanTauCeti.SymmetricSpectrum
Uses 3 · Used by 1
Statement usesTauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor · TauCeti.SymmetricSequence
Proof usesTauCeti.PointedSSet.monoidalClosed
Used byTauCeti.SymmetricSpectrum.isLimitOfLevelwise

DefinitionTauCeti.SymmetricSpectrum.isLimitOfLevelwise#

A cone of symmetric spectra is limiting if its cone of pointed simplicial sets is limiting at every level. In particular, the limiting maps respect the sphere action.

TauCeti.SymmetricSpectrum.isLimitOfLevelwise.{v, w} {J : Type w} [CategoryTheory.Category.{v, w} J]
  {F : CategoryTheory.Functor J TauCeti.SymmetricSpectrum} (c : CategoryTheory.Limits.Cone F)
  (h :
    (n : ℕ) →
      CategoryTheory.Limits.IsLimit
        (((CategoryTheory.evaluation TauCeti.FiniteBijection TauCeti.PointedSSet).obj
              { len := n }).mapCone
          ((CategoryTheory.MonoidalCategory.DayFunctor.equiv TauCeti.FiniteBijection
                  TauCeti.PointedSSet).functor.mapCone
            ((CategoryTheory.Mod.forget TauCeti.SymmetricSequence.sphere).mapCone c)))) :
  CategoryTheory.Limits.IsLimit c
Lean

Formalized in Tau Ceti as TauCeti.SymmetricSpectrum.isLimitOfLevelwise.

Sources
LeanTauCeti.SymmetricSpectrum.isLimitOfLevelwise
Uses 4
Statement usesTauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor · TauCeti.PointedSSet.monoidalClosed · TauCeti.SymmetricSequence · TauCeti.SymmetricSpectrum

AbbreviationTauCeti.SymmetricSequence#

Symmetric sequences of pointed simplicial sets: functors from the finite-bijection groupoid to pointed simplicial sets, with the Day convolution product along the block sum.

TauCeti.SymmetricSequence.{u} : Type (u + 1)
Lean

Formalized in Tau Ceti as TauCeti.SymmetricSequence.

Sources
LeanTauCeti.SymmetricSequence
Used by 2
Used byTauCeti.SymmetricSpectrum · TauCeti.SymmetricSpectrum.isLimitOfLevelwise

InstanceTauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor#

The block swap of FiniteBijection acts on X^∧(k + l) as the swap of the two smash factors X^∧k ∧ X^∧l, so the symmetric sequence of smash powers is a braided monoidal functor.

TauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor.{u} {X : TauCeti.PointedSSet} :
  X.smashPowFunctor.Braided
Lean

Formalized in Tau Ceti as TauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor.

Sources
LeanTauCeti.PointedSSet.instBraidedFiniteBijectionSmashPowFunctor
Used by 2
Used byTauCeti.SymmetricSpectrum · TauCeti.SymmetricSpectrum.isLimitOfLevelwise

InstanceTauCeti.PointedSSet.monoidalClosed#

The smash product of pointed simplicial sets is closed: X ⊗ - is left adjoint to the pointed mapping simplicial set functor Map_*(X, -).

TauCeti.PointedSSet.monoidalClosed.{u} : CategoryTheory.MonoidalClosed TauCeti.PointedSSet
Lean

Formalized in Tau Ceti as TauCeti.PointedSSet.monoidalClosed.

Sources
LeanTauCeti.PointedSSet.monoidalClosed
Used by 3
Used byTauCeti.PointedSSet.suspensionLoopAdjunction · TauCeti.SymmetricSpectrum · TauCeti.SymmetricSpectrum.isLimitOfLevelwise

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.