{-# OPTIONS --without-K --rewriting #-}
open import HoTT
module groups.HomSequence where
infix 15 _⊣|ᴳ
infixr 10 _→⟨_⟩ᴳ_
data HomSequence {i} : (G : Group i) (H : Group i) → Type (lsucc i) where
_⊣|ᴳ : (G : Group i) → HomSequence G G
_→⟨_⟩ᴳ_ : (G : Group i) {H K : Group i}
→ (G →ᴳ H) → HomSequence H K
→ HomSequence G K
HomSeq-++ : ∀ {i} {G H K : Group i}
→ HomSequence G H → HomSequence H K → HomSequence G K
HomSeq-++ (_ ⊣|ᴳ) seq = seq
HomSeq-++ (_ →⟨ φ ⟩ᴳ seq₁) seq₂ = _ →⟨ φ ⟩ᴳ HomSeq-++ seq₁ seq₂
HomSeq-snoc : ∀ {i} {G H K : Group i}
→ HomSequence G H → (H →ᴳ K) → HomSequence G K
HomSeq-snoc seq φ = HomSeq-++ seq (_ →⟨ φ ⟩ᴳ _ ⊣|ᴳ)
infix 15 _↓|ᴳ
infixr 10 _↓⟨_⟩ᴳ_
data HomSeqMap {i₀ i₁} : {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
→ HomSequence G₀ H₀ → HomSequence G₁ H₁
→ (G₀ →ᴳ G₁) → (H₀ →ᴳ H₁) → Type (lsucc (lmax i₀ i₁)) where
_↓|ᴳ : {G₀ : Group i₀} {G₁ : Group i₁} (ξ : G₀ →ᴳ G₁) → HomSeqMap (G₀ ⊣|ᴳ) (G₁ ⊣|ᴳ) ξ ξ
_↓⟨_⟩ᴳ_ : {G₀ H₀ K₀ : Group i₀} {G₁ H₁ K₁ : Group i₁}
→ {φ : G₀ →ᴳ H₀} {seq₀ : HomSequence H₀ K₀}
→ {ψ : G₁ →ᴳ H₁} {seq₁ : HomSequence H₁ K₁}
→ (ξG : G₀ →ᴳ G₁) {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
→ CommSquareᴳ φ ψ ξG ξH
→ HomSeqMap seq₀ seq₁ ξH ξK
→ HomSeqMap (G₀ →⟨ φ ⟩ᴳ seq₀) (G₁ →⟨ ψ ⟩ᴳ seq₁) ξG ξK
HomSeqMap-snoc : ∀ {i₀ i₁} {G₀ H₀ K₀ : Group i₀} {G₁ H₁ K₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{φ₀ : H₀ →ᴳ K₀} {φ₁ : H₁ →ᴳ K₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
→ HomSeqMap seq₀ seq₁ ξG ξH
→ CommSquareᴳ φ₀ φ₁ ξH ξK
→ HomSeqMap (HomSeq-snoc seq₀ φ₀) (HomSeq-snoc seq₁ φ₁) ξG ξK
HomSeqMap-snoc (ξG ↓|ᴳ) □ = ξG ↓⟨ □ ⟩ᴳ _ ↓|ᴳ
HomSeqMap-snoc (ξG ↓⟨ □₁ ⟩ᴳ seq) □₂ = ξG ↓⟨ □₁ ⟩ᴳ HomSeqMap-snoc seq □₂
is-seqᴳ-equiv : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
→ HomSeqMap seq₀ seq₁ ξG ξH
→ Type (lmax i₀ i₁)
is-seqᴳ-equiv (ξ ↓|ᴳ) = is-equiv (GroupHom.f ξ)
is-seqᴳ-equiv (ξ ↓⟨ _ ⟩ᴳ seq) = is-equiv (GroupHom.f ξ) × is-seqᴳ-equiv seq
is-seqᴳ-equiv-snoc : ∀ {i₀ i₁} {G₀ H₀ K₀ : Group i₀} {G₁ H₁ K₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{φ₀ : H₀ →ᴳ K₀} {φ₁ : H₁ →ᴳ K₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁} {ξK : K₀ →ᴳ K₁}
{seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
{cs : CommSquareᴳ φ₀ φ₁ ξH ξK}
→ is-seqᴳ-equiv seq-map → is-equiv (GroupHom.f ξK)
→ is-seqᴳ-equiv (HomSeqMap-snoc seq-map cs)
is-seqᴳ-equiv-snoc {seq-map = ξG ↓|ᴳ} ξG-is-equiv ξH-is-equiv = ξG-is-equiv , ξH-is-equiv
is-seqᴳ-equiv-snoc {seq-map = ξG ↓⟨ _ ⟩ᴳ seq} (ξG-is-equiv , seq-is-equiv) ξH-is-equiv =
ξG-is-equiv , is-seqᴳ-equiv-snoc seq-is-equiv ξH-is-equiv
private
is-seqᴳ-equiv-head : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
{seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
→ is-seqᴳ-equiv seq-map → is-equiv (GroupHom.f ξG)
is-seqᴳ-equiv-head {seq-map = ξ ↓|ᴳ} ise = ise
is-seqᴳ-equiv-head {seq-map = ξ ↓⟨ _ ⟩ᴳ _} ise = fst ise
is-seqᴳ-equiv-last : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
{seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
→ is-seqᴳ-equiv seq-map → is-equiv (GroupHom.f ξH)
is-seqᴳ-equiv-last {seq-map = ξ ↓|ᴳ} ise = ise
is-seqᴳ-equiv-last {seq-map = _ ↓⟨ _ ⟩ᴳ rest} (_ , rest-ise) = is-seqᴳ-equiv-last rest-ise
module is-seqᴳ-equiv {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
{seq-map : HomSeqMap seq₀ seq₁ ξG ξH}
(seq-map-is-equiv : is-seqᴳ-equiv seq-map) where
head = is-seqᴳ-equiv-head seq-map-is-equiv
last = is-seqᴳ-equiv-last seq-map-is-equiv
HomSeqEquiv : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
(seq₀ : HomSequence G₀ H₀) (seq₁ : HomSequence G₁ H₁)
(ξG : G₀ →ᴳ G₁) (ξH : H₀ →ᴳ H₁) → Type (lsucc (lmax i₀ i₁))
HomSeqEquiv seq₀ seq₁ ξG ξH = Σ (HomSeqMap seq₀ seq₁ ξG ξH) is-seqᴳ-equiv
HomSeqEquiv-inverse : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
(equiv : HomSeqEquiv seq₀ seq₁ ξG ξH)
→ HomSeqEquiv seq₁ seq₀
(GroupIso.g-hom (ξG , is-seqᴳ-equiv-head (snd equiv)))
(GroupIso.g-hom (ξH , is-seqᴳ-equiv-last (snd equiv)))
HomSeqEquiv-inverse ((ξ ↓|ᴳ) , ξ-ise) =
(GroupIso.g-hom (ξ , ξ-ise) ↓|ᴳ) , is-equiv-inverse ξ-ise
HomSeqEquiv-inverse ((ξ ↓⟨ □ ⟩ᴳ rest) , (ξ-ise , rest-ise)) =
(GroupIso.g-hom (ξ , ξ-ise)
↓⟨ CommSquareᴳ-inverse-v □ ξ-ise (is-seqᴳ-equiv-head rest-ise) ⟩ᴳ
fst rest-inverse-equiv) ,
is-equiv-inverse ξ-ise , snd rest-inverse-equiv
where
rest-inverse-equiv = HomSeqEquiv-inverse (rest , rest-ise)
private
hom-seq-map-index-type : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
→ ℕ → HomSeqMap seq₀ seq₁ ξG ξH → Type (lmax i₀ i₁)
hom-seq-map-index-type _ (_ ↓|ᴳ) = Lift ⊤
hom-seq-map-index-type O (_↓⟨_⟩ᴳ_ {φ = φ} {ψ = ψ} ξG {ξH} _ _)
= CommSquareᴳ φ ψ ξG ξH
hom-seq-map-index-type (S n) (_ ↓⟨ _ ⟩ᴳ seq-map)
= hom-seq-map-index-type n seq-map
abstract
hom-seq-map-index : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
(n : ℕ) (seq-map : HomSeqMap seq₀ seq₁ ξG ξH)
→ hom-seq-map-index-type n seq-map
hom-seq-map-index _ (_ ↓|ᴳ) = lift tt
hom-seq-map-index O (_ ↓⟨ □ ⟩ᴳ _) = □
hom-seq-map-index (S n) (_ ↓⟨ _ ⟩ᴳ seq-map)
= hom-seq-map-index n seq-map
private
hom-seq-equiv-index-type : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
→ ℕ → HomSeqMap seq₀ seq₁ ξG ξH → Type (lmax i₀ i₁)
hom-seq-equiv-index-type {ξG = ξG} O _ = is-equiv (GroupHom.f ξG)
hom-seq-equiv-index-type (S _) (_ ↓|ᴳ) = Lift ⊤
hom-seq-equiv-index-type (S n) (_ ↓⟨ _ ⟩ᴳ seq-map)
= hom-seq-equiv-index-type n seq-map
abstract
hom-seq-equiv-index : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
{seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
{ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
(n : ℕ) (seq-equiv : HomSeqEquiv seq₀ seq₁ ξG ξH)
→ hom-seq-equiv-index-type n (fst seq-equiv)
hom-seq-equiv-index O (seq-map , ise) = is-seqᴳ-equiv-head ise
hom-seq-equiv-index (S _) ((_ ↓|ᴳ) , _) = lift tt
hom-seq-equiv-index (S n) ((_ ↓⟨ _ ⟩ᴳ seq-map) , ise)
= hom-seq-equiv-index n (seq-map , snd ise)