Sections of families over the circle

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

Created on 2023-08-28.
Last modified on 2024-04-25.

module synthetic-homotopy-theory.sections-descent-circle where
Imports 
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-identifications
open import foundation.commuting-triangles-of-maps
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-identifications
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.transport-along-identifications
open import foundation.universe-levels

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

Idea

Sections of type families over the circle are exactly the fixpoints of the automorphism from the corresponding descent data.

Definitions

Fixpoints of descent data

A fixpoint of (X, e) is a fixpoint of e.

fixpoint-descent-data-circle :
  { l1 : Level}
  ( P : descent-data-circle l1) → UU l1
fixpoint-descent-data-circle P =
  Σ ( type-descent-data-circle P)
    ( λ x → (map-descent-data-circle P x) ＝ x)

Properties

Characterization of sections of type families over the circle

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

  map-compute-dependent-identification-loop-circle :
    ( x y : type-family-with-descent-data-circle A) →
    map-aut-family-with-descent-data-circle A x ＝ y →
    dependent-identification (family-family-with-descent-data-circle A)
      ( loop-free-loop l)
      ( map-equiv-family-with-descent-data-circle A x)
      ( map-equiv-family-with-descent-data-circle A y)
  map-compute-dependent-identification-loop-circle x y q =
    inv (coherence-square-family-with-descent-data-circle A x) ∙
    ( ap (map-equiv-family-with-descent-data-circle A) q)

  is-equiv-map-compute-dependent-identification-loop-circle :
    ( x y : type-family-with-descent-data-circle A) →
    is-equiv (map-compute-dependent-identification-loop-circle x y)
  is-equiv-map-compute-dependent-identification-loop-circle x y =
    fundamental-theorem-id
      ( is-contr-equiv'
        ( fiber
          ( map-equiv-family-with-descent-data-circle A)
          ( tr
            ( family-family-with-descent-data-circle A)
            ( loop-free-loop l)
            ( map-equiv-family-with-descent-data-circle A x)))
        ( equiv-fiber _ _)
        ( is-contr-map-is-equiv
          ( is-equiv-map-equiv (equiv-family-with-descent-data-circle A))
          ( tr
            ( family-family-with-descent-data-circle A)
            ( loop-free-loop l)
            ( map-equiv-family-with-descent-data-circle A x))))
      ( map-compute-dependent-identification-loop-circle x)
      ( y)

  compute-dependent-identification-loop-circle :
    ( x y : type-family-with-descent-data-circle A) →
    ( map-aut-family-with-descent-data-circle A x ＝ y) ≃
    ( dependent-identification
      ( family-family-with-descent-data-circle A)
      ( loop-free-loop l)
      ( map-equiv-family-with-descent-data-circle A x)
      ( map-equiv-family-with-descent-data-circle A y))
  pr1 (compute-dependent-identification-loop-circle x y) =
    map-compute-dependent-identification-loop-circle x y
  pr2 (compute-dependent-identification-loop-circle x y) =
    is-equiv-map-compute-dependent-identification-loop-circle x y

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

  ev-fixpoint-descent-data-circle :
    ( (x : S) → family-family-with-descent-data-circle A x) →
    ( fixpoint-descent-data-circle
      ( descent-data-family-with-descent-data-circle A))
  pr1 (ev-fixpoint-descent-data-circle s) =
    map-inv-equiv
      ( equiv-family-with-descent-data-circle A)
      ( s (base-free-loop l))
  pr2 (ev-fixpoint-descent-data-circle s) =
    map-inv-equiv
      ( compute-dependent-identification-loop-circle
        ( l)
        ( A)
        ( map-inv-equiv
          ( equiv-family-with-descent-data-circle A)
          ( s (base-free-loop l)))
        ( map-inv-equiv
          ( equiv-family-with-descent-data-circle A)
          ( s (base-free-loop l))))
      ( ( ap
          ( tr (family-family-with-descent-data-circle A) (loop-free-loop l))
          ( is-section-map-inv-equiv
            ( equiv-family-with-descent-data-circle A)
            ( s (base-free-loop l)))) ∙
        ( ( apd s (loop-free-loop l)) ∙
          ( inv
            ( is-section-map-inv-equiv
              ( equiv-family-with-descent-data-circle A)
              ( s (base-free-loop l))))))

  equiv-fixpoint-descent-data-circle-free-dependent-loop :
    ( fixpoint-descent-data-circle
      ( descent-data-family-with-descent-data-circle A)) ≃
    ( free-dependent-loop l (family-family-with-descent-data-circle A))
  equiv-fixpoint-descent-data-circle-free-dependent-loop =
    equiv-Σ
      ( λ x →
        dependent-identification
          ( family-family-with-descent-data-circle A)
          ( loop-free-loop l)
          ( x)
          ( x))
      ( equiv-family-with-descent-data-circle A)
      ( λ x →
        compute-dependent-identification-loop-circle l A x x)

  comparison-fixpoint-descent-data-circle :
    ( fixpoint-descent-data-circle
      ( descent-data-family-with-descent-data-circle A)) →
    ( free-dependent-loop l (family-family-with-descent-data-circle A))
  comparison-fixpoint-descent-data-circle =
    map-equiv equiv-fixpoint-descent-data-circle-free-dependent-loop

  triangle-comparison-fixpoint-descent-data-circle :
    coherence-triangle-maps
      ( ev-free-loop-Π l (family-family-with-descent-data-circle A))
      ( comparison-fixpoint-descent-data-circle)
      ( ev-fixpoint-descent-data-circle)
  triangle-comparison-fixpoint-descent-data-circle s =
    eq-Eq-free-dependent-loop l
      ( family-family-with-descent-data-circle A)
      ( ev-free-loop-Π l (family-family-with-descent-data-circle A) s)
      ( ( comparison-fixpoint-descent-data-circle ∘
          ev-fixpoint-descent-data-circle)
        ( s))
      ( inv is-section-inv-α ,
        inv
        ( ( horizontal-concat-Id²
            ( refl
              { x =
                ap
                  ( tr
                    ( family-family-with-descent-data-circle A)
                    ( loop-free-loop l))
                  ( inv is-section-inv-α)})
            ( is-section-map-inv-is-equiv
              ( is-equiv-map-compute-dependent-identification-loop-circle
                ( l)
                ( A)
                ( map-inv-equiv
                  ( equiv-family-with-descent-data-circle A)
                  ( s (base-free-loop l)))
                ( pr1 (ev-fixpoint-descent-data-circle s)))
              ( _))) ∙
          ( ( inv (assoc (ap _ (inv is-section-inv-α)) _ _)) ∙
            ( horizontal-concat-Id²
              ( inv
                ( map-coherence-triangle-identifications
                  ( tr
                    ( family-family-with-descent-data-circle A)
                    ( loop-free-loop l))
                  ( refl)
                  ( is-section-inv-α)
                  ( inv is-section-inv-α)
                  ( inv (left-inv is-section-inv-α))))
              ( refl)))))
    where
    is-section-inv-α :
      eq-value
        ( map-equiv-family-with-descent-data-circle A ∘
          map-inv-equiv (equiv-family-with-descent-data-circle A))
        ( id)
        ( s (base-free-loop l))
    is-section-inv-α =
      is-section-map-inv-equiv
        ( equiv-family-with-descent-data-circle A)
        ( s (base-free-loop l))

  is-equiv-comparison-fixpoint-descent-data-circle :
    is-equiv comparison-fixpoint-descent-data-circle
  is-equiv-comparison-fixpoint-descent-data-circle =
    is-equiv-map-equiv equiv-fixpoint-descent-data-circle-free-dependent-loop

  is-equiv-ev-fixpoint-descent-data-circle :
    dependent-universal-property-circle l →
    is-equiv ev-fixpoint-descent-data-circle
  is-equiv-ev-fixpoint-descent-data-circle dup-circle =
    is-equiv-top-map-triangle
      ( ev-free-loop-Π l (family-family-with-descent-data-circle A))
      ( comparison-fixpoint-descent-data-circle)
      ( ev-fixpoint-descent-data-circle)
      ( triangle-comparison-fixpoint-descent-data-circle)
      ( is-equiv-comparison-fixpoint-descent-data-circle)
      ( dup-circle (family-family-with-descent-data-circle A))

  equiv-ev-fixpoint-descent-data-circle :
    dependent-universal-property-circle l →
    ( (x : S) → (family-family-with-descent-data-circle A) x) ≃
    ( fixpoint-descent-data-circle
      ( descent-data-family-with-descent-data-circle A))
  pr1 (equiv-ev-fixpoint-descent-data-circle dup-circle) =
    ev-fixpoint-descent-data-circle
  pr2 (equiv-ev-fixpoint-descent-data-circle dup-circle) =
    is-equiv-ev-fixpoint-descent-data-circle dup-circle

  compute-ev-fixpoint-descent-data-circle :
    coherence-square-maps
      ( ev-fixpoint-descent-data-circle)
      ( ev-point (base-free-loop l))
      ( pr1)
      ( map-inv-equiv (equiv-family-with-descent-data-circle A))
  compute-ev-fixpoint-descent-data-circle = refl-htpy

Recent changes