Descent data for families of function types over the circle

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík

Created on 2023-08-28.
Last modified on 2023-09-12.

module synthetic-homotopy-theory.descent-circle-function-types where
Imports 
open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels
open import foundation.whiskering-homotopies

open import synthetic-homotopy-theory.descent-circle
open import synthetic-homotopy-theory.free-loops
open import synthetic-homotopy-theory.sections-descent-circle
open import synthetic-homotopy-theory.universal-property-circle

Idea

Given two families A, B : 𝕊¹ → U over the circle, the descent data for the family of function types λ t → (A t → B t) is (X → Y, λ h → f ∘ h ∘ e⁻¹), where (X, e) is descent data for A and (Y, f) is descent data for B.

This correspondence allows us to characterize sections of this family as homomorphisms from (X, e) to (Y, f).

Definitions

Descent data for families of function types over the circle

module _
  { l1 l2 l3 : Level} {S : UU l1} (l : free-loop S)
  ( A : family-with-descent-data-circle l l2)
  ( B : family-with-descent-data-circle l l3)
  where

  family-descent-data-circle-function-type : S → UU (l2 ⊔ l3)
  family-descent-data-circle-function-type x =
    family-family-with-descent-data-circle A x →
    family-family-with-descent-data-circle B x

  descent-data-circle-function-type : descent-data-circle (l2 ⊔ l3)
  pr1 descent-data-circle-function-type =
    type-family-with-descent-data-circle A →
    type-family-with-descent-data-circle B
  pr2 descent-data-circle-function-type =
    ( equiv-postcomp
      ( type-family-with-descent-data-circle A)
      ( aut-family-with-descent-data-circle B)) ∘e
    ( equiv-precomp
      ( inv-equiv (aut-family-with-descent-data-circle A))
      ( type-family-with-descent-data-circle B))

Properties

Characterization of descent data for families of function types over the circle

module _
  { l1 l2 l3 : Level} {S : UU l1} (l : free-loop S)
  ( A : family-with-descent-data-circle l l2)
  ( B : family-with-descent-data-circle l l3)
  where

  eq-descent-data-circle-function-type :
    Eq-descent-data-circle
      ( descent-data-circle-function-type l A B)
      ( ev-descent-data-circle
        ( l)
        ( family-descent-data-circle-function-type l A B))
  pr1 eq-descent-data-circle-function-type =
    ( equiv-postcomp
      ( family-family-with-descent-data-circle A (base-free-loop l))
      ( equiv-family-with-descent-data-circle B)) ∘e
    ( equiv-precomp
      ( inv-equiv (equiv-family-with-descent-data-circle A))
      ( type-family-with-descent-data-circle B))
  pr2 eq-descent-data-circle-function-type h =
    ( eq-htpy
      ( htpy-comp-horizontal
        ( h ·l
          inv-htpy
            ( coherence-square-inv-all
              ( equiv-family-with-descent-data-circle A)
              ( aut-family-with-descent-data-circle A)
              ( equiv-tr
                ( family-family-with-descent-data-circle A)
                ( loop-free-loop l))
              ( equiv-family-with-descent-data-circle A)
              ( coherence-square-family-with-descent-data-circle A)))
        ( coherence-square-family-with-descent-data-circle B))) ∙
    ( inv
      ( ( tr-function-type
          ( family-family-with-descent-data-circle A)
          ( family-family-with-descent-data-circle B) (loop-free-loop l))
        ( map-Eq-descent-data-circle
          ( descent-data-circle-function-type l A B)
          ( ev-descent-data-circle
            ( l)
            ( family-descent-data-circle-function-type l A B))
          ( eq-descent-data-circle-function-type)
          ( h))))

  family-with-descent-data-circle-function-type :
    family-with-descent-data-circle l (l2 ⊔ l3)
  pr1 family-with-descent-data-circle-function-type =
    family-descent-data-circle-function-type l A B
  pr1 (pr2 family-with-descent-data-circle-function-type) =
    descent-data-circle-function-type l A B
  pr2 (pr2 family-with-descent-data-circle-function-type) =
    eq-descent-data-circle-function-type

Maps between families over the circle are equivalent to homomorphisms between the families' descent data

module _
  { l1 l2 l3 : Level} {S : UU l1} (l : free-loop S)
  ( A : family-with-descent-data-circle l l2)
  ( B : family-with-descent-data-circle l l3)
  where

  equiv-fixpoint-descent-data-circle-function-type-hom :
    fixpoint-descent-data-circle (descent-data-circle-function-type l A B) ≃
    hom-descent-data-circle
      ( descent-data-family-with-descent-data-circle A)
      ( descent-data-family-with-descent-data-circle B)
  equiv-fixpoint-descent-data-circle-function-type-hom =
    equiv-tot
      ( λ h →
        ( equiv-inv-htpy
          ( map-aut-family-with-descent-data-circle B ∘ h)
          ( h ∘ map-aut-family-with-descent-data-circle A)) ∘e
        ( inv-equiv
          ( equiv-coherence-triangle-maps-inv-top
            ( map-aut-family-with-descent-data-circle B ∘ h)
            ( h)
            ( aut-family-with-descent-data-circle A))) ∘e
        ( equiv-inv-htpy _ _) ∘e
        ( equiv-funext))

  equiv-ev-descent-data-circle-function-type-hom :
    dependent-universal-property-circle (l2 ⊔ l3) l →
    ( (x : S) → family-descent-data-circle-function-type l A B x) ≃
    hom-descent-data-circle
      ( descent-data-family-with-descent-data-circle A)
      ( descent-data-family-with-descent-data-circle B)
  equiv-ev-descent-data-circle-function-type-hom dup-circle =
    equiv-fixpoint-descent-data-circle-function-type-hom ∘e
    ( equiv-ev-fixpoint-descent-data-circle
      ( l)
      ( family-with-descent-data-circle-function-type l A B)
      ( dup-circle))

Recent changes