Pointed types equipped with automorphisms

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-06-29.
Last modified on 2024-03-02.

module structured-types.pointed-types-equipped-with-automorphisms where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.automorphisms
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
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.homotopy-induction
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import structured-types.pointed-types

Idea

A pointed type equipped with an automorphism is a pair consisting of a pointed type A and an automorphism on the underlying type of A. The base point is not required to be preserved.

Definitions

Types equipped with an automorphism

Pointed-Type-With-Aut :
  (l : Level) → UU (lsuc l)
Pointed-Type-With-Aut l =
  Σ (Pointed-Type l) (λ X → Aut (type-Pointed-Type X))

module _
  {l : Level} (X : Pointed-Type-With-Aut l)
  where

  pointed-type-Pointed-Type-With-Aut : Pointed-Type l
  pointed-type-Pointed-Type-With-Aut = pr1 X

  type-Pointed-Type-With-Aut : UU l
  type-Pointed-Type-With-Aut =
    type-Pointed-Type pointed-type-Pointed-Type-With-Aut

  point-Pointed-Type-With-Aut : type-Pointed-Type-With-Aut
  point-Pointed-Type-With-Aut =
    point-Pointed-Type pointed-type-Pointed-Type-With-Aut

  aut-Pointed-Type-With-Aut : Aut type-Pointed-Type-With-Aut
  aut-Pointed-Type-With-Aut = pr2 X

  map-aut-Pointed-Type-With-Aut :
    type-Pointed-Type-With-Aut → type-Pointed-Type-With-Aut
  map-aut-Pointed-Type-With-Aut = map-equiv aut-Pointed-Type-With-Aut

  map-inv-aut-Pointed-Type-With-Aut :
    type-Pointed-Type-With-Aut → type-Pointed-Type-With-Aut
  map-inv-aut-Pointed-Type-With-Aut = map-inv-equiv aut-Pointed-Type-With-Aut

  is-section-map-inv-aut-Pointed-Type-With-Aut :
    (map-aut-Pointed-Type-With-Aut ∘ map-inv-aut-Pointed-Type-With-Aut) ~ id
  is-section-map-inv-aut-Pointed-Type-With-Aut =
    is-section-map-inv-equiv aut-Pointed-Type-With-Aut

  is-retraction-map-inv-aut-Pointed-Type-With-Aut :
    (map-inv-aut-Pointed-Type-With-Aut ∘ map-aut-Pointed-Type-With-Aut) ~ id
  is-retraction-map-inv-aut-Pointed-Type-With-Aut =
    is-retraction-map-inv-equiv aut-Pointed-Type-With-Aut

Morphisms of pointed types with automorphisms

hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} →
  Pointed-Type-With-Aut l1 → Pointed-Type-With-Aut l2 → UU (l1 ⊔ l2)
hom-Pointed-Type-With-Aut {l1} {l2} X Y =
  Σ ( type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut Y)
    ( λ f →
      (f (point-Pointed-Type-With-Aut X) ＝ point-Pointed-Type-With-Aut Y) ×
      ( ( f ∘ (map-aut-Pointed-Type-With-Aut X)) ~
        ( (map-aut-Pointed-Type-With-Aut Y) ∘ f)))

module _
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1) (Y : Pointed-Type-With-Aut l2)
  (f : hom-Pointed-Type-With-Aut X Y)
  where

  map-hom-Pointed-Type-With-Aut :
    type-Pointed-Type-With-Aut X → type-Pointed-Type-With-Aut Y
  map-hom-Pointed-Type-With-Aut = pr1 f

  preserves-point-map-hom-Pointed-Type-With-Aut :
    ( map-hom-Pointed-Type-With-Aut (point-Pointed-Type-With-Aut X)) ＝
    ( point-Pointed-Type-With-Aut Y)
  preserves-point-map-hom-Pointed-Type-With-Aut = pr1 (pr2 f)

  preserves-aut-map-hom-Pointed-Type-With-Aut :
    ( map-hom-Pointed-Type-With-Aut ∘ map-aut-Pointed-Type-With-Aut X) ~
    ( ( map-aut-Pointed-Type-With-Aut Y) ∘ map-hom-Pointed-Type-With-Aut)
  preserves-aut-map-hom-Pointed-Type-With-Aut = pr2 (pr2 f)

