Library HoTT.categories.Functor.Attributes
Require Import Category.Core Functor.Core HomFunctor Category.Morphisms Category.Dual Functor.Dual Category.Prod Functor.Prod NaturalTransformation.Core SetCategory.Core Functor.Composition.Core.
Require Import Basics.Overture Basics.Trunc hit.epi Types.Universe HSet hit.iso hit.Truncations UnivalenceImpliesFunext TruncType.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Local Open Scope category_scope.
Section full_faithful.
Context `{Funext}.
Variables C D : PreCategory.
Variable F : Functor C D.
Require Import Basics.Overture Basics.Trunc hit.epi Types.Universe HSet hit.iso hit.Truncations UnivalenceImpliesFunext TruncType.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Local Open Scope category_scope.
Section full_faithful.
Context `{Funext}.
Variables C D : PreCategory.
Variable F : Functor C D.
Natural transformation hom_C(─, ─) → hom_D(Fᵒᵖ(─), F(─))
TODO(JasonGross): Come up with a better name and location for this.
Definition induced_hom_natural_transformation
: NaturalTransformation (hom_functor C) (hom_functor D o (F^op, F)).
Proof.
refine (Build_NaturalTransformation
(hom_functor C)
(hom_functor D o (F^op, F))
(fun sd : object (C^op × C) ⇒
morphism_of F (s := _) (d := _))
_
).
abstract (
repeat (intros [] || intro);
simpl in *;
repeat (apply path_forall; intro);
simpl;
rewrite !composition_of;
reflexivity
).
Defined.
: NaturalTransformation (hom_functor C) (hom_functor D o (F^op, F)).
Proof.
refine (Build_NaturalTransformation
(hom_functor C)
(hom_functor D o (F^op, F))
(fun sd : object (C^op × C) ⇒
morphism_of F (s := _) (d := _))
_
).
abstract (
repeat (intros [] || intro);
simpl in *;
repeat (apply path_forall; intro);
simpl;
rewrite !composition_of;
reflexivity
).
Defined.
Class IsFaithful
:= is_faithful
: ∀ x y : C,
IsMonomorphism (induced_hom_natural_transformation (x, y)).
:= is_faithful
: ∀ x y : C,
IsMonomorphism (induced_hom_natural_transformation (x, y)).
Class IsFullyFaithful
:= is_fully_faithful
: ∀ x y : C,
IsIsomorphism (induced_hom_natural_transformation (x, y)).
:= is_fully_faithful
: ∀ x y : C,
IsIsomorphism (induced_hom_natural_transformation (x, y)).
Global Instance isfull_isfullyfaithful `{IsFullyFaithful}
: IsFull.
Proof.
intros ? ?; hnf in × |- .
typeclasses eauto.
Qed.
: IsFull.
Proof.
intros ? ?; hnf in × |- .
typeclasses eauto.
Qed.
Global Instance isfaithful_isfullyfaithful `{IsFullyFaithful}
: IsFaithful.
Proof.
intros ? ?; hnf in × |- .
typeclasses eauto.
Qed.
: IsFaithful.
Proof.
intros ? ?; hnf in × |- .
typeclasses eauto.
Qed.
Full * Faithful → Fully Faithful
We start with a helper method, which assumes that epi * mono → iso, and ten prove this assumption
Lemma isfullyfaithful_isfull_isfaithful_helper `{IsFull} `{IsFaithful}
(H' : ∀ x y (m : morphism set_cat x y),
IsEpimorphism m
→ IsMonomorphism m
→ IsIsomorphism m)
: IsFullyFaithful.
Proof.
intros ? ?; hnf in × |- .
apply H'; eauto.
Qed.
End full_faithful.
Section fully_faithful_helpers.
Context `{ua : Univalence}.
Variables x y : hSet.
Variable m : x → y.
Lemma isisomorphism_isequiv_set_cat
`{H' : IsEquiv _ _ m}
: IsIsomorphism (m : morphism set_cat x y).
Proof.
∃ (m^-1)%core;
apply path_forall; intro;
destruct H';
simpl in *;
eauto.
Qed.
Definition isequiv_isepimorphism_ismonomorphism
(Hepi : IsEpimorphism (m : morphism set_cat x y))
(Hmono : IsMonomorphism (m : morphism set_cat x y))
: @IsEquiv _ _ m
:= @isequiv_isepi_ismono _ x y m Hepi Hmono.
End fully_faithful_helpers.
Global Instance isfullyfaithful_isfull_isfaithful
`{Univalence}
`{Hfull : @IsFull _ C D F}
`{Hfaithful : @IsFaithful _ C D F}
: @IsFullyFaithful _ C D F
:= fun x y ⇒ @isisomorphism_isequiv_set_cat
_ _ _ _
(@isequiv_isepimorphism_ismonomorphism
_ _ _ _
(Hfull x y)
(Hfaithful x y)).
(H' : ∀ x y (m : morphism set_cat x y),
IsEpimorphism m
→ IsMonomorphism m
→ IsIsomorphism m)
: IsFullyFaithful.
Proof.
intros ? ?; hnf in × |- .
apply H'; eauto.
Qed.
End full_faithful.
Section fully_faithful_helpers.
Context `{ua : Univalence}.
Variables x y : hSet.
Variable m : x → y.
Lemma isisomorphism_isequiv_set_cat
`{H' : IsEquiv _ _ m}
: IsIsomorphism (m : morphism set_cat x y).
Proof.
∃ (m^-1)%core;
apply path_forall; intro;
destruct H';
simpl in *;
eauto.
Qed.
Definition isequiv_isepimorphism_ismonomorphism
(Hepi : IsEpimorphism (m : morphism set_cat x y))
(Hmono : IsMonomorphism (m : morphism set_cat x y))
: @IsEquiv _ _ m
:= @isequiv_isepi_ismono _ x y m Hepi Hmono.
End fully_faithful_helpers.
Global Instance isfullyfaithful_isfull_isfaithful
`{Univalence}
`{Hfull : @IsFull _ C D F}
`{Hfaithful : @IsFaithful _ C D F}
: @IsFullyFaithful _ C D F
:= fun x y ⇒ @isisomorphism_isequiv_set_cat
_ _ _ _
(@isequiv_isepimorphism_ismonomorphism
_ _ _ _
(Hfull x y)
(Hfaithful x y)).
Split Essentially Surjective
Quoting the HoTT Book:Class IsSplitEssentiallySurjective A B (F : Functor A B)
:= is_split_essentially_surjective
: ∀ b : B, ∃ a : A, F a <~=~> b.
Essentially Surjective
Quoting the HoTT Book:
Class IsEssentiallySurjective A B (F : Functor A B)
:= is_essentially_surjective
: ∀ b : B, hexists (fun a : A ⇒ F a <~=~> b).
:= is_essentially_surjective
: ∀ b : B, hexists (fun a : A ⇒ F a <~=~> b).
Weak Equivalence
Quoting the HoTT Book:
Class IsWeakEquivalence `{Funext} A B (F : Functor A B)
:= { is_fully_faithful__is_weak_equivalence :> IsFullyFaithful F;
is_essentially_surjective__is_weak_equivalence :> IsEssentiallySurjective F }.
:= { is_fully_faithful__is_weak_equivalence :> IsFullyFaithful F;
is_essentially_surjective__is_weak_equivalence :> IsEssentiallySurjective F }.