# Hatcher's acyclic type

Content created by Fredrik Bakke, Egbert Rijke, Raymond Baker and Tom de Jong.

Created on 2023-04-26.

module synthetic-homotopy-theory.hatchers-acyclic-type where

Imports
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.commuting-squares-of-identifications
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.pointed-universal-property-contractible-types

open import synthetic-homotopy-theory.acyclic-types
open import synthetic-homotopy-theory.eckmann-hilton-argument
open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.loop-spaces
open import synthetic-homotopy-theory.powers-of-loops
open import synthetic-homotopy-theory.suspensions-of-pointed-types
open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types


## Idea

Hatcher's acyclic type is a higher inductive type equipped with a base point and two loops a and b, and identifications witnessing that a⁵ ＝ b³ and b³ = (ab)². This type is acyclic, because the structure on Hatcher's acyclic type on any loop space is contractible.

## Definitions

### The structure of Hatcher's acyclic type

structure-Hatcher-Acyclic-Type : {l : Level} → Pointed-Type l → UU l
structure-Hatcher-Acyclic-Type A =
Σ ( type-Ω A)
( λ a →
Σ ( type-Ω A)
( λ b →
( power-nat-Ω 5 A a ＝ power-nat-Ω 3 A b) ×
( power-nat-Ω 3 A b ＝ power-nat-Ω 2 A (a ∙ b))))


### Algebras with the structure of Hatcher's acyclic type

algebra-Hatcher-Acyclic-Type : (l : Level) → UU (lsuc l)
algebra-Hatcher-Acyclic-Type l =
Σ (Pointed-Type l) structure-Hatcher-Acyclic-Type


### Morphisms of types equipped with the structure of Hatcher's acyclic type

module _
{l1 l2 : Level}
((A , a1 , a2 , r1 , r2) : algebra-Hatcher-Acyclic-Type l1)
((B , b1 , b2 , s1 , s2) : algebra-Hatcher-Acyclic-Type l2)
where

is-hom-pointed-map-algebra-Hatcher-Acyclic-Type : (A →∗ B) → UU l2
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type f =
Σ ( map-Ω f a1 ＝ b1)
( λ u →
Σ ( map-Ω f a2 ＝ b2)
( λ v →
( coherence-square-identifications
( ap (map-Ω f) r1)
( map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u)
( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)
( s1)) ×
( coherence-square-identifications
( ap (map-Ω f) r2)
( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)
( ( map-power-nat-Ω 2 f (a1 ∙ a2)) ∙
( ap
( power-nat-Ω 2 B)
( ( preserves-mul-map-Ω f) ∙
( horizontal-concat-Id² u v))))
( s2))))

hom-algebra-Hatcher-Acyclic-Type : UU (l1 ⊔ l2)
hom-algebra-Hatcher-Acyclic-Type =
Σ ( A →∗ B) is-hom-pointed-map-algebra-Hatcher-Acyclic-Type


### Initial Hatcher acyclic algebras

One characterization of Hatcher's acyclic type is through its universal property as being the initial Hatcher acyclic algebra.

is-initial-algebra-Hatcher-Acyclic-Type :
{l1 : Level} (A : algebra-Hatcher-Acyclic-Type l1) → UUω
is-initial-algebra-Hatcher-Acyclic-Type A =
{l : Level} →
(B : algebra-Hatcher-Acyclic-Type l) →
is-contr (hom-algebra-Hatcher-Acyclic-Type A B)


## Properties

### Characterization of identifications of Hatcher acyclic type structures

module _
{l : Level} (A : Pointed-Type l) (s : structure-Hatcher-Acyclic-Type A)
where

Eq-structure-Hatcher-Acyclic-Type :
structure-Hatcher-Acyclic-Type A → UU l
Eq-structure-Hatcher-Acyclic-Type t =
Σ ( pr1 s ＝ pr1 t)
( λ p →
Σ ( pr1 (pr2 s) ＝ pr1 (pr2 t))
( λ q →
( ( pr1 (pr2 (pr2 s)) ∙ ap (power-nat-Ω 3 A) q) ＝
( (ap (power-nat-Ω 5 A) p) ∙ pr1 (pr2 (pr2 t)))) ×
( ( pr2 (pr2 (pr2 s)) ∙
ap (power-nat-Ω 2 A) (horizontal-concat-Id² p q)) ＝
( ap (power-nat-Ω 3 A) q ∙ pr2 (pr2 (pr2 t))))))

