Theory Limit
chapter Limit
theory Limit
imports FreeCategory DiscreteCategory Adjunction
begin
text‹
This theory defines the notion of limit in terms of diagrams and cones and relates
it to the concept of a representation of a functor. The diagonal functor associated
with a diagram shape @{term J} is defined and it is shown that a right adjoint to
the diagonal functor gives limits of shape @{term J} and that a category has limits
of shape @{term J} if and only if the diagonal functor is a left adjoint functor.
Products and equalizers are defined as special cases of limits, and it is shown
that a category with equalizers has limits of shape @{term J} if it has products
indexed by the sets of objects and arrows of @{term J}.
The existence of limits in a set category is investigated, and it is shown that
every set category has equalizers and that a set category @{term S} has @{term I}-indexed
products if and only if the universe of @{term S} ``admits @{term I}-indexed tupling.''
The existence of limits in functor categories is also developed, showing that
limits in functor categories are ``determined pointwise'' and that a functor category
@{term "[A, B]"} has limits of shape @{term J} if @{term B} does.
Finally, it is shown that the Yoneda functor preserves limits.
This theory concerns itself only with limits; I have made no attempt to consider colimits.
Although it would be possible to rework the entire development in dual form,
it is possible that there is a more efficient way to dualize at least parts of it without
repeating all the work. This is something that deserves further thought.
›
section "Representations of Functors"
text‹
A representation of a contravariant functor ‹F: Cop → S›, where @{term S}
is a set category that is the target of a hom-functor for @{term C}, consists of
an object @{term a} of @{term C} and a natural isomorphism @{term "Φ: Y a → F"},
where ‹Y: C → [Cop, S]› is the Yoneda functor.
›
locale representation_of_functor =
C: category C +
Cop: dual_category C +
S: set_category S setp +
F: "functor" Cop.comp S F +
Hom: hom_functor C S setp φ +
Ya: yoneda_functor_fixed_object C S setp φ a +
natural_isomorphism Cop.comp S ‹Ya.Y a› F Φ
for C :: "'c comp" (infixr "⋅" 55)
and S :: "'s comp" (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
and F :: "'c ⇒ 's"
and a :: 'c
and Φ :: "'c ⇒ 's"
begin
abbreviation Y where "Y ≡ Ya.Y"
abbreviation ψ where "ψ ≡ Hom.ψ"
end
text‹
Two representations of the same functor are uniquely isomorphic.
›
locale two_representations_one_functor =
C: category C +
Cop: dual_category C +
S: set_category S setp +
F: set_valued_functor Cop.comp S setp F +
yoneda_functor C S setp φ +
Ya: yoneda_functor_fixed_object C S setp φ a +
Ya': yoneda_functor_fixed_object C S setp φ a' +
Φ: representation_of_functor C S setp φ F a Φ +
Φ': representation_of_functor C S setp φ F a' Φ'
for C :: "'c comp" (infixr "⋅" 55)
and S :: "'s comp" (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and F :: "'c ⇒ 's"
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
and a :: 'c
and Φ :: "'c ⇒ 's"
and a' :: 'c
and Φ' :: "'c ⇒ 's"
begin
interpretation Ψ: inverse_transformation Cop.comp S ‹Y a› F Φ ..
interpretation Ψ': inverse_transformation Cop.comp S ‹Y a'› F Φ' ..
interpretation ΦΨ': vertical_composite Cop.comp S ‹Y a› F ‹Y a'› Φ Ψ'.map ..
interpretation Φ'Ψ: vertical_composite Cop.comp S ‹Y a'› F ‹Y a› Φ' Ψ.map ..
lemma are_uniquely_isomorphic:
shows "∃!φ. «φ : a → a'» ∧ C.iso φ ∧ map φ = Cop_S.MkArr (Y a) (Y a') ΦΨ'.map"
proof -
interpret ΦΨ': natural_isomorphism Cop.comp S ‹Y a› ‹Y a'› ΦΨ'.map
using Φ.natural_isomorphism_axioms Ψ'.natural_isomorphism_axioms
natural_isomorphisms_compose
by blast
interpret Φ'Ψ: natural_isomorphism Cop.comp S ‹Y a'› ‹Y a› Φ'Ψ.map
using Φ'.natural_isomorphism_axioms Ψ.natural_isomorphism_axioms
natural_isomorphisms_compose
by blast
interpret ΦΨ'_Φ'Ψ: inverse_transformations Cop.comp S ‹Y a› ‹Y a'› ΦΨ'.map Φ'Ψ.map
proof
fix x
assume X: "Cop.ide x"
show "S.inverse_arrows (ΦΨ'.map x) (Φ'Ψ.map x)"
using S.inverse_arrows_compose S.inverse_arrows_sym X Φ'Ψ.map_simp_ide
ΦΨ'.map_simp_ide Ψ'.inverts_components Ψ.inverts_components
by force
qed
have "Cop_S.inverse_arrows (Cop_S.MkArr (Y a) (Y a') ΦΨ'.map)
(Cop_S.MkArr (Y a') (Y a) Φ'Ψ.map)"
proof -
have Ya: "functor Cop.comp S (Y a)" ..
have Ya': "functor Cop.comp S (Y a')" ..
have ΦΨ': "natural_transformation Cop.comp S (Y a) (Y a') ΦΨ'.map" ..
have Φ'Ψ: "natural_transformation Cop.comp S (Y a') (Y a) Φ'Ψ.map" ..
show ?thesis
by (metis (no_types, lifting) Cop_S.arr_MkArr Cop_S.comp_MkArr Cop_S.ide_MkIde
Cop_S.inverse_arrows_def Ya'.functor_axioms Ya.functor_axioms
Φ'Ψ.natural_transformation_axioms ΦΨ'.natural_transformation_axioms
ΦΨ'_Φ'Ψ.inverse_transformations_axioms inverse_transformations_inverse(1-2)
mem_Collect_eq)
qed
hence 3: "Cop_S.iso (Cop_S.MkArr (Y a) (Y a') ΦΨ'.map)" using Cop_S.isoI by blast
hence "∃f. «f : a → a'» ∧ map f = Cop_S.MkArr (Y a) (Y a') ΦΨ'.map"
using Ya.ide_a Ya'.ide_a is_full Y_def Cop_S.iso_is_arr full_functor.is_full
Cop_S.MkArr_in_hom ΦΨ'.natural_transformation_axioms preserves_ide
by force
from this obtain φ
where φ: "«φ : a → a'» ∧ map φ = Cop_S.MkArr (Y a) (Y a') ΦΨ'.map"
by blast
show ?thesis
by (metis 3 C.in_homE φ is_faithful reflects_iso)
qed
end
section "Diagrams and Cones"
text‹
A \emph{diagram} in a category @{term C} is a functor ‹D: J → C›.
We refer to the category @{term J} as the diagram \emph{shape}.
Note that in the usual expositions of category theory that use set theory
as their foundations, the shape @{term J} of a diagram is required to be
a ``small'' category, where smallness means that the collection of objects
of @{term J}, as well as each of the ``homs,'' is a set.
However, in HOL there is no class of all sets, so it is not meaningful
to speak of @{term J} as ``small'' in any kind of absolute sense.
There is likely a meaningful notion of smallness of @{term J}
\emph{relative to} @{term C} (the result below that states that a set
category has @{term I}-indexed products if and only if its universe
``admits @{term I}-indexed tuples'' is suggestive of how this might
be defined), but I haven't fully explored this idea at present.
›
locale diagram =
C: category C +
J: category J +
"functor" J C D
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
and D :: "'j ⇒ 'c"
begin
notation J.in_hom ("«_ : _ →⇩J _»")
end
lemma comp_diagram_functor:
assumes "diagram J C D" and "functor J' J F"
shows "diagram J' C (D o F)"
by (meson assms(1) assms(2) diagram_def functor.axioms(1) functor_comp)
text‹
A \emph{cone} over a diagram ‹D: J → C› is a natural transformation
from a constant functor to @{term D}. The value of the constant functor is
the \emph{apex} of the cone.
›
locale cone =
C: category C +
J: category J +
D: diagram J C D +
A: constant_functor J C a +
natural_transformation J C A.map D χ
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
and D :: "'j ⇒ 'c"
and a :: 'c
and χ :: "'j ⇒ 'c"
begin
lemma ide_apex:
shows "C.ide a"
using A.value_is_ide by auto
lemma component_in_hom:
assumes "J.arr j"
shows "«χ j : a → D (J.cod j)»"
using assms by auto
lemma cod_determines_component:
assumes "J.arr j"
shows "χ j = χ (J.cod j)"
using assms is_natural_2 A.map_simp C.comp_arr_ide ide_apex preserves_reflects_arr
by metis
end
text‹
A cone over diagram @{term D} is transformed into a cone over diagram @{term "D o F"}
by pre-composing with @{term F}.
›
lemma comp_cone_functor:
assumes "cone J C D a χ" and "functor J' J F"
shows "cone J' C (D o F) a (χ o F)"
proof -
interpret χ: cone J C D a χ using assms(1) by auto
interpret F: "functor" J' J F using assms(2) by auto
interpret A': constant_functor J' C a
using χ.A.value_is_ide by unfold_locales auto
have 1: "χ.A.map o F = A'.map"
using χ.A.map_def A'.map_def χ.J.not_arr_null by auto
interpret χ': natural_transformation J' C A'.map ‹D o F› ‹χ o F›
using 1 horizontal_composite F.as_nat_trans.natural_transformation_axioms
χ.natural_transformation_axioms
by fastforce
show "cone J' C (D o F) a (χ o F)" ..
qed
text‹
A cone over diagram @{term D} can be transformed into a cone over a diagram @{term D'}
by post-composing with a natural transformation from @{term D} to @{term D'}.
›
lemma vcomp_transformation_cone:
assumes "cone J C D a χ"
and "natural_transformation J C D D' τ"
shows "cone J C D' a (vertical_composite.map J C χ τ)"
by (meson assms cone.axioms(4-5) cone.intro diagram.intro natural_transformation.axioms(1-4)
vertical_composite.intro vertical_composite.is_natural_transformation)
context "functor"
begin
lemma preserves_diagrams:
fixes J :: "'j comp"
assumes "diagram J A D"
shows "diagram J B (F o D)"
by (meson assms diagram_def functor_axioms functor_comp functor_def)
lemma preserves_cones:
fixes J :: "'j comp"
assumes "cone J A D a χ"
shows "cone J B (F o D) (F a) (F o χ)"
proof -
interpret χ: cone J A D a χ using assms by auto
interpret Fa: constant_functor J B ‹F a›
using χ.ide_apex by unfold_locales auto
have 1: "F o χ.A.map = Fa.map"
proof
fix f
show "(F ∘ χ.A.map) f = Fa.map f"
using is_extensional Fa.is_extensional χ.A.is_extensional
by (cases "χ.J.arr f", simp_all)
qed
interpret χ': natural_transformation J B Fa.map ‹F o D› ‹F o χ›
using 1 horizontal_composite χ.natural_transformation_axioms
as_nat_trans.natural_transformation_axioms
by fastforce
show "cone J B (F o D) (F a) (F o χ)" ..
qed
end
context diagram
begin
abbreviation cone
where "cone a χ ≡ Limit.cone J C D a χ"
abbreviation cones :: "'c ⇒ ('j ⇒ 'c) set"
where "cones a ≡ { χ. cone a χ }"
text‹
An arrow @{term "f ∈ C.hom a' a"} induces by composition a transformation from
cones with apex @{term a} to cones with apex @{term a'}. This transformation
is functorial in @{term f}.
›
abbreviation cones_map :: "'c ⇒ ('j ⇒ 'c) ⇒ ('j ⇒ 'c)"
where "cones_map f ≡ (λχ ∈ cones (C.cod f). λj. if J.arr j then χ j ⋅ f else C.null)"
lemma cones_map_mapsto:
assumes "C.arr f"
shows "cones_map f ∈
extensional (cones (C.cod f)) ∩ (cones (C.cod f) → cones (C.dom f))"
proof
show "cones_map f ∈ extensional (cones (C.cod f))" by blast
show "cones_map f ∈ cones (C.cod f) → cones (C.dom f)"
proof
fix χ
assume "χ ∈ cones (C.cod f)"
hence χ: "cone (C.cod f) χ" by auto
interpret χ: cone J C D ‹C.cod f› χ using χ by auto
interpret B: constant_functor J C ‹C.dom f›
using assms by unfold_locales auto
have "cone (C.dom f) (λj. if J.arr j then χ j ⋅ f else C.null)"
using assms B.value_is_ide χ.is_natural_1 χ.is_natural_2
apply (unfold_locales, auto)
using χ.is_natural_1
apply (metis C.comp_assoc)
using χ.is_natural_2 C.comp_arr_dom
by (metis J.arr_cod_iff_arr J.cod_cod C.comp_assoc)
thus "(λj. if J.arr j then χ j ⋅ f else C.null) ∈ cones (C.dom f)" by auto
qed
qed
lemma cones_map_ide:
assumes "χ ∈ cones a"
shows "cones_map a χ = χ"
proof -
interpret χ: cone J C D a χ using assms by auto
show ?thesis
proof
fix j
show "cones_map a χ j = χ j"
using assms χ.A.value_is_ide χ.preserves_hom C.comp_arr_dom χ.is_extensional
by (cases "J.arr j", auto)
qed
qed
lemma cones_map_comp:
assumes "C.seq f g"
shows "cones_map (f ⋅ g) = restrict (cones_map g o cones_map f) (cones (C.cod f))"
proof (intro restr_eqI)
show "cones (C.cod (f ⋅ g)) = cones (C.cod f)" using assms by simp
show "⋀χ. χ ∈ cones (C.cod (f ⋅ g)) ⟹
(λj. if J.arr j then χ j ⋅ f ⋅ g else C.null) = (cones_map g o cones_map f) χ"
proof -
fix χ
assume χ: "χ ∈ cones (C.cod (f ⋅ g))"
show "(λj. if J.arr j then χ j ⋅ f ⋅ g else C.null) = (cones_map g o cones_map f) χ"
proof -
have "((cones_map g) o (cones_map f)) χ = cones_map g (cones_map f χ)"
by force
also have "... = (λj. if J.arr j then
(λj. if J.arr j then χ j ⋅ f else C.null) j ⋅ g else C.null)"
proof
fix j
have "cone (C.dom f) (cones_map f χ)"
using assms χ cones_map_mapsto by (elim C.seqE, force)
thus "cones_map g (cones_map f χ) j =
(if J.arr j then C (if J.arr j then χ j ⋅ f else C.null) g else C.null)"
using χ assms by auto
qed
also have "... = (λj. if J.arr j then χ j ⋅ f ⋅ g else C.null)"
using C.comp_assoc by fastforce
finally show ?thesis by auto
qed
qed
qed
end
text‹
Changing the apex of a cone by pre-composing with an arrow @{term f} commutes
with changing the diagram of a cone by post-composing with a natural transformation.
›
lemma cones_map_vcomp:
assumes "diagram J C D" and "diagram J C D'"
and "natural_transformation J C D D' τ"
and "cone J C D a χ"
and f: "partial_composition.in_hom C f a' a"
shows "diagram.cones_map J C D' f (vertical_composite.map J C χ τ)
= vertical_composite.map J C (diagram.cones_map J C D f χ) τ"
proof -
interpret D: diagram J C D using assms(1) by auto
interpret D': diagram J C D' using assms(2) by auto
interpret τ: natural_transformation J C D D' τ using assms(3) by auto
interpret χ: cone J C D a χ using assms(4) by auto
interpret τoχ: vertical_composite J C χ.A.map D D' χ τ ..
interpret τoχ: cone J C D' a τoχ.map ..
interpret χf: cone J C D a' ‹D.cones_map f χ›
using f χ.cone_axioms D.cones_map_mapsto by blast
interpret τoχf: vertical_composite J C χf.A.map D D' ‹D.cones_map f χ› τ ..
interpret τoχ_f: cone J C D' a' ‹D'.cones_map f τoχ.map›
using f τoχ.cone_axioms D'.cones_map_mapsto [of f] by blast
write C (infixr "⋅" 55)
show "D'.cones_map f τoχ.map = τoχf.map"
proof (intro NaturalTransformation.eqI)
show "natural_transformation J C χf.A.map D' (D'.cones_map f τoχ.map)" ..
show "natural_transformation J C χf.A.map D' τoχf.map" ..
show "⋀j. D.J.ide j ⟹ D'.cones_map f τoχ.map j = τoχf.map j"
proof -
fix j
assume j: "D.J.ide j"
have "D'.cones_map f τoχ.map j = τoχ.map j ⋅ f"
using f τoχ.cone_axioms τoχ.map_simp_2 τoχ.is_extensional by auto
also have "... = (τ j ⋅ χ (D.J.dom j)) ⋅ f"
using j τoχ.map_simp_2 by simp
also have "... = τ j ⋅ χ (D.J.dom j) ⋅ f"
using D.C.comp_assoc by simp
also have "... = τoχf.map j"
using j f χ.cone_axioms τoχf.map_simp_2 by auto
finally show "D'.cones_map f τoχ.map j = τoχf.map j" by auto
qed
qed
qed
text‹
Given a diagram @{term D}, we can construct a contravariant set-valued functor,
which takes each object @{term a} of @{term C} to the set of cones over @{term D}
with apex @{term a}, and takes each arrow @{term f} of @{term C} to the function
on cones over @{term D} induced by pre-composition with @{term f}.
For this, we need to introduce a set category @{term S} whose universe is large
enough to contain all the cones over @{term D}, and we need to have an explicit
correspondence between cones and elements of the universe of @{term S}.
A replete set category @{term S} equipped with an injective mapping
@{term_type "ι :: ('j => 'c) => 's"} serves this purpose.
›
locale cones_functor =
C: category C +
Cop: dual_category C +
J: category J +
D: diagram J C D +
S: replete_concrete_set_category S UNIV ι
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
and D :: "'j ⇒ 'c"
and S :: "'s comp" (infixr "⋅⇩S" 55)
and ι :: "('j ⇒ 'c) ⇒ 's"
begin
notation S.in_hom ("«_ : _ →⇩S _»")
abbreviation 𝗈 where "𝗈 ≡ S.DN"
definition map :: "'c ⇒ 's"
where "map = (λf. if C.arr f then
S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom f))
(ι o D.cones_map f o 𝗈)
else S.null)"
lemma map_simp [simp]:
assumes "C.arr f"
shows "map f = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom f))
(ι o D.cones_map f o 𝗈)"
using assms map_def by auto
lemma arr_map:
assumes "C.arr f"
shows "S.arr (map f)"
proof -
have "ι o D.cones_map f o 𝗈 ∈ ι ` D.cones (C.cod f) → ι ` D.cones (C.dom f)"
using assms D.cones_map_mapsto by force
thus ?thesis using assms S.UP_mapsto by auto
qed
lemma map_ide:
assumes "C.ide a"
shows "map a = S.mkIde (ι ` D.cones a)"
proof -
have "map a = S.mkArr (ι ` D.cones a) (ι ` D.cones a) (ι o D.cones_map a o 𝗈)"
using assms map_simp by force
also have "... = S.mkArr (ι ` D.cones a) (ι ` D.cones a) (λx. x)"
using S.UP_mapsto D.cones_map_ide by force
also have "... = S.mkIde (ι ` D.cones a)"
using assms S.mkIde_as_mkArr S.UP_mapsto by blast
finally show ?thesis by auto
qed
lemma map_preserves_dom:
assumes "Cop.arr f"
shows "map (Cop.dom f) = S.dom (map f)"
using assms arr_map map_ide by auto
lemma map_preserves_cod:
assumes "Cop.arr f"
shows "map (Cop.cod f) = S.cod (map f)"
using assms arr_map map_ide by auto
lemma map_preserves_comp:
assumes "Cop.seq g f"
shows "map (g ⋅⇧o⇧p f) = map g ⋅⇩S map f"
proof -
have "map (g ⋅⇧o⇧p f) = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom g))
((ι o D.cones_map g o 𝗈) o (ι o D.cones_map f o 𝗈))"
proof -
have 1: "S.arr (map (g ⋅⇧o⇧p f))"
using assms arr_map [of "C f g"] by simp
have "map (g ⋅⇧o⇧p f) = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom g))
(ι o D.cones_map (C f g) o 𝗈)"
using assms map_simp [of "C f g"] by simp
also have "... = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom g))
((ι o D.cones_map g o 𝗈) o (ι o D.cones_map f o 𝗈))"
using assms 1 calculation D.cones_map_mapsto D.cones_map_comp by auto
finally show ?thesis by blast
qed
also have "... = map g ⋅⇩S map f"
using assms arr_map [of f] arr_map [of g] map_simp S.comp_mkArr by auto
finally show ?thesis by auto
qed
lemma is_functor:
shows "functor Cop.comp S map"
apply (unfold_locales)
using map_def arr_map map_preserves_dom map_preserves_cod map_preserves_comp
by auto
end
sublocale cones_functor ⊆ "functor" Cop.comp S map using is_functor by auto
sublocale cones_functor ⊆ set_valued_functor Cop.comp S ‹λA. A ⊆ S.Univ› map ..
section Limits
subsection "Limit Cones"
text‹
A \emph{limit cone} for a diagram @{term D} is a cone @{term χ} over @{term D}
with the universal property that any other cone @{term χ'} over the diagram @{term D}
factors uniquely through @{term χ}.
›
locale limit_cone =
C: category C +
J: category J +
D: diagram J C D +
cone J C D a χ
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
and D :: "'j ⇒ 'c"
and a :: 'c
and χ :: "'j ⇒ 'c" +
assumes is_universal: "cone J C D a' χ' ⟹ ∃!f. «f : a' → a» ∧ D.cones_map f χ = χ'"
begin
definition induced_arrow :: "'c ⇒ ('j ⇒ 'c) ⇒ 'c"
where "induced_arrow a' χ' = (THE f. «f : a' → a» ∧ D.cones_map f χ = χ')"
lemma induced_arrowI:
assumes χ': "χ' ∈ D.cones a'"
shows "«induced_arrow a' χ' : a' → a»"
and "D.cones_map (induced_arrow a' χ') χ = χ'"
proof -
have "∃!f. «f : a' → a» ∧ D.cones_map f χ = χ'"
using assms χ' is_universal by simp
hence 1: "«induced_arrow a' χ' : a' → a» ∧ D.cones_map (induced_arrow a' χ') χ = χ'"
using theI' [of "λf. «f : a' → a» ∧ D.cones_map f χ = χ'"] induced_arrow_def
by presburger
show "«induced_arrow a' χ' : a' → a»" using 1 by simp
show "D.cones_map (induced_arrow a' χ') χ = χ'" using 1 by simp
qed
lemma cones_map_induced_arrow:
shows "induced_arrow a' ∈ D.cones a' → C.hom a' a"
and "⋀χ'. χ' ∈ D.cones a' ⟹ D.cones_map (induced_arrow a' χ') χ = χ'"
using induced_arrowI by auto
lemma induced_arrow_cones_map:
assumes "C.ide a'"
shows "(λf. D.cones_map f χ) ∈ C.hom a' a → D.cones a'"
and "⋀f. «f : a' → a» ⟹ induced_arrow a' (D.cones_map f χ) = f"
proof -
have a': "C.ide a'" using assms by (simp add: cone.ide_apex)
have cone_χ: "cone J C D a χ" ..
show "(λf. D.cones_map f χ) ∈ C.hom a' a → D.cones a'"
using cone_χ D.cones_map_mapsto by blast
fix f
assume f: "«f : a' → a»"
show "induced_arrow a' (D.cones_map f χ) = f"
proof -
have "D.cones_map f χ ∈ D.cones a'"
using f cone_χ D.cones_map_mapsto by blast
hence "∃!f'. «f' : a' → a» ∧ D.cones_map f' χ = D.cones_map f χ"
using assms is_universal by auto
thus ?thesis
using f induced_arrow_def
the1_equality [of "λf'. «f' : a' → a» ∧ D.cones_map f' χ = D.cones_map f χ"]
by presburger
qed
qed
text‹
For a limit cone @{term χ} with apex @{term a}, for each object @{term a'} the
hom-set @{term "C.hom a' a"} is in bijective correspondence with the set of cones
with apex @{term a'}.
›
lemma bij_betw_hom_and_cones:
assumes "C.ide a'"
shows "bij_betw (λf. D.cones_map f χ) (C.hom a' a) (D.cones a')"
proof (intro bij_betwI)
show "(λf. D.cones_map f χ) ∈ C.hom a' a → D.cones a'"
using assms induced_arrow_cones_map by blast
show "induced_arrow a' ∈ D.cones a' → C.hom a' a"
using assms cones_map_induced_arrow by blast
show "⋀f. f ∈ C.hom a' a ⟹ induced_arrow a' (D.cones_map f χ) = f"
using assms induced_arrow_cones_map by blast
show "⋀χ'. χ' ∈ D.cones a' ⟹ D.cones_map (induced_arrow a' χ') χ = χ'"
using assms cones_map_induced_arrow by blast
qed
lemma induced_arrow_eqI:
assumes "D.cone a' χ'" and "«f : a' → a»" and "D.cones_map f χ = χ'"
shows "induced_arrow a' χ' = f"
using assms is_universal induced_arrow_def
the1_equality [of "λf. f ∈ C.hom a' a ∧ D.cones_map f χ = χ'" f]
by simp
lemma induced_arrow_self:
shows "induced_arrow a χ = a"
proof -
have "«a : a → a» ∧ D.cones_map a χ = χ"
using ide_apex cone_axioms D.cones_map_ide by force
thus ?thesis using induced_arrow_eqI cone_axioms by auto
qed
end
context diagram
begin
abbreviation limit_cone
where "limit_cone a χ ≡ Limit.limit_cone J C D a χ"
text‹
A diagram @{term D} has object @{term a} as a limit if @{term a} is the apex
of some limit cone over @{term D}.
›
abbreviation has_as_limit :: "'c ⇒ bool"
where "has_as_limit a ≡ (∃χ. limit_cone a χ)"
abbreviation has_limit
where "has_limit ≡ (∃a χ. limit_cone a χ)"
definition some_limit :: 'c
where "some_limit = (SOME a. ∃χ. limit_cone a χ)"
definition some_limit_cone :: "'j ⇒ 'c"
where "some_limit_cone = (SOME χ. limit_cone some_limit χ)"
lemma limit_cone_some_limit_cone:
assumes has_limit
shows "limit_cone some_limit some_limit_cone"
proof -
have "∃a. has_as_limit a" using assms by simp
hence "has_as_limit some_limit"
using some_limit_def someI_ex [of "λa. ∃χ. limit_cone a χ"] by simp
thus "limit_cone some_limit some_limit_cone"
using assms some_limit_cone_def someI_ex [of "λχ. limit_cone some_limit χ"]
by simp
qed
lemma ex_limitE:
assumes "∃a. has_as_limit a"
obtains a χ where "limit_cone a χ"
using assms someI_ex by blast
end
subsection "Limits by Representation"
text‹
A limit for a diagram D can also be given by a representation ‹(a, Φ)›
of the cones functor.
›
locale representation_of_cones_functor =
C: category C +
Cop: dual_category C +
J: category J +
D: diagram J C D +
S: replete_concrete_set_category S UNIV ι +
Cones: cones_functor J C D S ι +
Hom: hom_functor C S ‹λA. A ⊆ S.Univ› φ +
representation_of_functor C S S.setp φ Cones.map a Φ
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
and D :: "'j ⇒ 'c"
and S :: "'s comp" (infixr "⋅⇩S" 55)
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
and ι :: "('j ⇒ 'c) ⇒ 's"
and a :: 'c
and Φ :: "'c ⇒ 's"
subsection "Putting it all Together"
text‹
A ``limit situation'' combines and connects the ways of presenting a limit.
›
locale limit_situation =
C: category C +
Cop: dual_category C +
J: category J +
D: diagram J C D +
S: replete_concrete_set_category S UNIV ι +
Cones: cones_functor J C D S ι +
Hom: hom_functor C S S.setp φ +
Φ: representation_of_functor C S S.setp φ Cones.map a Φ +
χ: limit_cone J C D a χ
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
and D :: "'j ⇒ 'c"
and S :: "'s comp" (infixr "⋅⇩S" 55)
and φ :: "'c * 'c ⇒ 'c ⇒ 's"
and ι :: "('j ⇒ 'c) ⇒ 's"
and a :: 'c
and Φ :: "'c ⇒ 's"
and χ :: "'j ⇒ 'c" +
assumes χ_in_terms_of_Φ: "χ = S.DN (S.Fun (Φ a) (φ (a, a) a))"
and Φ_in_terms_of_χ:
"Cop.ide a' ⟹ Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a')
(λx. ι (D.cones_map (Hom.ψ (a', a) x) χ))"
text (in limit_situation) ‹
The assumption @{prop χ_in_terms_of_Φ} states that the universal cone @{term χ} is obtained
by applying the function @{term "S.Fun (Φ a)"} to the identity @{term a} of
@{term[source=true] C} (after taking into account the necessary coercions).
›
text (in limit_situation) ‹
The assumption @{prop Φ_in_terms_of_χ} states that the component of @{term Φ} at @{term a'}
is the arrow of @{term[source=true] S} corresponding to the function that takes an arrow
@{term "f ∈ C.hom a' a"} and produces the cone with vertex @{term a'} obtained
by transforming the universal cone @{term χ} by @{term f}.
›
subsection "Limit Cones Induce Limit Situations"
text‹
To obtain a limit situation from a limit cone, we need to introduce a set category
that is large enough to contain the hom-sets of @{term C} as well as the cones
over @{term D}. We use the category of all @{typ "('c + ('j ⇒ 'c))"}-sets for this.
›
context limit_cone
begin
interpretation Cop: dual_category C ..
interpretation CopxC: product_category Cop.comp C ..
interpretation S: replete_setcat ‹TYPE('c + ('j ⇒ 'c))› .
notation S.comp (infixr "⋅⇩S" 55)
interpretation Sr: replete_concrete_set_category S.comp UNIV ‹S.UP o Inr›
apply unfold_locales
using S.UP_mapsto
apply auto[1]
using S.inj_UP inj_Inr inj_compose
by metis
interpretation Cones: cones_functor J C D S.comp ‹S.UP o Inr› ..
interpretation Hom: hom_functor C S.comp S.setp ‹λ_. S.UP o Inl›
apply (unfold_locales)
using S.UP_mapsto
apply auto[1]
using S.inj_UP injD inj_onI inj_Inl inj_compose
apply (metis (no_types, lifting))
using S.UP_mapsto
by auto
interpretation Y: yoneda_functor C S.comp S.setp ‹λ_. S.UP o Inl› ..
interpretation Ya: yoneda_functor_fixed_object C S.comp S.setp ‹λ_. S.UP o Inl› a
apply (unfold_locales) using ide_apex by auto
abbreviation inl :: "'c ⇒ 'c + ('j ⇒ 'c)" where "inl ≡ Inl"
abbreviation inr :: "('j ⇒ 'c) ⇒ 'c + ('j ⇒ 'c)" where "inr ≡ Inr"
abbreviation ι where "ι ≡ S.UP o inr"
abbreviation 𝗈 where "𝗈 ≡ Cones.𝗈"
abbreviation φ where "φ ≡ λ_. S.UP o inl"
abbreviation ψ where "ψ ≡ Hom.ψ"
abbreviation Y where "Y ≡ Y.Y"
lemma Ya_ide:
assumes a': "C.ide a'"
shows "Y a a' = S.mkIde (Hom.set (a', a))"
using assms ide_apex Y.Y_simp Hom.map_ide by simp
lemma Ya_arr:
assumes g: "C.arr g"
shows "Y a g = S.mkArr (Hom.set (C.cod g, a)) (Hom.set (C.dom g, a))
(φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a))"
using ide_apex g Y.Y_ide_arr [of a g "C.dom g" "C.cod g"] by auto
lemma is_cone [simp]:
shows "χ ∈ D.cones a"
using cone_axioms by simp
text‹
For each object @{term a'} of @{term[source=true] C} we have a function mapping
@{term "C.hom a' a"} to the set of cones over @{term D} with apex @{term a'},
which takes @{term "f ∈ C.hom a' a"} to ‹χf›, where ‹χf› is the cone obtained by
composing @{term χ} with @{term f} (after accounting for coercions to and from the
universe of @{term S}). The corresponding arrows of @{term S} are the
components of a natural isomorphism from @{term "Y a"} to ‹Cones›.
›
definition Φo :: "'c ⇒ ('c + ('j ⇒ 'c)) setcat.arr"
where
"Φo a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (λx. ι (D.cones_map (ψ (a', a) x) χ))"
lemma Φo_in_hom:
assumes a': "C.ide a'"
shows "«Φo a' : S.mkIde (Hom.set (a', a)) →⇩S S.mkIde (ι ` D.cones a')»"
proof -
have " «S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (λx. ι (D.cones_map (ψ (a', a) x) χ)) :
S.mkIde (Hom.set (a', a)) →⇩S S.mkIde (ι ` D.cones a')»"
proof -
have "(λx. ι (D.cones_map (ψ (a', a) x) χ)) ∈ Hom.set (a', a) → ι ` D.cones a'"
proof
fix x
assume x: "x ∈ Hom.set (a', a)"
hence "«ψ (a', a) x : a' → a»"
using ide_apex a' Hom.ψ_mapsto by auto
hence "D.cones_map (ψ (a', a) x) χ ∈ D.cones a'"
using ide_apex a' x D.cones_map_mapsto is_cone by force
thus "ι (D.cones_map (ψ (a', a) x) χ) ∈ ι ` D.cones a'" by simp
qed
moreover have "Hom.set (a', a) ⊆ S.Univ"
using ide_apex a' Hom.set_subset_Univ by auto
moreover have "ι ` D.cones a' ⊆ S.Univ"
using S.UP_mapsto by auto
ultimately show ?thesis using S.mkArr_in_hom by simp
qed
thus ?thesis using Φo_def [of a'] by auto
qed
interpretation Φ: transformation_by_components Cop.comp S.comp ‹Y a› Cones.map Φo
proof
fix a'
assume A': "Cop.ide a'"
show "«Φo a' : Y a a' →⇩S Cones.map a'»"
using A' Ya_ide Φo_in_hom Cones.map_ide by auto
next
fix g
assume g: "Cop.arr g"
show "Φo (Cop.cod g) ⋅⇩S Y a g = Cones.map g ⋅⇩S Φo (Cop.dom g)"
proof -
let ?A = "Hom.set (C.cod g, a)"
let ?B = "Hom.set (C.dom g, a)"
let ?B' = "ι ` D.cones (C.cod g)"
let ?C = "ι ` D.cones (C.dom g)"
let ?F = "φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a)"
let ?F' = "ι o D.cones_map g o 𝗈"
let ?G = "λx. ι (D.cones_map (ψ (C.dom g, a) x) χ)"
let ?G' = "λx. ι (D.cones_map (ψ (C.cod g, a) x) χ)"
have "S.arr (Y a g) ∧ Y a g = S.mkArr ?A ?B ?F"
using ide_apex g Ya.preserves_arr Ya_arr by fastforce
moreover have "S.arr (Φo (Cop.cod g))"
using g Φo_in_hom [of "Cop.cod g"] by auto
moreover have "Φo (Cop.cod g) = S.mkArr ?B ?C ?G"
using g Φo_def [of "C.dom g"] by auto
moreover have "S.seq (Φo (Cop.cod g)) (Y a g)"
using ide_apex g Φo_in_hom [of "Cop.cod g"] by auto
ultimately have 1: "S.seq (Φo (Cop.cod g)) (Y a g) ∧
Φo (Cop.cod g) ⋅⇩S Y a g = S.mkArr ?A ?C (?G o ?F)"
using S.comp_mkArr [of ?A ?B ?F ?C ?G] by argo
have "Cones.map g = S.mkArr (ι ` D.cones (C.cod g)) (ι ` D.cones (C.dom g)) ?F'"
using g Cones.map_simp by fastforce
moreover have "Φo (Cop.dom g) = S.mkArr ?A ?B' ?G'"
using g Φo_def by fastforce
moreover have "S.seq (Cones.map g) (Φo (Cop.dom g))"
using g Cones.preserves_hom [of g "C.cod g" "C.dom g"] Φo_in_hom [of "Cop.dom g"]
by force
ultimately have
2: "S.seq (Cones.map g) (Φo (Cop.dom g)) ∧
Cones.map g ⋅⇩S Φo (Cop.dom g) = S.mkArr ?A ?C (?F' o ?G')"
using S.seqI' [of "Φo (Cop.dom g)" "Cones.map g"] S.comp_mkArr by auto
have "Φo (Cop.cod g) ⋅⇩S Y a g = S.mkArr ?A ?C (?G o ?F)"
using 1 by auto
also have "... = S.mkArr ?A ?C (?F' o ?G')"
proof (intro S.mkArr_eqI')
show "S.arr (S.mkArr ?A ?C (?G o ?F))" using 1 by force
show "⋀x. x ∈ ?A ⟹ (?G o ?F) x = (?F' o ?G') x"
proof -
fix x
assume x: "x ∈ ?A"
hence 1: "«ψ (C.cod g, a) x : C.cod g → a»"
using ide_apex g Hom.ψ_mapsto [of "C.cod g" a] by auto
have "(?G o ?F) x = ι (D.cones_map (ψ (C.dom g, a)
(φ (C.dom g, a) (ψ (C.cod g, a) x ⋅ g))) χ)"
proof -
have "(?G o ?F) x = ?G (?F x)" by simp
also have "... = ι (D.cones_map (ψ (C.dom g, a)
(φ (C.dom g, a) (ψ (C.cod g, a) x ⋅ g))) χ)"
by (metis Cop.comp_def comp_apply)
finally show ?thesis by auto
qed
also have "... = ι (D.cones_map (ψ (C.cod g, a) x ⋅ g) χ)"
proof -
have "«ψ (C.cod g, a) x ⋅ g : C.dom g → a»" using g 1 by auto
thus ?thesis using Hom.ψ_φ by presburger
qed
also have "... = ι (D.cones_map g (D.cones_map (ψ (C.cod g, a) x) χ))"
using g x 1 is_cone D.cones_map_comp [of "ψ (C.cod g, a) x" g] by fastforce
also have "... = ι (D.cones_map g (𝗈 (ι (D.cones_map (ψ (C.cod g, a) x) χ))))"
using 1 is_cone D.cones_map_mapsto Sr.DN_UP by auto
also have "... = (?F' o ?G') x" by simp
finally show "(?G o ?F) x = (?F' o ?G') x" by auto
qed
qed
also have "... = Cones.map g ⋅⇩S Φo (Cop.dom g)"
using 2 by auto
finally show ?thesis by auto
qed
qed
interpretation Φ: set_valued_transformation Cop.comp S.comp S.setp
‹Y a› Cones.map Φ.map ..
interpretation Φ: natural_isomorphism Cop.comp S.comp ‹Y a› Cones.map Φ.map
proof
fix a'
assume a': "Cop.ide a'"
show "S.iso (Φ.map a')"
proof -
let ?F = "λx. ι (D.cones_map (ψ (a', a) x) χ)"
have bij: "bij_betw ?F (Hom.set (a', a)) (ι ` D.cones a')"
proof -
have "⋀x x'. ⟦ x ∈ Hom.set (a', a); x' ∈ Hom.set (a', a);
ι (D.cones_map (ψ (a', a) x) χ) = ι (D.cones_map (ψ (a', a) x') χ) ⟧
⟹ x = x'"
proof -
fix x x'
assume x: "x ∈ Hom.set (a', a)" and x': "x' ∈ Hom.set (a', a)"
and xx': "ι (D.cones_map (ψ (a', a) x) χ) = ι (D.cones_map (ψ (a', a) x') χ)"
have ψx: "«ψ (a', a) x : a' → a»" using x ide_apex a' Hom.ψ_mapsto by auto
have ψx': "«ψ (a', a) x' : a' → a»" using x' ide_apex a' Hom.ψ_mapsto by auto
have 1: "∃!f. «f : a' → a» ∧ ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)"
proof -
have "D.cones_map (ψ (a', a) x) χ ∈ D.cones a'"
using ψx a' is_cone D.cones_map_mapsto by force
hence 2: "∃!f. «f : a' → a» ∧ D.cones_map f χ = D.cones_map (ψ (a', a) x) χ"
using a' is_universal by simp
show "∃!f. «f : a' → a» ∧ ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)"
proof -
have "⋀f. ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)
⟷ D.cones_map f χ = D.cones_map (ψ (a', a) x) χ"
proof -
fix f :: 'c
have "D.cones_map f χ = D.cones_map (ψ (a', a) x) χ
⟶ ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)"
by simp
thus "(ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ))
= (D.cones_map f χ = D.cones_map (ψ (a', a) x) χ)"
by (meson Sr.inj_UP injD)
qed
thus ?thesis using 2 by auto
qed
qed
have 2: "∃!x''. x'' ∈ Hom.set (a', a) ∧
ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)"
proof -
from 1 obtain f'' where
f'': "«f'' : a' → a» ∧ ι (D.cones_map f'' χ) = ι (D.cones_map (ψ (a', a) x) χ)"
by blast
have "φ (a', a) f'' ∈ Hom.set (a', a) ∧
ι (D.cones_map (ψ (a', a) (φ (a', a) f'')) χ) = ι (D.cones_map (ψ (a', a) x) χ)"
proof
show "φ (a', a) f'' ∈ Hom.set (a', a)" using f'' Hom.set_def by auto
show "ι (D.cones_map (ψ (a', a) (φ (a', a) f'')) χ) =
ι (D.cones_map (ψ (a', a) x) χ)"
using f'' Hom.ψ_φ by presburger
qed
moreover have
"⋀x''. x'' ∈ Hom.set (a', a) ∧
ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)
⟹ x'' = φ (a', a) f''"
proof -
fix x''
assume x'': "x'' ∈ Hom.set (a', a) ∧
ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)"
hence "«ψ (a', a) x'' : a' → a» ∧
ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)"
using ide_apex a' Hom.set_def Hom.ψ_mapsto [of a' a] by auto
hence "φ (a', a) (ψ (a', a) x'') = φ (a', a) f''"
using 1 f'' by auto
thus "x'' = φ (a', a) f''"
using ide_apex a' x'' Hom.φ_ψ by simp
qed
ultimately show ?thesis
using ex1I [of "λx'. x' ∈ Hom.set (a', a) ∧
ι (D.cones_map (ψ (a', a) x') χ) =
ι (D.cones_map (ψ (a', a) x) χ)"
"φ (a', a) f''"]
by simp
qed
thus "x = x'" using x x' xx' by auto
qed
hence "inj_on ?F (Hom.set (a', a))"
using inj_onI [of "Hom.set (a', a)" ?F] by auto
moreover have "?F ` Hom.set (a', a) = ι ` D.cones a'"
proof
show "?F ` Hom.set (a', a) ⊆ ι ` D.cones a'"
proof
fix X'
assume X': "X' ∈ ?F ` Hom.set (a', a)"
from this obtain x' where x': "x' ∈ Hom.set (a', a) ∧ ?F x' = X'" by blast
show "X' ∈ ι ` D.cones a'"
proof -
have "X' = ι (D.cones_map (ψ (a', a) x') χ)" using x' by blast
hence "X' = ι (D.cones_map (ψ (a', a) x') χ)" using x' by force
moreover have "«ψ (a', a) x' : a' → a»"
using ide_apex a' x' Hom.set_def Hom.ψ_φ by auto
ultimately show ?thesis
using x' is_cone D.cones_map_mapsto by force
qed
qed
show "ι ` D.cones a' ⊆ ?F ` Hom.set (a', a)"
proof
fix X'
assume X': "X' ∈ ι ` D.cones a'"
hence "𝗈 X' ∈ 𝗈 ` ι ` D.cones a'" by simp
with Sr.DN_UP have "𝗈 X' ∈ D.cones a'"
by auto
hence "∃!f. «f : a' → a» ∧ D.cones_map f χ = 𝗈 X'"
using a' is_universal by simp
from this obtain f where "«f : a' → a» ∧ D.cones_map f χ = 𝗈 X'"
by auto
hence f: "«f : a' → a» ∧ ι (D.cones_map f χ) = X'"
using X' Sr.UP_DN by auto
have "X' = ?F (φ (a', a) f)"
using f Hom.ψ_φ by presburger
thus "X' ∈ ?F ` Hom.set (a', a)"
using f Hom.set_def by force
qed
qed
ultimately show ?thesis
using bij_betw_def [of ?F "Hom.set (a', a)" "ι ` D.cones a'"] inj_on_def by auto
qed
let ?f = "S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F"
have iso: "S.iso ?f"
proof -
have "?F ∈ Hom.set (a', a) → ι ` D.cones a'"
using bij bij_betw_imp_funcset by fast
hence 1: "S.arr ?f"
using ide_apex a' Hom.set_subset_Univ S.UP_mapsto by auto
thus ?thesis using bij S.iso_char S.set_mkIde by fastforce
qed
moreover have "?f = Φ.map a'"
using a' Φo_def by force
finally show ?thesis by auto
qed
qed
interpretation R: representation_of_functor C S.comp S.setp φ Cones.map a Φ.map ..
lemma χ_in_terms_of_Φ:
shows "χ = 𝗈 (Φ.FUN a (φ (a, a) a))"
proof -
have "Φ.FUN a (φ (a, a) a) =
(λx ∈ Hom.set (a, a). ι (D.cones_map (ψ (a, a) x) χ)) (φ (a, a) a)"
using ide_apex S.Fun_mkArr Φ.map_simp_ide Φo_def Φ.preserves_reflects_arr [of a]
by simp
also have "... = ι (D.cones_map a χ)"
proof -
have "(λx ∈ Hom.set (a, a). ι (D.cones_map (ψ (a, a) x) χ)) (φ (a, a) a)
= ι (D.cones_map (ψ (a, a) (φ (a, a) a)) χ)"
proof -
have "φ (a, a) a ∈ Hom.set (a, a)"
using ide_apex Hom.φ_mapsto by fastforce
thus ?thesis
using restrict_apply' [of "φ (a, a) a" "Hom.set (a, a)"] by blast
qed
also have "... = ι (D.cones_map a χ)"
proof -
have "ψ (a, a) (φ (a, a) a) = a"
using ide_apex Hom.ψ_φ [of a a a] by fastforce
thus ?thesis by metis
qed
finally show ?thesis by auto
qed
finally have "Φ.FUN a (φ (a, a) a) = ι (D.cones_map a χ)" by auto
also have "... = ι χ"
using ide_apex D.cones_map_ide [of χ a] is_cone by simp
finally have "Φ.FUN a (φ (a, a) a) = ι χ" by blast
hence "𝗈 (Φ.FUN a (φ (a, a) a)) = 𝗈 (ι χ)" by simp
thus ?thesis using is_cone Sr.DN_UP by simp
qed
abbreviation Hom
where "Hom ≡ Hom.map"
abbreviation Φ
where "Φ ≡ Φ.map"
lemma induces_limit_situation:
shows "limit_situation J C D S.comp φ ι a Φ χ"
using χ_in_terms_of_Φ Φo_def by unfold_locales auto
no_notation S.comp (infixr "⋅⇩S" 55)
end
sublocale limit_cone ⊆ limit_situation J C D replete_setcat.comp φ ι a Φ χ
using induces_limit_situation by auto
subsection "Representations of the Cones Functor Induce Limit Situations"
context representation_of_cones_functor
begin
interpretation Φ: set_valued_transformation Cop.comp S S.setp ‹Y a› Cones.map Φ ..
interpretation Ψ: inverse_transformation Cop.comp S ‹Y a› Cones.map Φ ..
interpretation Ψ: set_valued_transformation Cop.comp S S.setp
Cones.map ‹Y a› Ψ.map ..
abbreviation 𝗈
where "𝗈 ≡ Cones.𝗈"
abbreviation χ
where "χ ≡ 𝗈 (S.Fun (Φ a) (φ (a, a) a))"
lemma Cones_SET_eq_ι_img_cones:
assumes "C.ide a'"
shows "Cones.SET a' = ι ` D.cones a'"
proof -
have "ι ` D.cones a' ⊆ S.Univ" using S.UP_mapsto by auto
thus ?thesis using assms Cones.map_ide S.set_mkIde by auto
qed
lemma ιχ:
shows "ι χ = S.Fun (Φ a) (φ (a, a) a)"
proof -
have "S.Fun (Φ a) (φ (a, a) a) ∈ Cones.SET a"
using Ya.ide_a Hom.φ_mapsto S.Fun_mapsto [of "Φ a"] Hom.set_map by fastforce
thus ?thesis
using Ya.ide_a Cones_SET_eq_ι_img_cones by auto
qed
interpretation χ: cone J C D a χ
proof -
have "ι χ ∈ ι ` D.cones a"
using Ya.ide_a ιχ S.Fun_mapsto [of "Φ a"] Hom.φ_mapsto Hom.set_map
Cones_SET_eq_ι_img_cones by fastforce
thus "D.cone a χ"
by (metis (no_types, lifting) S.DN_UP UNIV_I f_inv_into_f inv_into_into mem_Collect_eq)
qed
lemma cone_χ:
shows "D.cone a χ" ..
lemma Φ_FUN_simp:
assumes a': "C.ide a'" and x: "x ∈ Hom.set (a', a)"
shows "Φ.FUN a' x = Cones.FUN (ψ (a', a) x) (ι χ)"
proof -
have ψx: "«ψ (a', a) x : a' → a»"
using Ya.ide_a a' x Hom.ψ_mapsto by blast
have φa: "φ (a, a) a ∈ Hom.set (a, a)" using Ya.ide_a Hom.φ_mapsto by fastforce
have "Φ.FUN a' x = (Φ.FUN a' o Ya.FUN (ψ (a', a) x)) (φ (a, a) a)"
proof -
have "φ (a', a) (a ⋅ ψ (a', a) x) = x"
using Ya.ide_a a' x ψx Hom.φ_ψ C.comp_cod_arr by fastforce
moreover have "S.arr (S.mkArr (Hom.set (a, a)) (Hom.set (a', a))
(φ (a', a) ∘ Cop.comp (ψ (a', a) x) ∘ ψ (a, a)))"
by (metis C.arrI Cop.arr_char Ya.Y_ide_arr(2) Ya.preserves_arr χ.ide_apex ψx)
ultimately show ?thesis
using Ya.ide_a a' x Ya.Y_ide_arr ψx φa C.ide_in_hom by auto
qed
also have "... = (Cones.FUN (ψ (a', a) x) o Φ.FUN a) (φ (a, a) a)"
proof -
have "(Φ.FUN a' o Ya.FUN (ψ (a', a) x)) (φ (a, a) a)
= S.Fun (Φ a' ⋅⇩S Y a (ψ (a', a) x)) (φ (a, a) a)"
using ψx a' φa Ya.ide_a Ya.map_simp Hom.set_map by (elim C.in_homE, auto)
also have "... = S.Fun (S (Cones.map (ψ (a', a) x)) (Φ a)) (φ (a, a) a)"
using ψx is_natural_1 [of "ψ (a', a) x"] is_natural_2 [of "ψ (a', a) x"] by auto
also have "... = (Cones.FUN (ψ (a', a) x) o Φ.FUN a) (φ (a, a) a)"
proof -
have "S.seq (Cones.map (ψ (a', a) x)) (Φ a)"
using Ya.ide_a ψx Cones.map_preserves_dom [of "ψ (a', a) x"]
apply (intro S.seqI)
apply auto[2]
by fastforce
thus ?thesis
using Ya.ide_a φa Hom.set_map by auto
qed
finally show ?thesis by simp
qed
also have "... = Cones.FUN (ψ (a', a) x) (ι χ)" using ιχ by simp
finally show ?thesis by auto
qed
lemma χ_is_universal:
assumes "D.cone a' χ'"
shows "«ψ (a', a) (Ψ.FUN a' (ι χ')) : a' → a»"
and "D.cones_map (ψ (a', a) (Ψ.FUN a' (ι χ'))) χ = χ'"
and "⟦ «f' : a' → a»; D.cones_map f' χ = χ' ⟧ ⟹ f' = ψ (a', a) (Ψ.FUN a' (ι χ'))"
proof -
interpret χ': cone J C D a' χ' using assms by auto
have a': "C.ide a'" using χ'.ide_apex by simp
have ιχ': "ι χ' ∈ Cones.SET a'" using assms a' Cones_SET_eq_ι_img_cones by auto
let ?f = "ψ (a', a) (Ψ.FUN a' (ι χ'))"
have A: "Ψ.FUN a' (ι χ') ∈ Hom.set (a', a)"
proof -
have "Ψ.FUN a' ∈ Cones.SET a' → Ya.SET a'"
using a' Ψ.preserves_hom [of a' a' a'] S.Fun_mapsto [of "Ψ.map a'"] by fastforce
thus ?thesis using a' ιχ' Ya.ide_a Hom.set_map by auto
qed
show f: "«?f : a' → a»" using A a' Ya.ide_a Hom.ψ_mapsto [of a' a] by auto
have E: "⋀f. «f : a' → a» ⟹ Cones.FUN f (ι χ) = Φ.FUN a' (φ (a', a) f)"
proof -
fix f
assume f: "«f : a' → a»"
have "φ (a', a) f ∈ Hom.set (a', a)"
using a' Ya.ide_a f Hom.φ_mapsto by auto
thus "Cones.FUN f (ι χ) = Φ.FUN a' (φ (a', a) f)"
using a' f Φ_FUN_simp by simp
qed
have I: "Φ.FUN a' (Ψ.FUN a' (ι χ')) = ι χ'"
proof -
have "Φ.FUN a' (Ψ.FUN a' (ι χ')) =
compose (Ψ.DOM a') (Φ.FUN a') (Ψ.FUN a') (ι χ')"
using a' ιχ' Cones.map_ide Ψ.preserves_hom [of a' a' a'] by force
also have "... = (λx ∈ Ψ.DOM a'. x) (ι χ')"
using a' Ψ.inverts_components S.inverse_arrows_char by force
also have "... = ι χ'"
using a' ιχ' Cones.map_ide Ψ.preserves_hom [of a' a' a'] by force
finally show ?thesis by auto
qed
show fχ: "D.cones_map ?f χ = χ'"
proof -
have "D.cones_map ?f χ = (𝗈 o Cones.FUN ?f o ι) χ"
using f Cones.preserves_arr [of ?f] cone_χ
by (cases "D.cone a χ", auto)
also have "... = χ'"
using f Ya.ide_a a' A E I by auto
finally show ?thesis by auto
qed
show "⟦ «f' : a' → a»; D.cones_map f' χ = χ' ⟧ ⟹ f' = ?f"
proof -
assume f': "«f' : a' → a»" and f'χ: "D.cones_map f' χ = χ'"
show "f' = ?f"
proof -
have 1: "φ (a', a) f' ∈ Hom.set (a', a) ∧ φ (a', a) ?f ∈ Hom.set (a', a)"
using Ya.ide_a a' f f' Hom.φ_mapsto by auto
have "S.iso (Φ a')" using χ'.ide_apex components_are_iso by auto
hence 2: "S.arr (Φ a') ∧ bij_betw (Φ.FUN a') (Hom.set (a', a)) (Cones.SET a')"
using Ya.ide_a a' S.iso_char Hom.set_map by auto
have "Φ.FUN a' (φ (a', a) f') = Φ.FUN a' (φ (a', a) ?f)"
proof -
have "Φ.FUN a' (φ (a', a) ?f) = ι χ'"
using A I Hom.φ_ψ Ya.ide_a a' by simp
also have "... = Cones.FUN f' (ι χ)"
using f f' A E cone_χ Cones.preserves_arr fχ f'χ by (elim C.in_homE, auto)
also have "... = Φ.FUN a' (φ (a', a) f')"
using f' E by simp
finally show ?thesis by argo
qed
moreover have "inj_on (Φ.FUN a') (Hom.set (a', a))"
using 2 bij_betw_imp_inj_on by blast
ultimately have 3: "φ (a', a) f' = φ (a', a) ?f"
using 1 inj_on_def [of "Φ.FUN a'" "Hom.set (a', a)"] by blast
show ?thesis
proof -
have "f' = ψ (a', a) (φ (a', a) f')"
using Ya.ide_a a' f' Hom.ψ_φ by simp
also have "... = ψ (a', a) (Ψ.FUN a' (ι χ'))"
using Ya.ide_a a' Hom.ψ_φ A 3 by simp
finally show ?thesis by blast
qed
qed
qed
qed
interpretation χ: limit_cone J C D a χ
proof
show "⋀a' χ'. D.cone a' χ' ⟹ ∃!f. «f : a' → a» ∧ D.cones_map f χ = χ'"
proof -
fix a' χ'
assume 1: "D.cone a' χ'"
show "∃!f. «f : a' → a» ∧ D.cones_map f χ = χ'"
proof
show "«ψ (a', a) (Ψ.FUN a' (ι χ')) : a' → a» ∧
D.cones_map (ψ (a', a) (Ψ.FUN a' (ι χ'))) χ = χ'"
using 1 χ_is_universal by blast
show "⋀f. «f : a' → a» ∧ D.cones_map f χ = χ' ⟹ f = ψ (a', a) (Ψ.FUN a' (ι χ'))"
using 1 χ_is_universal by blast
qed
qed
qed
lemma χ_is_limit_cone:
shows "D.limit_cone a χ" ..
lemma induces_limit_situation:
shows "limit_situation J C D S φ ι a Φ χ"
proof
show "χ = χ" by simp
fix a'
assume a': "Cop.ide a'"
let ?F = "λx. ι (D.cones_map (ψ (a', a) x) χ)"
show "Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F"
proof -
have 1: "«Φ a' : S.mkIde (Hom.set (a', a)) →⇩S S.mkIde (ι ` D.cones a')»"
using a' Cones.map_ide Ya.ide_a by auto
moreover have "Φ.DOM a' = Hom.set (a', a)"
using 1 Hom.set_subset_Univ a' Ya.ide_a Hom.set_map by simp
moreover have "Φ.COD a' = ι ` D.cones a'"
using a' Cones_SET_eq_ι_img_cones by fastforce
ultimately have 2: "Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (Φ.FUN a')"
using S.mkArr_Fun [of "Φ a'"] by fastforce
also have "... = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F"
proof
show "S.arr (S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (Φ.FUN a'))"
using 1 2 by auto
show "⋀x. x ∈ Hom.set (a', a) ⟹ Φ.FUN a' x = ?F x"
proof -
fix x
assume x: "x ∈ Hom.set (a', a)"
hence ψx: "«ψ (a', a) x : a' → a»"
using a' Ya.ide_a Hom.ψ_mapsto by auto
show "Φ.FUN a' x = ?F x"
proof -
have "Φ.FUN a' x = Cones.FUN (ψ (a', a) x) (ι χ)"
using a' x Φ_FUN_simp by simp
also have "... = restrict (ι o D.cones_map (ψ (a', a) x) o 𝗈) (ι ` D.cones a) (ι χ)"
using ψx Cones.map_simp Cones.preserves_arr [of "ψ (a', a) x"] S.Fun_mkArr
by (elim C.in_homE, auto)
also have "... = ?F x" using cone_χ by simp
ultimately show ?thesis by simp
qed
qed
qed
finally show "Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F" by auto
qed
qed
end
sublocale representation_of_cones_functor ⊆ limit_situation J C D S φ ι a Φ χ
using induces_limit_situation by auto
section "Categories with Limits"
context category
begin
text‹
A category @{term[source=true] C} has limits of shape @{term J} if every diagram of shape
@{term J} admits a limit cone.
›
definition has_limits_of_shape
where "has_limits_of_shape J ≡ ∀D. diagram J C D ⟶ (∃a χ. limit_cone J C D a χ)"
text‹
A category has limits at a type @{typ 'j} if it has limits of shape @{term J}
for every category @{term J} whose arrows are of type @{typ 'j}.
›
definition has_limits
where "has_limits (_ :: 'j) ≡ ∀J :: 'j comp. category J ⟶ has_limits_of_shape J"
text‹
Whether a category has limits of shape ‹J› truly depends only on the ``shape''
(\emph{i.e.}~isomorphism class) of ‹J› and not on details of its construction.
›
lemma has_limits_preserved_by_isomorphism:
assumes "has_limits_of_shape J" and "isomorphic_categories J J'"
shows "has_limits_of_shape J'"
proof -
interpret J: category J
using assms(2) isomorphic_categories_def isomorphic_categories_axioms_def by auto
interpret J': category J'
using assms(2) isomorphic_categories_def isomorphic_categories_axioms_def by auto
from assms(2) obtain φ ψ where IF: "inverse_functors J' J φ ψ"
using isomorphic_categories_def isomorphic_categories_axioms_def
inverse_functors_sym
by blast
interpret IF: inverse_functors J' J φ ψ using IF by auto
have ψφ: "ψ o φ = J.map" using IF.inv by metis
have φψ: "φ o ψ = J'.map" using IF.inv' by metis
have "⋀D'. diagram J' C D' ⟹ ∃a χ. limit_cone J' C D' a χ"
proof -
fix D'
assume D': "diagram J' C D'"
interpret D': diagram J' C D' using D' by auto
interpret D: composite_functor J J' C φ D' ..
interpret D: diagram J C ‹D' o φ› ..
have D: "diagram J C (D' o φ)" ..
from assms(1) obtain a χ where χ: "D.limit_cone a χ"
using D has_limits_of_shape_def by blast
interpret χ: limit_cone J C ‹D' o φ› a χ using χ by auto
interpret A': constant_functor J' C a
using χ.ide_apex by (unfold_locales, auto)
have χoψ: "cone J' C (D' o φ o ψ) a (χ o ψ)"
using comp_cone_functor IF.G.functor_axioms χ.cone_axioms by fastforce
hence χoψ: "cone J' C D' a (χ o ψ)"
using φψ by (metis D'.functor_axioms Fun.comp_assoc comp_functor_identity)
interpret χoψ: cone J' C D' a ‹χ o ψ› using χoψ by auto
interpret χoψ: limit_cone J' C D' a ‹χ o ψ›
proof
fix a' χ'
assume χ': "D'.cone a' χ'"
interpret χ': cone J' C D' a' χ' using χ' by auto
have χ'oφ: "cone J C (D' o φ) a' (χ' o φ)"
using χ' comp_cone_functor IF.F.functor_axioms by fastforce
interpret χ'oφ: cone J C ‹D' o φ› a' ‹χ' o φ› using χ'oφ by auto
have "cone J C (D' o φ) a' (χ' o φ)" ..
hence 1: "∃!f. «f : a' → a» ∧ D.cones_map f χ = χ' o φ"
using χ.is_universal by simp
show "∃!f. «f : a' → a» ∧ D'.cones_map f (χ o ψ) = χ'"
proof
let ?f = "THE f. «f : a' → a» ∧ D.cones_map f χ = χ' o φ"
have f: "«?f : a' → a» ∧ D.cones_map ?f χ = χ' o φ"
using 1 theI' [of "λf. «f : a' → a» ∧ D.cones_map f χ = χ' o φ"] by blast
have f_in_hom: "«?f : a' → a»" using f by blast
have "D'.cones_map ?f (χ o ψ) = χ'"
proof
fix j'
have "¬J'.arr j' ⟹ D'.cones_map ?f (χ o ψ) j' = χ' j'"
proof -
assume j': "¬J'.arr j'"
have "D'.cones_map ?f (χ o ψ) j' = null"
using j' f_in_hom χoψ by fastforce
thus ?thesis
using j' χ'.is_extensional by simp
qed
moreover have "J'.arr j' ⟹ D'.cones_map ?f (χ o ψ) j' = χ' j'"
proof -
assume j': "J'.arr j'"
have "D'.cones_map ?f (χ o ψ) j' = χ (ψ j') ⋅ ?f"
using j' f χoψ by fastforce
also have "... = D.cones_map ?f χ (ψ j')"
using j' f_in_hom χ χ.is_cone by fastforce
also have "... = χ' j'"
using j' f χ φψ Fun.comp_def J'.map_simp by metis
finally show "D'.cones_map ?f (χ o ψ) j' = χ' j'" by auto
qed
ultimately show "D'.cones_map ?f (χ o ψ) j' = χ' j'" by blast
qed
thus "«?f : a' → a» ∧ D'.cones_map ?f (χ o ψ) = χ'" using f by auto
fix f'
assume f': "«f' : a' → a» ∧ D'.cones_map f' (χ o ψ) = χ'"
have "D.cones_map f' χ = χ' o φ"
proof
fix j
have "¬J.arr j ⟹ D.cones_map f' χ j = (χ' o φ) j"
using f' χ χ'oφ.is_extensional χ.is_cone mem_Collect_eq restrict_apply by auto
moreover have "J.arr j ⟹ D.cones_map f' χ j = (χ' o φ) j"
proof -
assume j: "J.arr j"
have "D.cones_map f' χ j = C (χ j) f'"
using j f' χ.is_cone by auto
also have "... = C ((χ o ψ) (φ j)) f'"
using j f' ψφ by (metis comp_apply J.map_simp)
also have "... = D'.cones_map f' (χ o ψ) (φ j)"
using j f' χoψ by fastforce
also have "... = (χ' o φ) j"
using j f' by auto
finally show "D.cones_map f' χ j = (χ' o φ) j" by auto
qed
ultimately show "D.cones_map f' χ j = (χ' o φ) j" by blast
qed
hence "«f' : a' → a» ∧ D.cones_map f' χ = χ' o φ"
using f' by auto
moreover have "⋀P x x'. (∃!x. P x) ∧ P x ∧ P x' ⟹ x = x'"
by auto
ultimately show "f' = ?f" using 1 f by blast
qed
qed
have "limit_cone J' C D' a (χ o ψ)" ..
thus "∃a χ. limit_cone J' C D' a χ" by blast
qed
thus ?thesis using has_limits_of_shape_def by auto
qed
end
subsection "Diagonal Functors"
text‹
The existence of limits can also be expressed in terms of adjunctions: a category @{term C}
has limits of shape @{term J} if the diagonal functor taking each object @{term a}
in @{term C} to the constant-@{term a} diagram and each arrow ‹f ∈ C.hom a a'›
to the constant-@{term f} natural transformation between diagrams is a left adjoint functor.
›
locale diagonal_functor =
C: category C +
J: category J +
J_C: functor_category J C
for J :: "'j comp" (infixr "⋅⇩J" 55)
and C :: "'c comp" (infixr "⋅" 55)
begin
notation J.in_hom ("«_ : _ →⇩J _»")
notation J_C.comp (infixr "⋅⇩[⇩J⇩,⇩C⇩]" 55)
notation J_C.in_hom ("«_ : _ →⇩[⇩J⇩,⇩C⇩] _»")
definition map :: "'c ⇒ ('j, 'c) J_C.arr"
where "map f = (if C.arr f then J_C.MkArr (constant_functor.map J C (C.dom f))
(constant_functor.map J C (C.cod f))
(constant_transformation.map J C f)
else J_C.null)"
lemma is_functor:
shows "functor C J_C.comp map"
proof
fix f
show "¬ C.arr f ⟹ local.map f = J_C.null"
using map_def by simp
assume f: "C.arr f"
interpret Dom_f: constant_functor J C ‹C.dom f›
using f by (unfold_locales, auto)
interpret Cod_f: constant_functor J C ‹C.cod f›
using f by (unfold_locales, auto)
interpret Fun_f: constant_transformation J C f
using f by (unfold_locales, auto)
show 1: "J_C.arr (map f)"
using f map_def by (simp add: Fun_f.natural_transformation_axioms)
show "J_C.dom (map f) = map (C.dom f)"
proof -
have "constant_transformation J C (C.dom f)"
using f by unfold_locales auto
hence "constant_transformation.map J C (C.dom f) = Dom_f.map"
using Dom_f.map_def constant_transformation.map_def [of J C "C.dom f"] by auto
thus ?thesis using f 1 by (simp add: map_def J_C.dom_char)
qed
show "J_C.cod (map f) = map (C.cod f)"
proof -
have "constant_transformation J C (C.cod f)"
using f by unfold_locales auto
hence "constant_transformation.map J C (C.cod f) = Cod_f.map"
using Cod_f.map_def constant_transformation.map_def [of J C "C.cod f"] by auto
thus ?thesis using f 1 by (simp add: map_def J_C.cod_char)
qed
next
fix f g
assume g: "C.seq g f"
have f: "C.arr f" using g by auto
interpret Dom_f: constant_functor J C ‹C.dom f›
using f by unfold_locales auto
interpret Cod_f: constant_functor J C ‹C.cod f›
using f by unfold_locales auto
interpret Fun_f: constant_transformation J C f
using f by unfold_locales auto
interpret Cod_g: constant_functor J C ‹C.cod g›
using g by unfold_locales auto
interpret Fun_g: constant_transformation J C g
using g by unfold_locales auto
interpret Fun_g: natural_transformation J C Cod_f.map Cod_g.map Fun_g.map
apply unfold_locales
using f g C.seqE [of g f] C.comp_arr_dom C.comp_cod_arr Fun_g.is_extensional by auto
interpret Fun_fg: vertical_composite
J C Dom_f.map Cod_f.map Cod_g.map Fun_f.map Fun_g.map ..
have 1: "J_C.arr (map f)"
using f map_def by (simp add: Fun_f.natural_transformation_axioms)
show "map (g ⋅ f) = map g ⋅⇩[⇩J⇩,⇩C⇩] map f"
proof -
have "map (C g f) = J_C.MkArr Dom_f.map Cod_g.map
(constant_transformation.map J C (C g f))"
using f g map_def by simp
also have "... = J_C.MkArr Dom_f.map Cod_g.map (λj. if J.arr j then C g f else C.null)"
proof -
have "constant_transformation J C (g ⋅ f)"
using g by unfold_locales auto
thus ?thesis using constant_transformation.map_def by metis
qed
also have "... = J_C.comp (J_C.MkArr Cod_f.map Cod_g.map Fun_g.map)
(J_C.MkArr Dom_f.map Cod_f.map Fun_f.map)"
proof -
have "J_C.MkArr Cod_f.map Cod_g.map Fun_g.map ⋅⇩[⇩J⇩,⇩C⇩]
J_C.MkArr Dom_f.map Cod_f.map Fun_f.map
= J_C.MkArr Dom_f.map Cod_g.map Fun_fg.map"
using J_C.comp_char J_C.comp_MkArr Fun_f.natural_transformation_axioms
Fun_g.natural_transformation_axioms
by blast
also have "... = J_C.MkArr Dom_f.map Cod_g.map
(λj. if J.arr j then g ⋅ f else C.null)"
using Fun_fg.is_extensional Fun_fg.map_simp_2 by auto
finally show ?thesis by auto
qed
also have "... = map g ⋅⇩[⇩J⇩,⇩C⇩] map f"
using f g map_def by fastforce
finally show ?thesis by auto
qed
qed
sublocale "functor" C J_C.comp map
using is_functor by auto
text‹
The objects of ‹[J, C]› correspond bijectively to diagrams of shape @{term J}
in @{term C}.
›
lemma ide_determines_diagram:
assumes "J_C.ide d"
shows "diagram J C (J_C.Map d)" and "J_C.MkIde (J_C.Map d) = d"
proof -
interpret δ: natural_transformation J C ‹J_C.Map d› ‹J_C.Map d› ‹J_C.Map d›
using assms J_C.ide_char J_C.arr_MkArr by fastforce
interpret D: "functor" J C ‹J_C.Map d› ..
show "diagram J C (J_C.Map d)" ..
show "J_C.MkIde (J_C.Map d) = d"
using assms J_C.ide_char by (metis J_C.ideD(1) J_C.MkArr_Map)
qed
lemma diagram_determines_ide:
assumes "diagram J C D"
shows "J_C.ide (J_C.MkIde D)" and "J_C.Map (J_C.MkIde D) = D"
proof -
interpret D: diagram J C D using assms by auto
show "J_C.ide (J_C.MkIde D)" using J_C.ide_char
using D.functor_axioms J_C.ide_MkIde by auto
thus "J_C.Map (J_C.MkIde D) = D"
using J_C.in_homE by simp
qed
lemma bij_betw_ide_diagram:
shows "bij_betw J_C.Map (Collect J_C.ide) (Collect (diagram J C))"
proof (intro bij_betwI)
show "J_C.Map ∈ Collect J_C.ide → Collect (diagram J C)"
using ide_determines_diagram by blast
show "J_C.MkIde ∈ Collect (diagram J C) → Collect J_C.ide"
using diagram_determines_ide by blast
show "⋀d. d ∈ Collect J_C.ide ⟹ J_C.MkIde (J_C.Map d) = d"
using ide_determines_diagram by blast
show "⋀D. D ∈ Collect (diagram J C) ⟹ J_C.Map (J_C.MkIde D) = D"
using diagram_determines_ide by blast
qed
text‹
Arrows from from the diagonal functor correspond bijectively to cones.
›
lemma arrow_determines_cone:
assumes "J_C.ide d" and "arrow_from_functor C J_C.comp map a d x"
shows "cone J C (J_C.Map d) a (J_C.Map x)"
and "J_C.MkArr (constant_functor.map J C a) (J_C.Map d) (J_C.Map x) = x"
proof -
interpret D: diagram J C ‹J_C.Map d›
using assms ide_determines_diagram by auto
interpret x: arrow_from_functor C J_C.comp map a d x
using assms by auto
interpret A: constant_functor J C a
using x.arrow by (unfold_locales, auto)
interpret α: constant_transformation J C a
using x.arrow by (unfold_locales, auto)
have Dom_x: "J_C.Dom x = A.map"
using J_C.in_hom_char map_def x.arrow by force
have Cod_x: "J_C.Cod x = J_C.Map d"
using x.arrow by auto
interpret χ: natural_transformation J C A.map ‹J_C.Map d› ‹J_C.Map x›
using x.arrow J_C.arr_char [of x] Dom_x Cod_x by force
show "D.cone a (J_C.Map x)" ..
show "J_C.MkArr A.map (J_C.Map d) (J_C.Map x) = x"
using x.arrow Dom_x Cod_x χ.natural_transformation_axioms
by (intro J_C.arr_eqI, auto)
qed
lemma cone_determines_arrow:
assumes "J_C.ide d" and "cone J C (J_C.Map d) a χ"
shows "arrow_from_functor C J_C.comp map a d
(J_C.MkArr (constant_functor.map J C a) (J_C.Map d) χ)"
and "J_C.Map (J_C.MkArr (constant_functor.map J C a) (J_C.Map d) χ) = χ"
proof -
interpret χ: cone J C ‹J_C.Map d› a χ using assms(2) by auto
let ?x = "J_C.MkArr χ.A.map (J_C.Map d) χ"
interpret x: arrow_from_functor C J_C.comp map a d ?x
proof
have "«J_C.MkArr χ.A.map (J_C.Map d) χ :
J_C.MkIde χ.A.map →⇩[⇩J⇩,⇩C⇩] J_C.MkIde (J_C.Map d)»"
using χ.natural_transformation_axioms by auto
moreover have "J_C.MkIde χ.A.map = map a"
using χ.A.value_is_ide map_def χ.A.map_def C.ide_char
by (metis (no_types, lifting) J_C.dom_MkArr preserves_arr preserves_dom)
moreover have "J_C.MkIde (J_C.Map d) = d"
using assms ide_determines_diagram(2) by simp
ultimately show "C.ide a ∧ «J_C.MkArr χ.A.map (J_C.Map d) χ : map a →⇩[⇩J⇩,⇩C⇩] d»"
using χ.A.value_is_ide by simp
qed
show "arrow_from_functor C J_C.comp map a d ?x" ..
show "J_C.Map (J_C.MkArr (constant_functor.map J C a) (J_C.Map d) χ) = χ"
by (simp add: χ.natural_transformation_axioms)
qed
text‹
Transforming a cone by composing at the apex with an arrow @{term g} corresponds,
via the preceding bijections, to composition in ‹[J, C]› with the image of @{term g}
under the diagonal functor.
›
lemma cones_map_is_composition:
assumes "«g : a' → a»" and "cone J C D a χ"
shows "J_C.MkArr (constant_functor.map J C a') D (diagram.cones_map J C D g χ)
= J_C.MkArr (constant_functor.map J C a) D χ ⋅⇩[⇩J⇩,⇩C⇩] map g"
proof -
interpret A: constant_transformation J C a
using assms(1) by (unfold_locales, auto)
interpret χ: cone J C D a χ using assms(2) by auto
have cone_χ: "cone J C D a χ" ..
interpret A': constant_transformation J C a'
using assms(1) by (unfold_locales, auto)
let ?χ' = "χ.D.cones_map g χ"
interpret χ': cone J C D a' ?χ'
using assms(1) cone_χ χ.D.cones_map_mapsto by blast
let ?x = "J_C.MkArr χ.A.map D χ"
let ?x' = "J_C.MkArr χ'.A.map D ?χ'"
show "?x' = J_C.comp ?x (map g)"
proof (intro J_C.arr_eqI)
have x: "J_C.arr ?x"
using χ.natural_transformation_axioms J_C.arr_char [of ?x] by simp
show x': "J_C.arr ?x'"
using χ'.natural_transformation_axioms J_C.arr_char [of ?x'] by simp
have 3: "«?x : map a →⇩[⇩J⇩,⇩C⇩] J_C.MkIde D»"
using χ.D.diagram_axioms arrow_from_functor.arrow cone_χ cone_determines_arrow(1)
diagram_determines_ide(1)
by fastforce
have 4: "«?x' : map a' →⇩[⇩J⇩,⇩C⇩] J_C.MkIde D»"
by (metis (no_types, lifting) J_C.Dom.simps(1) J_C.Dom_cod J_C.Map_cod
J_C.cod_MkArr χ'.cone_axioms arrow_from_functor.arrow category.ide_cod
cone_determines_arrow(1) functor_def is_functor x)
have seq_xg: "J_C.seq ?x (map g)"
using assms(1) 3 preserves_hom [of g] by (intro J_C.seqI', auto)
show 2: "J_C.seq ?x (map g)"
using seq_xg J_C.seqI' by blast
show "J_C.Dom ?x' = J_C.Dom (?x ⋅⇩[⇩J⇩,⇩C⇩] map g)"
proof -
have "J_C.Dom ?x' = J_C.Dom (J_C.dom ?x')"
using x' J_C.Dom_dom by simp
also have "... = J_C.Dom (map a')"
using 4 by force
also have "... = J_C.Dom (J_C.dom (?x ⋅⇩[⇩J⇩,⇩C⇩] map g))"
using assms(1) 2 by auto
also have "... = J_C.Dom (?x ⋅⇩[⇩J⇩,⇩C⇩] map g)"
using seq_xg J_C.Dom_dom J_C.seqI' by blast
finally show ?thesis by auto
qed
show "J_C.Cod ?x' = J_C.Cod (?x ⋅⇩[⇩J⇩,⇩C⇩] map g)"
proof -
have "J_C.Cod ?x' = J_C.Cod (J_C.cod ?x')"
using x' J_C.Cod_cod by simp
also have "... = J_C.Cod (J_C.MkIde D)"
using 4 by force
also have "... = J_C.Cod (J_C.cod (?x ⋅⇩[⇩J⇩,⇩C⇩] map g))"
using 2 3 J_C.cod_comp J_C.in_homE by metis
also have "... = J_C.Cod (?x ⋅⇩[⇩J⇩,⇩C⇩] map g)"
using seq_xg J_C.Cod_cod J_C.seqI' by blast
finally show ?thesis by auto
qed
show "J_C.Map ?x' = J_C.Map (?x ⋅⇩[⇩J⇩,⇩C⇩] map g)"
proof -
interpret g: constant_transformation J C g
apply unfold_locales using assms(1) by auto
interpret χog: vertical_composite J C A'.map χ.A.map D g.map χ
using assms(1) C.comp_arr_dom C.comp_cod_arr A'.is_extensional g.is_extensional
apply (unfold_locales, auto)
by (elim J.seqE, auto)
have "J_C.Map (?x ⋅⇩[⇩J⇩,⇩C⇩] map g) = χog.map"
using assms(1) 2 J_C.comp_char map_def by auto
also have "... = J_C.Map ?x'"
using x' χog.map_def J_C.arr_char [of ?x'] natural_transformation.is_extensional
assms(1) cone_χ χog.map_simp_2
by fastforce
finally show ?thesis by auto
qed
qed
qed
text‹
Coextension along an arrow from a functor is equivalent to a transformation of cones.
›
lemma coextension_iff_cones_map:
assumes x: "arrow_from_functor C J_C.comp map a d x"
and g: "«g : a' → a