michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(category): prove that the yoneda embedding is an embedding

Browse source
This commit is contained in:
Floris van Doorn 2015-09-03 00:46:11 -04:00 committed by Leonardo de Moura
parent fd89aa77a3
commit 1a3b363467
10 changed files with 135 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
hott/algebra/category/adjoint.hlean
View file

@ -62,6 +62,42 @@ namespace category
: is_equiv (@(to_fun_hom F) c c') :=
!H
definition hom_equiv_F_hom_F [constructor] (F : C ⇒ D)
[H : fully_faithful F] (c c' : C) : (c ⟶ c') ≃ (F c ⟶ F c') :=
equiv.mk _ !H
definition iso_of_F_iso_F (F : C ⇒ D)
[H : fully_faithful F] (c c' : C) (g : F c ≅ F c') : c ≅ c' :=
begin
induction g with g G, induction G with h p q, fapply iso.MK,
{ rexact (@(to_fun_hom F) c c')⁻¹ᶠ g},
{ rexact (@(to_fun_hom F) c' c)⁻¹ᶠ h},
{ exact abstract begin
apply eq_of_fn_eq_fn' (@(to_fun_hom F) c c),
rewrite [respect_comp, respect_id,
right_inv (@(to_fun_hom F) c c'), right_inv (@(to_fun_hom F) c' c), p],
end end},
{ exact abstract begin
apply eq_of_fn_eq_fn' (@(to_fun_hom F) c' c'),
rewrite [respect_comp, respect_id,
right_inv (@(to_fun_hom F) c c'), right_inv (@(to_fun_hom F) c' c), q],
end end}
end
definition iso_equiv_F_iso_F [constructor] (F : C ⇒ D)
[H : fully_faithful F] (c c' : C) : (c ≅ c') ≃ (F c ≅ F c') :=
begin
fapply equiv.MK,
{ exact preserve_iso F},
{ apply iso_of_F_iso_F},
{ exact abstract begin
intro f, induction f with f F', induction F' with g p q, apply iso_eq,
esimp [iso_of_F_iso_F], apply right_inv end end},
{ exact abstract begin
intro f, induction f with f F', induction F' with g p q, apply iso_eq,
esimp [iso_of_F_iso_F], apply right_inv end end},
end
definition is_iso_unit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (unit F) :=
!is_equivalence.is_iso_unit
@ -83,18 +119,18 @@ namespace category
to_fun_hom G' (natural_map ε d) ∘
natural_map η' (to_fun_ob G d) = id,
{ intro d, esimp,
rewrite [assoc],
rewrite [category.assoc],
rewrite [-assoc (G (ε' d))],
esimp, rewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
esimp, rewrite [assoc],
esimp, rewrite [-assoc],
esimp, rewrite [category.assoc],
esimp, rewrite [-category.assoc],
rewrite [↑functor.compose, -respect_comp G],
rewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
rewrite [respect_comp G],
rewrite [assoc,-assoc (G (ε d))],
rewrite [category.assoc,▸*,-category.assoc (G (ε d))],
rewrite [↑functor.compose, -respect_comp G],
rewrite [H' (G d)],
rewrite [respect_id,id_right],
rewrite [respect_id,▸*,category.id_right],
apply K},
assert lem₃ : Π (d : carrier D),
(to_fun_hom G' (natural_map ε d) ∘
@ -102,17 +138,17 @@ namespace category
to_fun_hom G (natural_map ε' d) ∘
natural_map η (to_fun_ob G' d) = id,
{ intro d, esimp,
rewrite [assoc, -assoc (G' (ε d))],
rewrite [category.assoc, -assoc (G' (ε d))],
esimp, rewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
esimp, rewrite [assoc], esimp, rewrite [-assoc],
esimp, rewrite [category.assoc], esimp, rewrite [-category.assoc],
rewrite [↑functor.compose, -respect_comp G'],
rewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d)],
esimp,
rewrite [respect_comp G'],
rewrite [assoc,-assoc (G' (ε' d))],
rewrite [category.assoc,▸*,-category.assoc (G' (ε' d))],
rewrite [↑functor.compose, -respect_comp G'],
rewrite [H (G' d)],
rewrite [respect_id,id_right],
rewrite [respect_id,▸*,category.id_right],
apply K'},
fapply lem₁,
{ fapply functor.eq_of_pointwise_iso,
@ -129,12 +165,13 @@ namespace category
rewrite functor.hom_of_eq_eq_of_pointwise_iso,
apply nat_trans_eq, intro c, esimp,
refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
esimp, rewrite [-respect_comp G',H c,respect_id G',id_left]},
esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,category.id_left]},
{ clear lem₁, refine transport_hom_of_eq_left _ ε ⬝ _,
krewrite inv_of_eq_compose_left,
rewrite functor.inv_of_eq_eq_of_pointwise_iso,
apply nat_trans_eq, intro d, esimp,
rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}
krewrite [respect_comp],
rewrite [assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}
end
definition full_of_fully_faithful (H : fully_faithful F) : full F :=

8
hott/algebra/category/category.hlean
View file

@ -6,7 +6,7 @@ Author: Jakob von Raumer
import .iso
open iso is_equiv eq is_trunc
open iso is_equiv equiv eq is_trunc
-- A category is a precategory extended by a witness
-- that the function from paths to isomorphisms,
@ -34,6 +34,9 @@ namespace category
-- TODO: Unsafe class instance?
attribute iso_of_path_equiv [instance]
definition eq_equiv_iso [constructor] (a b : ob) : (a = b) ≃ (a ≅ b) :=
equiv.mk iso_of_eq _
definition eq_of_iso [reducible] {a b : ob} : a ≅ b → a = b :=
iso_of_eq⁻¹ᶠ
@ -46,6 +49,9 @@ namespace category
definition inv_of_eq_eq_of_iso {a b : ob} (p : a ≅ b) : inv_of_eq (eq_of_iso p) = to_inv p :=
ap to_inv !iso_of_eq_eq_of_iso
theorem eq_of_iso_refl {a : ob} : eq_of_iso (iso.refl a) = idp :=
inv_eq_of_eq idp
definition is_trunc_1_ob : is_trunc 1 ob :=
begin
apply is_trunc_succ_intro, intro a b,

6
hott/algebra/category/constructions/functor.hlean
View file

@ -216,16 +216,16 @@ namespace category
end functor
definition category_functor [instance] (D : Category) (C : Precategory)
definition category_functor [instance] [constructor] (D : Category) (C : Precategory)
: category (D ^c C) :=
category.mk (D ^c C) (functor.is_univalent D C)
definition Category_functor (D : Category) (C : Precategory) : Category :=
definition Category_functor [constructor] (D : Category) (C : Precategory) : Category :=
category.Mk (D ^c C) !category_functor
--this definition is only useful if the exponent is a category,
-- and the elaborator has trouble with inserting the coercion
definition Category_functor' (D C : Category) : Category :=
definition Category_functor' [constructor] (D C : Category) : Category :=
Category_functor D C
namespace ops

8
hott/algebra/category/constructions/hset.hlean
View file

@ -25,26 +25,28 @@ namespace category
namespace set
local attribute is_equiv_subtype_eq [instance]
definition iso_of_equiv {A B : Precategory_hset} (f : A ≃ B) : A ≅ B :=
definition iso_of_equiv [constructor] {A B : Precategory_hset} (f : A ≃ B) : A ≅ B :=
iso.MK (to_fun f)
(to_inv f)
(eq_of_homotopy (left_inv (to_fun f)))
(eq_of_homotopy (right_inv (to_fun f)))
definition equiv_of_iso {A B : Precategory_hset} (f : A ≅ B) : A ≃ B :=
definition equiv_of_iso [constructor] {A B : Precategory_hset} (f : A ≅ B) : A ≃ B :=
begin
apply equiv.MK (to_hom f) (iso.to_inv f),
exact ap10 (to_right_inverse f),
exact ap10 (to_left_inverse f)
end
definition is_equiv_iso_of_equiv (A B : Precategory_hset) : is_equiv (@iso_of_equiv A B) :=
definition is_equiv_iso_of_equiv [constructor] (A B : Precategory_hset)
: is_equiv (@iso_of_equiv A B) :=
adjointify _ (λf, equiv_of_iso f)
(λf, proof iso_eq idp qed)
(λf, equiv_eq idp)
local attribute is_equiv_iso_of_equiv [instance]
-- TODO: move
open sigma.ops
definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)] (u v : Σa, B a)
: u = v → u.1 = v.1 :=

20
hott/algebra/category/functor.hlean
View file

@ -78,8 +78,8 @@ namespace functor
: functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
functor_eq (λc, idp) (λa b f, !id_leftright ⬝ !pH)
protected definition preserve_iso (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] :
is_iso (F f) :=
definition preserve_is_iso [constructor] (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f]
: is_iso (F f) :=
begin
fapply @is_iso.mk, apply (F (f⁻¹)),
repeat (apply concat ; symmetry ; apply (respect_comp F) ;
@ -88,8 +88,7 @@ namespace functor
apply (respect_id F) ),
end
definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b)
[H : is_iso f] [H' : is_iso (F f)] :
definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] [H' : is_iso (F f)] :
F (f⁻¹) = (F f)⁻¹ :=
begin
fapply @left_inverse_eq_right_inverse, apply (F f),
@ -101,7 +100,10 @@ namespace functor
apply right_inverse
end
attribute functor.preserve_iso [instance]
attribute preserve_is_iso [instance] [priority 100]
definition preserve_iso [constructor] (F : C ⇒ D) {a b : C} (f : a ≅ b) : F a ≅ F b :=
iso.mk (F f)
definition respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ :=
respect_inv F f
@ -163,11 +165,11 @@ namespace functor
esimp
end
definition functor_eq2' {F₁ F₂ : C ⇒ D} {p₁ p₂ : to_fun_ob F₁ = to_fun_ob F₂} (q₁ q₂)
theorem functor_eq2' {F₁ F₂ : C ⇒ D} {p₁ p₂ : to_fun_ob F₁ = to_fun_ob F₂} (q₁ q₂)
(r : p₁ = p₂) : functor_eq' p₁ q₁ = functor_eq' p₂ q₂ :=
by cases r; apply (ap (functor_eq' p₂)); apply is_hprop.elim
definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ~ ap010 to_fun_ob q)
theorem functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ~ ap010 to_fun_ob q)
: p = q :=
begin
cases F₁ with ob₁ hom₁ id₁ comp₁,
@ -178,12 +180,12 @@ namespace functor
exact r,
end
definition ap010_apd01111_functor {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
theorem ap010_apd01111_functor {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
{H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} {id₁ id₂ comp₁ comp₂}
(pF : F₁ = F₂) (pH : pF ▸ H₁ = H₂) (pid : cast (apd011 _ pF pH) id₁ = id₂)
(pcomp : cast (apd0111 _ pF pH pid) comp₁ = comp₂) (c : C)
: ap010 to_fun_ob (apd01111 functor.mk pF pH pid pcomp) c = ap10 pF c :=
by cases pF; cases pH; cases pid; cases pcomp; apply idp
by induction pF; induction pH; induction pid; induction pcomp; reflexivity
definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ~ to_fun_ob F₂)
(q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ~3 to_fun_hom F₂) (c : C) :

6
hott/algebra/category/iso.hlean
View file

@ -131,14 +131,14 @@ structure iso {ob : Type} [C : precategory ob] (a b : ob) :=
(to_hom : hom a b)
[struct : is_iso to_hom]
infix `≅`:50 := iso
attribute iso.struct [instance] [priority 4000]
namespace iso
variables {ob : Type} [C : precategory ob]
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
include C
infix `≅`:50 := iso
attribute struct [instance] [priority 400]
attribute to_hom [coercion]
protected definition MK [constructor] (f : a ⟶ b) (g : b ⟶ a)

4
hott/algebra/category/nat_trans.hlean
View file

@ -32,10 +32,10 @@ namespace nat_trans
infixr `∘n`:60 := nat_trans.compose
protected definition id [reducible] {F : C ⇒ D} : nat_trans F F :=
protected definition id [reducible] [constructor] {F : C ⇒ D} : nat_trans F F :=
mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹)
protected definition ID [reducible] (F : C ⇒ D) : nat_trans F F :=
protected definition ID [reducible] [constructor] (F : C ⇒ D) : nat_trans F F :=
(@nat_trans.id C D F)
notation 1 := nat_trans.id

65
hott/algebra/category/yoneda.hlean
View file

@ -6,6 +6,7 @@ Authors: Floris van Doorn
--note: modify definition in category.set
import .constructions.functor .constructions.hset .constructions.product .constructions.opposite
.adjoint
open category eq category.ops functor prod.ops is_trunc iso
@ -198,7 +199,7 @@ open functor
namespace yoneda
open category.set nat_trans lift
--should this be defined as "yoneda_embedding Cᵒᵖ"?
-- should this be defined as "yoneda_embedding Cᵒᵖ"?
definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
functor_curry !hom_functor
@ -207,12 +208,6 @@ namespace yoneda
notation `ɏ` := yoneda_embedding _
-- set_option pp.implicit true
-- set_option pp.notation false
-- -- -- set_option pp.full_names true
-- set_option pp.coercions true -- [constructor]
set_option formatter.hide_full_terms false
definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set)
(x : trunctype.carrier (F c)) : ɏ c ⟹ F :=
begin
@ -223,7 +218,6 @@ namespace yoneda
exact ap10 !(@respect_comp Cᵒᵖ set)⁻¹ x}
end
-- set_option pp.implicit true
definition yoneda_lemma {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ set) :
homset (ɏ c) F ≅ lift_functor (F c) :=
begin
@ -231,13 +225,60 @@ namespace yoneda
fapply equiv.MK,
{ intro η, exact up (η c id)},
{ intro x, induction x with x, exact yoneda_lemma_hom c F x},
{ intro x, induction x with x, esimp, apply ap up,
exact ap10 !respect_id x},
{ intro η, esimp, apply nat_trans_eq,
{ exact abstract begin intro x, induction x with x, esimp, apply ap up,
exact ap10 !respect_id x end end},
{ exact abstract begin intro η, esimp, apply nat_trans_eq,
intro c', esimp, apply eq_of_homotopy,
intro f, esimp [yoneda_embedding] at f,
transitivity (F f ∘ η c) id, reflexivity,
rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left},
rewrite naturality, esimp [yoneda_embedding], rewrite [id_left], apply ap _ !id_left end end},
end
theorem yoneda_lemma_natural_ob {C : Precategory} (F : Cᵒᵖ ⇒ set) {c c' : C} (f : c' ⟶ c)
(η : ɏ c ⟹ F) :
to_fun_hom (lift_functor ∘f F) f (to_hom (yoneda_lemma c F) η) =
proof to_hom (yoneda_lemma c' F) (η ∘n to_fun_hom ɏ f) qed :=
begin
esimp [yoneda_lemma,yoneda_embedding], apply ap up,
transitivity (F f ∘ η c) id, reflexivity,
rewrite naturality,
esimp [yoneda_embedding],
apply ap (η c'),
esimp [yoneda_embedding, Opposite],
rewrite [+id_left,+id_right],
end
theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ set)
(θ : F ⟹ F') (η : to_fun_ob ɏ c ⟹ F) :
proof (lift_functor.{v u} ∘fn θ) c (to_hom (yoneda_lemma c F) η) qed =
(to_hom (yoneda_lemma c F') proof (θ ∘n η : (to_fun_ob ɏ c : Cᵒᵖ ⇒ set) ⟹ F') qed) :=
by reflexivity
definition fully_faithful_yoneda_embedding [instance] (C : Precategory) :
fully_faithful (ɏ : C ⇒ set ^c Cᵒᵖ) :=
begin
intro c c',
fapply is_equiv_of_equiv_of_homotopy,
{ symmetry, transitivity _, apply @equiv_of_iso (homset _ _),
rexact yoneda_lemma c (ɏ c'), esimp [yoneda_embedding], exact !equiv_lift⁻¹ᵉ},
{ intro f, apply nat_trans_eq, intro c, apply eq_of_homotopy, intro f',
esimp [equiv.symm,equiv.trans],
esimp [yoneda_lemma,yoneda_embedding,Opposite],
rewrite [id_left,id_right]}
end
definition injective_on_objects_yoneda_embedding (C : Category) :
is_embedding (ɏ : C → Cᵒᵖ ⇒ set) :=
begin
apply is_embedding.mk, intro c c', fapply is_equiv_of_equiv_of_homotopy,
{ exact !eq_equiv_iso ⬝e !iso_equiv_F_iso_F ⬝e !eq_equiv_iso⁻¹ᵉ},
{ intro p, induction p, esimp [equiv.trans, equiv.symm],
esimp [preserve_iso],
rewrite -eq_of_iso_refl,
apply ap eq_of_iso, apply iso_eq, esimp,
apply nat_trans_eq, intro c',
apply eq_of_homotopy, esimp [yoneda_embedding], intro f,
rewrite [category.category.id_left], apply id_right}
end
end yoneda

4
hott/init/equiv.hlean
View file

@ -309,7 +309,7 @@ namespace equiv
definition eq_equiv_fn_eq_of_equiv [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
equiv.mk (ap f) !is_equiv_ap
definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) :=
definition equiv_ap [constructor] (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) :=
equiv.mk (transport P p) !is_equiv_tr
definition eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : x = y :=
@ -325,7 +325,7 @@ namespace equiv
definition equiv_of_equiv_of_eq [trans] {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q
definition equiv_of_eq_of_equiv [trans] {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▸ p
definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _
definition equiv_lift [constructor] (A : Type) : A ≃ lift A := equiv.mk up _
definition equiv_rect (f : A ≃ B) (P : B → Type) (g : Πa, P (f a)) (b : B) : P b :=
right_inv f b ▸ g (f⁻¹ b)

2
hott/init/pathover.hlean
View file

@ -172,7 +172,7 @@ namespace eq
{b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) : b =[p] b₂ :=
by cases p; apply (idp_rec_on q); apply idpo
definition pathover_compose (B' : A' → Type) (f : A → A') (p : a = a₂)
definition pathover_compose [constructor] (B' : A' → Type) (f : A → A') (p : a = a₂)
(b : B' (f a)) (b₂ : B' (f a₂)) : b =[p] b₂ ≃ b =[ap f p] b₂ :=
begin
fapply equiv.MK,