refl-Eq-structure-Hatcher-Acyclic-Type :
Eq-structure-Hatcher-Acyclic-Type s
pr1 refl-Eq-structure-Hatcher-Acyclic-Type = refl
pr1 (pr2 refl-Eq-structure-Hatcher-Acyclic-Type) = refl
pr1 (pr2 (pr2 refl-Eq-structure-Hatcher-Acyclic-Type)) = right-unit
pr2 (pr2 (pr2 refl-Eq-structure-Hatcher-Acyclic-Type)) = right-unit

is-torsorial-Eq-structure-Hatcher-Acyclic-Type :
is-torsorial Eq-structure-Hatcher-Acyclic-Type
is-torsorial-Eq-structure-Hatcher-Acyclic-Type =
is-torsorial-Eq-structure
( is-torsorial-Id (pr1 s))
( pr1 s , refl)
( is-torsorial-Eq-structure
( is-torsorial-Id (pr1 (pr2 s)))
( pr1 (pr2 s) , refl)
( is-torsorial-Eq-structure
( is-torsorial-Id (pr1 (pr2 (pr2 s)) ∙ refl))
( pr1 (pr2 (pr2 s)) , right-unit)
( is-torsorial-Id (pr2 (pr2 (pr2 s)) ∙ refl))))

Eq-eq-structure-Hatcher-Acyclic-Type :
(t : structure-Hatcher-Acyclic-Type A) →
(s ＝ t) → Eq-structure-Hatcher-Acyclic-Type t
Eq-eq-structure-Hatcher-Acyclic-Type .s refl =
refl-Eq-structure-Hatcher-Acyclic-Type

is-equiv-Eq-eq-structure-Hatcher-Acyclic-Type :
(t : structure-Hatcher-Acyclic-Type A) →
is-equiv (Eq-eq-structure-Hatcher-Acyclic-Type t)
is-equiv-Eq-eq-structure-Hatcher-Acyclic-Type =
fundamental-theorem-id
is-torsorial-Eq-structure-Hatcher-Acyclic-Type
Eq-eq-structure-Hatcher-Acyclic-Type

extensionality-structure-Hatcher-Acyclic-Type :
(t : structure-Hatcher-Acyclic-Type A) →
(s ＝ t) ≃ Eq-structure-Hatcher-Acyclic-Type t
pr1 (extensionality-structure-Hatcher-Acyclic-Type t) =
Eq-eq-structure-Hatcher-Acyclic-Type t
pr2 (extensionality-structure-Hatcher-Acyclic-Type t) =
is-equiv-Eq-eq-structure-Hatcher-Acyclic-Type t

eq-Eq-structure-Hatcher-Acyclic-Type :
(t : structure-Hatcher-Acyclic-Type A) →
Eq-structure-Hatcher-Acyclic-Type t → s ＝ t
eq-Eq-structure-Hatcher-Acyclic-Type t =
map-inv-equiv (extensionality-structure-Hatcher-Acyclic-Type t)


### Loop spaces uniquely have the structure of a Hatcher acyclic type

module _
{l : Level} (A : Pointed-Type l)
where

