一点犯愁论笔记

(请求一个数学tag x (超小声(

这是从senioria的blog里转来的一点用agda做犯愁论习题的碎碎念… x x (超小声(
很零碎而且很不成体系警告… x x (超小声(
(反正也没人看 x (超小声(

代码确实很一次性… qaq… 不过毕竟确实是一次性代码, 所以… x x (超小声(缩成球(

Premable

module chap-1-3 where

open import Categories.Category using (Category)
open import Categories.Functor using (Functor)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper)
open import Categories.Morphism using (Iso; IsIso)
import Categories.Morphism.Reasoning as MR
open import Level
open import Data.Product using (Σ-syntax; proj₁; proj₂; _×_) renaming (_,_ to ⟨_,_⟩)

private variable
  l-o l-l l-e : Level

Problems

1.3.26: Lemma 1.3.11

module lemma-1-3-11 {A B : Category l-o l-l l-e} {F G : Functor A B} where
  private
    module A = Category A
    module B = Category B
    module F = Functor F
    module G = Functor G
    module NI = NaturalIsomorphism
    module NT = NaturalTransformation

  cis : ∀ (α : NaturalIsomorphism F G) → ∀ {a : A.Obj} → (IsIso B (NT.η (NI.F⇒G α) a))
  cis α {a} = record
          { inv = NT.η α.F⇐G a
          ; iso = α.iso a
          }
      where
      module α = NaturalIsomorphism α
  trans : ∀ (α : NaturalTransformation F G) → (∀ {a : A.Obj} → IsIso B (NT.η α a)) → NaturalIsomorphism F G
  trans α iso = record
                { F⇒G = α
                ; F⇐G = ntHelper
                  record
                  { η = λ a → iso.inv
                  ; commute = commute
                  }
                ; iso = λ a → iso.iso
                }
    where
    module iso {a} = IsIso (iso {a})
    module α = NaturalTransformation α
    open Category B
    open Category.HomReasoning B
    open MR B

    commute : ∀ {a b : A.Obj} (f : a A.⇒ b) → iso.inv ∘ G.F₁ f ≈ F.F₁ f ∘ iso.inv
    commute {a} {b} f =
            begin iso.inv ∘ G.F₁ f ≈˘⟨ refl⟩∘⟨ cancelʳ (Iso.isoʳ iso.iso) ⟩
            iso.inv ∘ (G.F₁ f ∘ α.η a) ∘ iso.inv ≈˘⟨ refl⟩∘⟨ α.commute f ⟩∘⟨refl ⟩
            iso.inv ∘ ((α.η b ∘ F.F₁ f) ∘ iso.inv) ≈⟨ sym-assoc ⟩
            (iso.inv ∘ (α.η b ∘ F.F₁ f)) ∘ iso.inv ≈⟨ cancelˡ (Iso.isoˡ iso.iso) ⟩∘⟨refl ⟩
            F.F₁ f ∘ iso.inv ∎

1.3.32: equivalence functor iff faithful, full, and essentially surjective

不能摆烂了好可恶 x (超小声(被打死(((((

先定义一下那些性质:

module prop-1-3-18 where
  open Categories.Functor renaming (id to f-id)
  import Function

  record Equivalence {l-a l-b l-c} {A B : Category l-a l-b l-c} (F : Functor A B) : Set (l-a ⊔ l-b ⊔ l-c) where
    field
      G : Functor B A
      G∘F : NaturalIsomorphism (G ∘F F) f-id
      F∘G : NaturalIsomorphism (F ∘F G) f-id
    module G∘F = NaturalIsomorphism G∘F
    module F∘G = NaturalIsomorphism F∘G
    module F = Functor F
    module G = Functor G

正方向的证明:

  module cis-faithful {A B : Category l-o l-l l-e} {F : Functor A B} where
    module A = Category A
    module B = Category B
    module F = Functor F
    open A
    open A.HomReasoning
    open MR A

    cis-faithful : Equivalence F → ∀ {a b : A.Obj} {f g : a A.⇒ b} → F.₁ f B.≈ F.₁ g → f A.≈ g
    cis-faithful record { G = G ; G∘F = G∘F ; F∘G = F∘G } {a} {b} {f} {g} f≈g =
               begin f ≈˘⟨ cancelʳ (Iso.isoʳ (G∘F.iso a)) ⟩
               (f ∘ G∘F.⇒.η a) ∘ G∘F.⇐.η a ≈˘⟨ G∘F.⇒.commute f ⟩∘⟨refl ⟩
               (G∘F.⇒.η b ∘ G.F₁ (F.₁ f)) ∘ G∘F.⇐.η a ≈⟨ assoc ⟩
               G∘F.⇒.η b ∘ ((G.F₁ (F.₁ f)) ∘ G∘F.⇐.η a) ≈⟨ refl⟩∘⟨ G∘F-f≈g ⟩∘⟨refl ⟩
               G∘F.⇒.η b ∘ ((G.F₁ (F.₁ g)) ∘ G∘F.⇐.η a) ≈˘⟨ refl⟩∘⟨ G∘F.⇐.commute g ⟩
               G∘F.⇒.η b ∘ (G∘F.⇐.η b ∘ g) ≈⟨ cancelˡ (Iso.isoʳ (G∘F.iso b)) ⟩
               g ∎
      where
      module G = Functor G
      module G∘F = NaturalIsomorphism G∘F
      G∘F-f≈g : G.₁ (F.₁ f) ≈ G.₁ (F.₁ g)
      G∘F-f≈g = G.F-resp-≈ f≈g
  open cis-faithful using (cis-faithful)

  module cis-full {A B : Category l-o l-l l-e} {F : Functor A B} where
    module A = Category A
    module B = Category B
    module F = Functor F
    open A using (_⇒_; _≈_; _∘_; assoc)
    open A.HomReasoning
    open MR A

    cis-full : Equivalence F → ∀ {a b : A.Obj} {g : F.F₀ a B.⇒ F.F₀ b} → Σ[ f ∈ a A.⇒ b ] F.F₁ f B.≈ g
    cis-full record { G = G ; G∘F = G∘F ; F∘G = F∘G } {a} {b} {g} =
             ⟨ f , cis-faithful (record { G = F ; G∘F = F∘G ; F∘G = G∘F }) G∘F/f≈G/g ⟩
      where
      module G = Functor G
      module G∘F = NaturalIsomorphism G∘F
      module F∘G = NaturalIsomorphism F∘G

      f : a A.⇒ b
      f = G∘F.⇒.η b A.∘ G.₁ g A.∘ G∘F.⇐.η a

      G∘F/f≈G/g : G.₁ (F.₁ f) A.≈ G.₁ g
      G∘F/f≈G/g =
                begin G.₁ (F.₁ f) ≈˘⟨ cancelˡ (Iso.isoˡ (G∘F.iso b)) ⟩
                G∘F.⇐.η b ∘ G∘F.⇒.η b ∘ G.₁ (F.₁ f) ≈⟨ refl⟩∘⟨ G∘F.⇒.commute f ⟩
                G∘F.⇐.η b ∘ f ∘ G∘F.⇒.η a ≈⟨ A.Equiv.refl ⟩
                G∘F.⇐.η b ∘ ((G∘F.⇒.η b ∘ (G.₁ g ∘ G∘F.⇐.η a)) ∘ G∘F.⇒.η a) ≈˘⟨ assoc ⟩
                (G∘F.⇐.η b ∘ (G∘F.⇒.η b ∘ (G.₁ g ∘ G∘F.⇐.η a))) ∘ G∘F.⇒.η a ≈⟨ cancelˡ (Iso.isoˡ (G∘F.iso b)) ⟩∘⟨refl ⟩
                (G.₁ g ∘ G∘F.⇐.η a) ∘ G∘F.⇒.η a ≈⟨ cancelʳ (Iso.isoˡ (G∘F.iso a)) ⟩
                G.₁ g ∎
  open cis-full using (cis-full)

  module cis-essen-surj {A B : Category l-o l-l l-e} {F : Functor A B} where
    module A = Category A
    module B = Category B
    module F = Functor F
    open A using (_⇒_; _≈_; _∘_; assoc)
    open Categories.Morphism B using (_≅_)

    cis-essen-surj : Equivalence F → ∀ {a′ : B.Obj} → Σ[ a ∈ A.Obj ] (F.F₀ a ≅ a′)
    cis-essen-surj record { G = G ; G∘F = G∘F ; F∘G = F∘G } {a′} =
                   ⟨ G.₀ a′ , record { from = F∘G.⇒.η a′ ; to = F∘G.⇐.η a′ ; iso = F∘G.iso a′ } ⟩
      where
      module G = Functor G
      module G∘F = NaturalIsomorphism G∘F
      module F∘G = NaturalIsomorphism F∘G
  open cis-essen-surj using (cis-essen-surj)

反方向的证明:

  record trans {l-a l-b l-c} {A B : Category l-a l-b l-c} {F : Functor A B} : Set (l-a ⊔ l-b ⊔ l-c) where
    module A = Category A
    module B = Category B
    module F = Functor F
    open Categories.Morphism B using (_≅_)

    field
      faithful : ∀ {a b : A.Obj} {f g : a A.⇒ b} → F.₁ f B.≈ F.₁ g → f A.≈ g
      full : ∀ {a b : A.Obj} {g : F.F₀ a B.⇒ F.F₀ b} → Σ[ f ∈ a A.⇒ b ] F.F₁ f B.≈ g
      essen-surj : ∀ {a′ : B.Obj} → Σ[ a ∈ A.Obj ] (F.F₀ a ≅ a′)

    G₀ : ∀ (a′ : B.Obj) → A.Obj
    G₀ a′ = proj₁ (essen-surj {a′})
    G₀-iso : ∀ {a′ : B.Obj} → F.₀ (G₀ a′) ≅ a′
    G₀-iso {a′} = proj₂ (essen-surj {a′})
    module G₀-iso {a′} = _≅_ (G₀-iso {a′})
    G₁ : ∀ {a′ b′} → a′ B.⇒ b′ → G₀ a′ A.⇒ G₀ b′
    G₁ {a′} {b′} f′ = proj₁ (full {g = G₀-iso.to B.∘ f′ B.∘ G₀-iso.from})
    G₁-iso : ∀ {a′ b′} {f′ : a′ B.⇒ b′} → F.₁ (G₁ f′) B.≈ G₀-iso.to B.∘ f′ B.∘ G₀-iso.from
    G₁-iso {a′} {b′} {f′} = proj₂ (full)

    G : Functor B A
    G = record
          { F₀ = G₀
          ; F₁ = G₁
          ; identity = faithful identity
          ; homomorphism = faithful homomorphism
          ; F-resp-≈ = λ f≈g → faithful (resp-≈ f≈g)
          }
      where
      open Category B
      open B.HomReasoning
      open MR B
      identity : ∀ {a′} → F.₁ (G₁ {a′} B.id) B.≈ F.₁ A.id
      identity {a′} =
               begin F.₁ (G₁ B.id) ≈⟨ G₁-iso ⟩
               G₀-iso.to ∘ B.id ∘ G₀-iso.from ≈˘⟨ refl⟩∘⟨ lemma-binid ⟩∘⟨refl ⟩
               G₀-iso.to ∘ (G₀-iso.from ∘ B.id ∘ G₀-iso.to) ∘ G₀-iso.from ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ F.identity ⟩∘⟨refl) ⟩∘⟨refl ⟩
               G₀-iso.to ∘ (G₀-iso.from ∘ F.₁ A.id ∘ G₀-iso.to) ∘ G₀-iso.from ≈⟨ sym-assoc ⟩
               (G₀-iso.to ∘ (G₀-iso.from ∘ F.₁ A.id ∘ G₀-iso.to)) ∘ G₀-iso.from ≈⟨ cancelˡ (Iso.isoˡ G₀-iso.iso) ⟩∘⟨refl ⟩
               (F.₁ A.id ∘ G₀-iso.to) ∘ G₀-iso.from ≈⟨ cancelʳ (Iso.isoˡ G₀-iso.iso) ⟩
               F.₁ A.id ∎
        where
        lemma-binid : G₀-iso.from ∘ B.id ∘ G₀-iso.to ≈ B.id
        lemma-binid =
                    begin G₀-iso.from ∘ B.id ∘ G₀-iso.to ≈⟨ refl⟩∘⟨ B.identityˡ ⟩
                    G₀-iso.from ∘ G₀-iso.to ≈⟨ Iso.isoʳ G₀-iso.iso ⟩
                    B.id ∎

      homomorphism : ∀ {a′ b′ c′} {f : a′ B.⇒ b′} {g : b′ B.⇒ c′} → F.₁ (G₁ (g B.∘ f)) B.≈ F.₁ (G₁ g A.∘ G₁ f)
      homomorphism {f = f} {g} =
                   begin F.₁ (G₁ (g ∘ f)) ≈⟨ G₁-iso ⟩
                   G₀-iso.to ∘ (g ∘ f) ∘ G₀-iso.from ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ B.identityˡ) ⟩∘⟨refl ⟩
                   G₀-iso.to ∘ (g ∘ id ∘ f) ∘ G₀-iso.from ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ Iso.isoʳ G₀-iso.iso ⟩∘⟨refl) ⟩∘⟨refl ⟩
                   G₀-iso.to ∘ (g ∘ (G₀-iso.from ∘ G₀-iso.to) ∘ f) ∘ G₀-iso.from ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ assoc) ⟩∘⟨refl ⟩
                   G₀-iso.to ∘ (g ∘ (G₀-iso.from ∘ (G₀-iso.to ∘ f))) ∘ G₀-iso.from ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩
                   G₀-iso.to ∘ ((g ∘ G₀-iso.from) ∘ (G₀-iso.to ∘ f)) ∘ G₀-iso.from ≈⟨ refl⟩∘⟨ assoc ⟩
                   G₀-iso.to ∘ (g ∘ G₀-iso.from) ∘ (G₀-iso.to ∘ f) ∘ G₀-iso.from ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
                   G₀-iso.to ∘ (g ∘ G₀-iso.from) ∘ (G₀-iso.to ∘ f ∘ G₀-iso.from) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ G₁-iso ⟩
                   G₀-iso.to ∘ (g ∘ G₀-iso.from) ∘ F.₁ (G₁ f) ≈⟨ sym-assoc ⟩
                   (G₀-iso.to ∘ (g ∘ G₀-iso.from)) ∘ F.₁ (G₁ f) ≈˘⟨ G₁-iso ⟩∘⟨refl ⟩
                   F.₁ (G₁ g) ∘ F.₁ (G₁ f) ≈˘⟨ F.homomorphism ⟩
                   F.₁ (G₁ g A.∘ G₁ f) ∎

      resp-≈ : ∀ {a′ b′} {f g : a′ B.⇒ b′} → f ≈ g → F.₁ (G₁ f) ≈ F.₁ (G₁ g)
      resp-≈ {f = f} {g} f≈g =
             begin F.₁ (G₁ f) ≈⟨ G₁-iso ⟩
             G₀-iso.to ∘ f ∘ G₀-iso.from ≈⟨ refl⟩∘⟨ f≈g ⟩∘⟨refl ⟩
             G₀-iso.to ∘ g ∘ G₀-iso.from ≈˘⟨ G₁-iso ⟩
             F.₁ (G₁ g) ∎

    F∘G-id : NaturalIsomorphism (F ∘F G) f-id
    F∘G-id = niHelper (record
             { η = λ a → G₀-iso.from
             ; η⁻¹ = λ a → G₀-iso.to
             ; commute = commute
             ; iso = λ a → G₀-iso.iso
             })
      where
      open Category B
      open B.HomReasoning
      open MR B
      commute : ∀ {a b} (f : a B.⇒ b) → G₀-iso.from ∘ F.₁ (G₁ f) ≈ f ∘ G₀-iso.from
      commute f =
              begin G₀-iso.from ∘ F.₁ (G₁ f) ≈⟨ refl⟩∘⟨ G₁-iso ⟩
              G₀-iso.from ∘ (G₀-iso.to ∘ f ∘ G₀-iso.from) ≈⟨ cancelˡ (Iso.isoʳ G₀-iso.iso) ⟩
              f ∘ G₀-iso.from ∎
    module F∘G-id = NaturalIsomorphism F∘G-id

    G∘F-id : NaturalIsomorphism (G ∘F F) f-id
    G∘F-id = niHelper (record
             { η = λ a → proj₁ (full {g = G₀-iso.from})
             ; η⁻¹ = λ a → proj₁ (full {g = G₀-iso.to})
             ; commute = λ f → faithful commute
             ; iso = λ a → record { isoˡ = faithful (iso G₀-iso.isoˡ) ; isoʳ = faithful (iso G₀-iso.isoʳ) }
             })
      where
      open Category B
      open B.HomReasoning
      open MR B
      module G = Functor G
      commute : ∀ {a b} {f : a A.⇒ b} → F.₁ (proj₁ full A.∘ G.₁ (F.₁ f)) ≈ F.₁ (f A.∘ proj₁ full)
      commute {a} {b} {f = f} =
              begin F.₁ (proj₁ full A.∘ G.₁ (F.₁ f)) ≈⟨ F.homomorphism ⟩
              F.₁ (proj₁ full) ∘ F.₁ (G.₁ (F.₁ f)) ≈⟨ proj₂ full ⟩∘⟨refl ⟩
              G₀-iso.from ∘ F.₁ (G.₁ (F.₁ f)) ≈⟨ F∘G-id.⇒.commute (F.₁ f) ⟩
              F.₁ f ∘ G₀-iso.from ≈˘⟨ refl⟩∘⟨ proj₂ full ⟩
              F.₁ f ∘ F.₁ (proj₁ full) ≈˘⟨ F.homomorphism ⟩
              F.₁ (f A.∘ proj₁ full) ∎
      iso : ∀ {a b} {f : F.₀ a B.⇒ F.₀ b} {g : F.₀ b B.⇒ F.₀ a} → g ∘ f ≈ B.id
            → F.₁ (proj₁ (full {g = g}) A.∘ proj₁ (full {g = f})) ≈ F.₁ (A.id {a})
      iso {f = f} {g = g} g∘f≈id =
          begin F.₁ (proj₁ full A.∘ proj₁ full) ≈⟨ F.homomorphism ⟩
          F.₁ (proj₁ full) ∘ F.₁ (proj₁ full) ≈⟨ proj₂ full ⟩∘⟨refl ⟩
          g ∘ F.₁ (proj₁ full) ≈⟨ refl⟩∘⟨ proj₂ full ⟩
          g ∘ f ≈⟨ g∘f≈id ⟩
          B.id ≈˘⟨ F.identity ⟩
          F.₁ A.id ∎

1.3.34: category equivalence is equivalence relation

(这个在库里其实有, 而且代码确实挺简单的… (超小声(
因为口胡出来比较容易所以咕咕了 (!) x (超小声(被打死((((((

(The Rest)

因为懒得找记号所以咕咕了… >< (超小声(缩成球(

Premable

module chap-2-1 where

open import Categories.Category using (Category)
open import Categories.Functor using (Functor)
import Categories.Morphism.Reasoning as MR
open import Level
open import Data.Product using (Σ-syntax; proj₁; proj₂; _×_) renaming (_,_ to ⟨_,_⟩)

private variable
  l-o l-l l-e : Level

Adjoints in the library is defined in a different way as the book,
with the naturality between objects.
Due to Senioriae lack to essential knowledge, to avoid cyclic proof,
and to agree with the definition in the book,
we define adjoints in another way, focusing on the naturality between arrows.

record Adjoint {A B : Category l-o l-l l-e} (F : Functor A B) (G : Functor B A)
               : Set (l-o ⊔ l-l ⊔ l-e) where
  private
    module A = Category A
    module B = Category B
    module F = Functor F
    module G = Functor G

  field
    A⇒B : ∀ {a b} → a A.⇒ G.₀ b → F.₀ a B.⇒ b
    B⇒A : ∀ {a b} → F.₀ a B.⇒ b → a A.⇒ G.₀ b

  field
    inv-A : ∀ {a b} {f : a A.⇒ G.₀ b} → B⇒A (A⇒B f) A.≈ f
    inv-B : ∀ {a b} {f : F.₀ a B.⇒ b} → A⇒B (B⇒A f) B.≈ f
    A⇒B-distrib : ∀ {a b c} {f : a A.⇒ b} {g : b A.⇒ G.₀ c} → A⇒B (g A.∘ f) B.≈ A⇒B g B.∘ F.₁ f
    B⇒A-distrib : ∀ {a b c} {f : F.₀ a B.⇒ b} {g : b B.⇒ c} → B⇒A (g B.∘ f) A.≈ G.₁ g A.∘ B⇒A f
    A⇒B-resp-≈ : ∀ {a b} {f g : a A.⇒ G.₀ b} → f A.≈ g → A⇒B f B.≈ A⇒B g
    B⇒A-resp-≈ : ∀ {a b} {f g : F.₀ a B.⇒ b} → f B.≈ g → B⇒A f A.≈ B⇒A g

Problems

2.1.15: preservation of left and right adjoints

Before we discuss the properties of initials and terminals,
again, we should define them.
The definitions are quite trivial and clear.

record Initial {A : Category l-l l-o l-e} (i : Category.Obj A) : Set (l-l ⊔ l-o ⊔ l-e) where
  open Category A
  field
    map : ∀ (a : Obj) → i ⇒ a
    uniq : ∀ {a} {f g : i ⇒ a} → f ≈ g

record Terminal {A : Category l-l l-o l-e} (t : Category.Obj A) : Set (l-l ⊔ l-o ⊔ l-e) where
  open Category A
  field
    map : ∀ (a : Obj) → a ⇒ t
    uniq : ∀ {a} {f g : a ⇒ t} → f ≈ g

The proof to the initials:

module prob-2-1-15 {A B : Category l-l l-o l-e} {F : Functor A B} {G : Functor B A} where
  module A = Category A
  module B = Category B
  module F = Functor F
  module G = Functor G

  resp-init : Adjoint F G → ∀ {i} → Initial {A = A} i → Initial {A = B} (F.₀ i)
  resp-init adj init = record
            { map = λ a → adj.A⇒B (init.map (G.₀ a))
            ; uniq = λ {a} {f} {g} → begin
                   f ≈˘⟨ adj.inv-B ⟩
                   adj.A⇒B (adj.B⇒A f) ≈⟨ adj.A⇒B-resp-≈ init.uniq ⟩
                   adj.A⇒B (adj.B⇒A g) ≈⟨ adj.inv-B ⟩
                   g ∎
            }
    where
    module adj = Adjoint adj
    module init = Initial init
    open MR B
    open B.HomReasoning

The proof to the terminals is similar:

  resp-term : Adjoint F G → ∀ {t} → Terminal {A = B} t → Terminal {A = A} (G.₀ t)
  resp-term adj term = record
            { map = λ a → adj.B⇒A (term.map (F.₀ a))
            ; uniq = λ {a} {f} {g} → begin
                   f ≈˘⟨ adj.inv-A ⟩
                   adj.B⇒A (adj.A⇒B f) ≈⟨ adj.B⇒A-resp-≈ term.uniq ⟩
                   adj.B⇒A (adj.A⇒B g) ≈⟨ adj.inv-A ⟩
                   g ∎
            }
    where
    module adj = Adjoint adj
    module term = Terminal term
    open MR A
    open A.HomReasoning

title: 2.2 Adjunctions via units and counits

This chapter is kinda ease since adjunctions in the library
are defined with units and counits.

Premable

module chap-2-2 where

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; _∘F_) renaming (id to F-id)
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper; IsNI)
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MR
open import Level
open import Data.Product using (Σ-syntax; proj₁; proj₂; _×_) renaming (_,_ to ⟨_,_⟩)
open import Categories.Adjoint using (Adjoint)
open import Categories.Category.SubCategory using (FullSubCategory; SubCat)

private variable
  l-o l-l l-e : Level

Problems

2.2.11: Equivalence on full subcategories definied by η_A

Senioria don’t know how to qualify the object set of A to its subset
fulfilling the condition, so the formal proof is omitted ;;><;;

module prob-2-2-11 {A B : Category l-o l-l l-e} {F : Functor A B} {G : Functor B A}
                   {adj : Adjoint F G} where
  module A = Category A
  module B = Category B
  module F = Functor F
  module G = Functor G
  module adj = Adjoint adj

  -- TODO: ??

2.2.12: Right adjoint is full and faithful iff counit is isomorphism

module prob-2-2-12 {A B : Category l-o l-l l-e} {F : Functor A B} {G : Functor B A}
                   {adj : Adjoint F G} where
  record LHS {A B : Category l-o l-l l-e} (F : Functor A B) : Set (l-o ⊔ l-l ⊔ l-e) where
    private
      module A = Category A
      module B = Category B
      module F = Functor F
    field
      faithful : ∀ {a b : A.Obj} {f g : a A.⇒ b} → F.₁ f B.≈ F.₁ g → f A.≈ g
      full : ∀ {a b : A.Obj} {g : F.₀ a B.⇒ F.₀ b} → Σ[ f ∈ a A.⇒ b ] F.₁ f B.≈ g

  module A = Category A
  module B = Category B
  module F = Functor F
  module G = Functor G
  module adj = Adjoint adj

  cis : LHS G → NaturalIsomorphism (F ∘F G) F-id
  cis (record { faithful = faithful ; full = full }) = niHelper (record
    { η = adj.counit.η
    ; η⁻¹ = η⁻¹
    ; commute = adj.counit.commute
    ; iso = λ a → record
      { isoˡ = isoˡ
      ; isoʳ = faithful isoʳ
      }
    })
    where
    η⁻¹ : ∀ (a : B.Obj) → a B.⇒ F.₀ (G.₀ a)
    η⁻¹ a = proj₁ (full {g = adj.unit.η (G.₀ a)})
    isoˡ : ∀ {a} → η⁻¹ a B.∘ adj.counit.η a B.≈ B.id
    isoˡ {a} = begin
         η⁻¹ a ∘ adj.counit.η a ≈˘⟨ adj.counit.commute (η⁻¹ a) ⟩
         adj.counit.η (F.₀ (G.₀ a)) ∘ F.₁ (G.₁ (η⁻¹ a)) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (proj₂ full) ⟩
         adj.counit.η (F.₀ (G.₀ a)) ∘ F.₁ (adj.unit.η (G.₀ a)) ≈⟨ adj.zig ⟩
         B.id ∎
      where
      open B
      open MR B
      open B.HomReasoning
    isoʳ : ∀ {a} → G.₁ (adj.counit.η a B.∘ η⁻¹ a) A.≈ G.₁ B.id
    isoʳ {a} = begin
         G.₁ (adj.counit.η a B.∘ η⁻¹ a) ≈⟨ G.homomorphism ⟩
         G.₁ (adj.counit.η a) ∘ G.₁ (η⁻¹ a) ≈⟨ refl⟩∘⟨ proj₂ full ⟩
         G.₁ (adj.counit.η a) ∘ adj.unit.η (G.₀ a) ≈⟨ adj.zag ⟩
         A.id ≈˘⟨ G.identity ⟩
         G.₁ B.id ∎
      where
      open A
      open MR A
      open A.HomReasoning

  trans : IsNI adj.counit → LHS G
  trans ni = record
    { faithful = faithful
    ; full = full
    }
    where
    module ni = IsNI ni
    module unit = adj.unit
    module counit = adj.counit
    module counit⁻¹ = NaturalTransformation ni.F⇐G
    module iso {a} = Morphism.Iso (ni.iso a)
    faithful : ∀ {a b} {f g : a B.⇒ b} → G.₁ f A.≈ G.₁ g → f B.≈ g
    faithful {a} {b} {f} {g} Gf≈g = begin
             f ≈˘⟨ cancelʳ iso.isoʳ ⟩
             (f ∘ counit.η a) ∘ counit⁻¹.η a ≈˘⟨ counit.commute f ⟩∘⟨refl ⟩
             (counit.η b ∘ F.₁ (G.₁ f)) ∘ counit⁻¹.η a ≈⟨ (refl⟩∘⟨ F.F-resp-≈ Gf≈g) ⟩∘⟨refl ⟩
             (counit.η b ∘ F.₁ (G.₁ g)) ∘ counit⁻¹.η a ≈⟨ counit.commute g ⟩∘⟨refl ⟩
             (g ∘ counit.η a) ∘ counit⁻¹.η a ≈⟨ cancelʳ iso.isoʳ ⟩
             g ∎
      where
      open B
      open MR B
      open B.HomReasoning
    full : ∀ {a b} {g : G.₀ a A.⇒ G.₀ b} → Σ[ f ∈ a B.⇒ b ] G.₁ f A.≈ g
    full {a} {b} {g} = ⟨ f , f≈g ⟩
      where
      f : a B.⇒ b
      f = counit.η b B.∘ F.₁ g B.∘ counit⁻¹.η a
      f≈g : G.₁ f A.≈ g
      f≈g = begin
          G.₁ f ≈⟨ G.homomorphism ⟩
          G.₁ (counit.η b) ∘ G.₁ (F.₁ g B.∘ counit⁻¹.η a) ≈⟨ refl⟩∘⟨ G.homomorphism ⟩
          G.₁ (counit.η b) ∘ G.₁ (F.₁ g) ∘ G.₁ (counit⁻¹.η a) ≈˘⟨ A.assoc ⟩
          (G.₁ (counit.η b) ∘ G.₁ (F.₁ g)) ∘ G.₁ (counit⁻¹.η a) ≈˘⟨ refl⟩∘⟨ cancelʳ adj.zag ⟩
          (G.₁ (counit.η b) ∘ G.₁ (F.₁ g)) ∘ (G.₁ (counit⁻¹.η a) ∘ G.₁ (counit.η a)) ∘ unit.η (G.₀ a)
            ≈⟨ refl⟩∘⟨ elimˡ (A.Equiv.sym G.homomorphism ○ G.F-resp-≈ iso.isoˡ ○ G.identity) ⟩
          (G.₁ (counit.η b) ∘ G.₁ (F.₁ g)) ∘ unit.η (G.₀ a) ≈⟨ A.assoc ⟩
          G.₁ (counit.η b) ∘ G.₁ (F.₁ g) ∘ unit.η (G.₀ a) ≈˘⟨ refl⟩∘⟨ unit.commute g ⟩
          G.₁ (counit.η b) ∘ unit.η (G.₀ b) ∘ g ≈⟨ cancelˡ adj.zag ⟩
          g ∎
        where
        open A
        open MR A
        open A.HomReasoning

(The rest)

咕咕咕咕 (超小声(被打死(((((((

3 Likes

(虽然, 发这种装点门面的东西有什么意义呢… (sigh… x x (超小声(

无所谓,我看不懂(