Properties

Characterization of the identity type of morphisms of pointed types with automorphisms

htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1)
  (Y : Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  UU (l1 ⊔ l2)
htpy-hom-Pointed-Type-With-Aut X Y h1 h2 =
  Σ ( map-hom-Pointed-Type-With-Aut X Y h1
      ~ map-hom-Pointed-Type-With-Aut X Y h2)
    ( λ H →
      ( ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1) ＝
        ( ( H (point-Pointed-Type-With-Aut X)) ∙
          ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h2))) ×
      ( ( x : type-Pointed-Type-With-Aut X) →
        ( ( ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1 x) ∙
            ( ap (map-aut-Pointed-Type-With-Aut Y) (H x))) ＝
          ( ( H (map-aut-Pointed-Type-With-Aut X x)) ∙
            ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h2 x)))))

refl-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1)
  (Y : Pointed-Type-With-Aut l2) (h : hom-Pointed-Type-With-Aut X Y) →
  htpy-hom-Pointed-Type-With-Aut X Y h h
refl-htpy-hom-Pointed-Type-With-Aut X Y h =
  pair refl-htpy (pair refl (λ x → right-unit))

htpy-hom-Pointed-Type-With-Aut-eq :
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1)
  (Y : Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  h1 ＝ h2 → htpy-hom-Pointed-Type-With-Aut X Y h1 h2
htpy-hom-Pointed-Type-With-Aut-eq X Y h1 .h1 refl =
  refl-htpy-hom-Pointed-Type-With-Aut X Y h1

is-torsorial-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1)
  (Y : Pointed-Type-With-Aut l2) (h1 : hom-Pointed-Type-With-Aut X Y) →
  is-torsorial (htpy-hom-Pointed-Type-With-Aut X Y h1)
is-torsorial-htpy-hom-Pointed-Type-With-Aut X Y h1 =
  is-torsorial-Eq-structure
    ( is-torsorial-htpy (map-hom-Pointed-Type-With-Aut X Y h1))
    ( pair (map-hom-Pointed-Type-With-Aut X Y h1) refl-htpy)
    ( is-torsorial-Eq-structure
      ( is-torsorial-Id
        ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1))
      ( pair (preserves-point-map-hom-Pointed-Type-With-Aut X Y h1) refl)
      ( is-contr-equiv'
        ( Σ ( ( x : type-Pointed-Type-With-Aut X) →
              ( map-hom-Pointed-Type-With-Aut X Y h1
                ( map-aut-Pointed-Type-With-Aut X x)) ＝
              ( map-aut-Pointed-Type-With-Aut Y
                ( map-hom-Pointed-Type-With-Aut X Y h1 x)))
            ( λ aut-h2 →
              ( x : type-Pointed-Type-With-Aut X) →
              preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1 x ＝ aut-h2 x))
        ( equiv-tot (equiv-concat-htpy right-unit-htpy))
        ( is-torsorial-htpy
          ( preserves-aut-map-hom-Pointed-Type-With-Aut X Y h1))))

is-equiv-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1)
  (Y : Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  is-equiv (htpy-hom-Pointed-Type-With-Aut-eq X Y h1 h2)
is-equiv-htpy-hom-Pointed-Type-With-Aut X Y h1 =
  fundamental-theorem-id
    ( is-torsorial-htpy-hom-Pointed-Type-With-Aut X Y h1)
    ( htpy-hom-Pointed-Type-With-Aut-eq X Y h1)

eq-htpy-hom-Pointed-Type-With-Aut :
  {l1 l2 : Level} (X : Pointed-Type-With-Aut l1)
  (Y : Pointed-Type-With-Aut l2) (h1 h2 : hom-Pointed-Type-With-Aut X Y) →
  htpy-hom-Pointed-Type-With-Aut X Y h1 h2 → h1 ＝ h2
eq-htpy-hom-Pointed-Type-With-Aut X Y h1 h2 =
  map-inv-is-equiv (is-equiv-htpy-hom-Pointed-Type-With-Aut X Y h1 h2)

Recent changes