is-contr-structure-Hatcher-Acyclic-Type-Ω :
is-contr (structure-Hatcher-Acyclic-Type (Ω A))
is-contr-structure-Hatcher-Acyclic-Type-Ω =
is-contr-equiv
( Σ (type-Ω (Ω A)) (λ a → refl ＝ a))
( equiv-tot
( λ a →
( ( inv-equiv
( equiv-ap
( equiv-concat' (refl-Ω A) (power-nat-Ω 5 (Ω A) a))
( refl-Ω (Ω A))
( a))) ∘e
( equiv-concat'
( power-nat-Ω 5 (Ω A) a)
( ( inv (power-nat-mul-Ω 3 2 (Ω A) a)) ∙
( power-nat-succ-Ω' 5 (Ω A) a)))) ∘e
( ( ( left-unit-law-Σ-is-contr
( is-torsorial-Id' (a ∙ a))
( a ∙ a , refl)) ∘e
( inv-associative-Σ
( type-Ω (Ω A))
( λ b → b ＝ (a ∙ a))
( λ bq →
power-nat-Ω 5 (Ω A) a ＝ power-nat-Ω 3 (Ω A) (pr1 bq)))) ∘e
( equiv-tot
( λ b →
( commutative-product) ∘e
( equiv-product
( id-equiv)
( ( ( inv-equiv
( equiv-ap
( equiv-concat' (refl-Ω A) (b ∙ b))
( b)
( a ∙ a))) ∘e
( equiv-concat
( inv (power-nat-add-Ω 1 2 (Ω A) b))
( (a ∙ a) ∙ (b ∙ b)))) ∘e
( equiv-concat'
( power-nat-Ω 3 (Ω A) b)
( interchange-concat-Ω² a b a b)))))))))
( is-torsorial-Id refl)


### For a fixed pointed map, the is-hom-pointed-map-algebra-Hatcher-Acyclic-Type family is torsorial

In proving this, it is helpful to consider an equivalent formulation of is-hom-pointed-map-algebra-Hatcher-Acyclic-Type for which torsoriality is almost immediate.

module _
{l1 l2 : Level}
((A , a1 , a2 , r1 , r2) : algebra-Hatcher-Acyclic-Type l1)
((B , b1 , b2 , s1 , s2) : algebra-Hatcher-Acyclic-Type l2)
where

is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' : (A →∗ B) → UU l2
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' f =
Σ ( map-Ω f a1 ＝ b1)
( λ u →
Σ ( map-Ω f a2 ＝ b2)
( λ v →
( Id
( inv (map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u) ∙
( ap (map-Ω f) r1 ∙
(map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)))
( s1)) ×
( Id
( inv (map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v) ∙
( ap (map-Ω f) r2 ∙
( ( map-power-nat-Ω 2 f (a1 ∙ a2)) ∙
( ap
( power-nat-Ω 2 B)
( ( preserves-mul-map-Ω f) ∙
( horizontal-concat-Id² u v))))))
( s2))))

module _
{l1 l2 : Level}
((A , σ) : algebra-Hatcher-Acyclic-Type l1)
((B , τ) : algebra-Hatcher-Acyclic-Type l2)
where

equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type :
(f : A →∗ B) →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type (A , σ) (B , τ) f ≃
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' (A , σ) (B , τ) f
equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type f =
equiv-tot
( λ p →
equiv-tot
( λ q →
equiv-product
( equiv-left-transpose-eq-concat' _ _ _ ∘e equiv-inv _ _)
( equiv-left-transpose-eq-concat' _ _ _ ∘e equiv-inv _ _)))

module _
{l1 l2 : Level}
(A : Pointed-Type l1)
(B : Pointed-Type l2)
(σ@(a1 , a2 , r1 , r2) : structure-Hatcher-Acyclic-Type A)
(f : A →∗ B)
where

is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' :
is-torsorial
( λ τ →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' (A , σ) (B , τ) f)
is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' =
is-torsorial-Eq-structure
( is-torsorial-Id (map-Ω f a1)) ((map-Ω f a1) , refl)
( is-torsorial-Eq-structure
( is-torsorial-Id (map-Ω f a2)) ((map-Ω f a2) , refl)
( is-torsorial-Eq-structure
( is-torsorial-Id _)
( _ , refl)
( is-torsorial-Id _)))

abstract
is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type :
is-torsorial
( λ τ →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type (A , σ) (B , τ) f)
is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type =
is-contr-equiv
( Σ ( structure-Hatcher-Acyclic-Type B)
( λ τ →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type'
( A , σ)
( B , τ)
( f)))
( equiv-tot
( λ τ →
equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
( A , σ)
( B , τ)
( f)))
( is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type')


### Characterization of pointed maps out of Hatcher's acyclic type

For the initial Hatcher acyclic algebra A and any pointed type B, we exhibit an equivalence (A →∗ B) ≃ structure-Hatcher-Acyclic-Type B.

We first show that for any Hatcher acyclic algebra A (so not necessarily the initial one) and a pointed type B, a pointed map f : A →∗ B induces a Hatcher acyclic structure on B. Moreover, with this induced structure, the map f becomes a homomorphism of Hatcher acyclic algebras.

module _
{l1 l2 : Level}
(A : Pointed-Type l1)
(B : Pointed-Type l2)
(σ@(a1 , a2 , r1 , r2) : structure-Hatcher-Acyclic-Type A)
where

map-Ω-structure-Hatcher-Acyclic-Type :
(f : A →∗ B) →
( power-nat-Ω 5 B (map-Ω f a1) ＝
power-nat-Ω 3 B (map-Ω f a2)) ×
( power-nat-Ω 3 B (map-Ω f a2) ＝
power-nat-Ω 2 B (mul-Ω B (map-Ω f a1) (map-Ω f a2)))
pr1 (map-Ω-structure-Hatcher-Acyclic-Type f) =
inv (map-power-nat-Ω 5 f a1) ∙ (ap (map-Ω f) r1 ∙ map-power-nat-Ω 3 f a2)
pr2 (map-Ω-structure-Hatcher-Acyclic-Type f) =
inv (map-power-nat-Ω 3 f a2) ∙
( ap (map-Ω f) r2 ∙
( map-power-nat-Ω 2 f (a1 ∙ a2) ∙
ap (power-nat-Ω 2 B) (preserves-mul-map-Ω f)))

structure-Hatcher-Acyclic-Type-pointed-map :
(A →∗ B) → structure-Hatcher-Acyclic-Type B
pr1 (structure-Hatcher-Acyclic-Type-pointed-map f) = map-Ω f a1
pr1 (pr2 (structure-Hatcher-Acyclic-Type-pointed-map f)) = map-Ω f a2
(pr2 (pr2 (structure-Hatcher-Acyclic-Type-pointed-map f))) =
map-Ω-structure-Hatcher-Acyclic-Type f

hom-algebra-Hatcher-Acyclic-Type-pointed-map' :
(f : A →∗ B) →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type'
( A , σ)
( B , structure-Hatcher-Acyclic-Type-pointed-map f)
( f)
pr1 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f) = refl
pr1 (pr2 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f)) = refl
pr1 (pr2 (pr2 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f))) =
ap-binary
( λ p q → inv p ∙ (ap (map-Ω f) r1 ∙ q))
( right-unit {p = map-power-nat-Ω 5 f a1})
( right-unit)
pr2 (pr2 (pr2 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f))) =
ap-binary
( λ p q →
inv p ∙
( ap (map-Ω f) r2 ∙
( map-power-nat-Ω 2 f (a1 ∙ a2) ∙ ap (power-nat-Ω 2 B) q)))
( right-unit {p = map-power-nat-Ω 3 f a2})
( right-unit {p = preserves-mul-map-Ω f})

hom-algebra-Hatcher-Acyclic-Type-pointed-map :
(f : A →∗ B) →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
( A , σ)
( B , structure-Hatcher-Acyclic-Type-pointed-map f)
( f)
hom-algebra-Hatcher-Acyclic-Type-pointed-map f =
map-inv-equiv
( equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
( A , σ)
( B , structure-Hatcher-Acyclic-Type-pointed-map f)
( f))
( hom-algebra-Hatcher-Acyclic-Type-pointed-map' f)

is-equiv-structure-Hatcher-Acyclic-Type-pointed-map :
is-initial-algebra-Hatcher-Acyclic-Type (A , σ) →
is-equiv structure-Hatcher-Acyclic-Type-pointed-map
is-equiv-structure-Hatcher-Acyclic-Type-pointed-map i =
is-equiv-htpy-equiv
( equivalence-reasoning
A →∗ B
≃ Σ ( A →∗ B)
( λ f →
Σ ( structure-Hatcher-Acyclic-Type B)
( λ τ →
is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
( A , σ)
( B , τ)
( f)))
by inv-right-unit-law-Σ-is-contr
( λ f →
is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
( A)
( B)
( σ)
( f))
≃ Σ ( structure-Hatcher-Acyclic-Type B)
( λ τ → hom-algebra-Hatcher-Acyclic-Type (A , σ) (B , τ))
by equiv-left-swap-Σ
≃ structure-Hatcher-Acyclic-Type B
by equiv-pr1 (λ τ → i (B , τ)))
( λ f →
ap
( pr1)
( inv
( contraction
( is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type A B
( σ)
( f))
( structure-Hatcher-Acyclic-Type-pointed-map f ,
hom-algebra-Hatcher-Acyclic-Type-pointed-map f))))

equiv-pointed-map-Hatcher-Acyclic-Type :
is-initial-algebra-Hatcher-Acyclic-Type (A , σ) →
(A →∗ B) ≃ structure-Hatcher-Acyclic-Type B
pr1 (equiv-pointed-map-Hatcher-Acyclic-Type i) =
structure-Hatcher-Acyclic-Type-pointed-map
pr2 (equiv-pointed-map-Hatcher-Acyclic-Type i) =
is-equiv-structure-Hatcher-Acyclic-Type-pointed-map i


### Hatcher's acyclic type is acyclic

Proof: For the Hatcher acyclic type A, and any pointed type X, we have

 (Σ A →∗ X) ≃ (A →∗ Ω X) ≃ structure-Hatcher-Acyclic-Type (Ω X),


where the first equivalence is the suspension-loop space adjunction, the second equivalence was just proven above, and the latter type is contractible, as shown by is-contr-structure-Hatcher-Acyclic-Type-Ω.

Hence, the suspension Σ A of A satisfies the universal property of contractible types with respect to pointed types and maps, and hence must be contractible.

module _
{l1 : Level}
((A , σ) : algebra-Hatcher-Acyclic-Type l1)
where

is-acyclic-is-initial-algebra-Hatcher-Acyclic-Type :
is-initial-algebra-Hatcher-Acyclic-Type (A , σ) →
is-acyclic (type-Pointed-Type A)
is-acyclic-is-initial-algebra-Hatcher-Acyclic-Type i =
is-contr-universal-property-contr-Pointed-Type
( suspension-Pointed-Type A)
( λ X →
is-contr-equiv
( structure-Hatcher-Acyclic-Type (Ω X))
( ( equiv-pointed-map-Hatcher-Acyclic-Type A (Ω X) σ i) ∘e
( is-contr-structure-Hatcher-Acyclic-Type-Ω X))


ConceptFile
Acyclic mapssynthetic-homotopy-theory.acyclic-maps
Acyclic typessynthetic-homotopy-theory.acyclic-types
Acyclic undirected graphsgraph-theory.acyclic-undirected-graphs
Braceletsunivalent-combinatorics.bracelets
The category of cyclic ringsring-theory.category-of-cyclic-rings
The circlesynthetic-homotopy-theory.circle
Connected set bundles over the circlesynthetic-homotopy-theory.connected-set-bundles-circle
Cyclic finite typesunivalent-combinatorics.cyclic-finite-types
Cyclic groupsgroup-theory.cyclic-groups
Cyclic higher groupshigher-group-theory.cyclic-higher-groups
Cyclic ringsring-theory.cyclic-rings
Cyclic typesstructured-types.cyclic-types
Euler's totient functionelementary-number-theory.eulers-totient-function
Finitely cyclic mapselementary-number-theory.finitely-cyclic-maps
Generating elements of groupsgroup-theory.generating-elements-groups
Hatcher's acyclic typesynthetic-homotopy-theory.hatchers-acyclic-type
Homomorphisms of cyclic ringsring-theory.homomorphisms-cyclic-rings
Infinite cyclic typessynthetic-homotopy-theory.infinite-cyclic-types
Multiplicative units in the standard cyclic ringselementary-number-theory.multiplicative-units-standard-cyclic-rings
Necklacesunivalent-combinatorics.necklaces
Polygonsgraph-theory.polygons
The poset of cyclic ringsring-theory.poset-of-cyclic-rings
Standard cyclic groups (ℤ/k)elementary-number-theory.standard-cyclic-groups
Standard cyclic rings (ℤ/k)elementary-number-theory.standard-cyclic-rings