Theory Colimit
chapter Colimit
theory Colimit
imports Category3.Limit
begin
text‹
After mulling it over for a long time, I do not have any strong sense that it would be
simpler or more useful to try to come up with some clever way of dualizing the material
in @{theory Category3.Limit}, than just to do the dualization directly. This theory
therefore contains (a portion of) such a direct dualization, including at least the general
definitions of cocone and colimit, and including particular special cases of colimits
that I have wanted to work with. I have omitted theorems about preservation of colimits
for now.
›
section "Diagrams and Cocones"
text‹
A \emph{cocone} over a diagram ‹D: J → C› is a natural transformation
from @{term D} to a constant functor. The value of the constant functor is
the \emph{apex} of the cocone.
›
locale cocone =
C: category C +
J: category J +
D: diagram J C D +
A: constant_functor J C a +
natural_transformation J C D A.map χ
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 : D (J.dom j) → a»"
using assms by auto
lemma dom_determines_component:
assumes "J.arr j"
shows "χ j = χ (J.dom j)"
by (metis A.map_simp J.arr_dom_iff_arr J.dom_dom assms naturality1)
end
text‹
A cocone over diagram @{term D} is transformed into a cocone over diagram @{term "D o F"}
by pre-composing with @{term F}.
›
lemma comp_cocone_functor:
assumes "cocone J C D a χ" and "functor J' J F"
shows "cocone J' C (D o F) a (χ o F)"
proof -
interpret χ: cocone 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 ‹D o F› A'.map ‹χ o F›
using 1 horizontal_composite F.as_nat_trans.natural_transformation_axioms
χ.natural_transformation_axioms
by fastforce
show "cocone J' C (D o F) a (χ o F)" ..
qed
text‹
A cocone over diagram @{term D} can be transformed into a cocone over a diagram @{term D'}
by pre-composing with a natural transformation from @{term D'} to @{term D}.
›
lemma vcomp_transformation_cocone:
assumes "cocone J C D a χ"
and "natural_transformation J C D' D τ"
shows "cocone J C D' a (vertical_composite.map J C τ χ)"
by (meson assms(1,2) cocone.axioms(4,5) cocone.intro diagram.intro natural_transformation_def
vertical_composite.intro vertical_composite.is_natural_transformation)
context "functor"
begin
lemma preserves_cocones:
fixes J :: "'j comp"
assumes "cocone J A D a χ"
shows "cocone J B (F o D) (F a) (F o χ)"
proof -
interpret χ: cocone 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 extensionality Fa.extensionality χ.A.extensionality
by (cases "χ.J.arr f", simp_all)
qed
interpret χ': natural_transformation J B ‹F o D› Fa.map ‹F o χ›
using 1 horizontal_composite χ.natural_transformation_axioms
as_nat_trans.natural_transformation_axioms
by fastforce
show "cocone J B (F o D) (F a) (F o χ)" ..
qed
end
context diagram
begin
abbreviation cocone
where "cocone a χ ≡ Colimit.cocone J C D a χ"
abbreviation cocones :: "'c ⇒ ('j ⇒ 'c) set"
where "cocones a ≡ { χ. cocone a χ }"
text‹
An arrow @{term "f ∈ C.hom a a'"} induces by composition a transformation from
cocones with apex @{term a} to cocones with apex @{term a'}. This transformation
is functorial in @{term f}.
›
abbreviation cocones_map :: "'c ⇒ ('j ⇒ 'c) ⇒ ('j ⇒ 'c)"
where "cocones_map f ≡ (λχ ∈ cocones (C.dom f). λj. if J.arr j then f ⋅ χ j else C.null)"
lemma cocones_map_mapsto:
assumes "C.arr f"
shows "cocones_map f ∈
extensional (cocones (C.dom f)) ∩ (cocones (C.dom f) → cocones (C.cod f))"
proof
show "cocones_map f ∈ extensional (cocones (C.dom f))" by blast
show "cocones_map f ∈ cocones (C.dom f) → cocones (C.cod f)"
proof
fix χ
assume "χ ∈ cocones (C.dom f)"
hence χ: "cocone (C.dom f) χ" by auto
interpret χ: cocone J C D ‹C.dom f› χ using χ by auto
interpret B: constant_functor J C ‹C.cod f›
using assms by unfold_locales auto
have "cocone (C.cod f) (λj. if J.arr j then f ⋅ χ j else C.null)"
using assms B.value_is_ide
apply (unfold_locales, simp_all)
apply (metis C.comp_assoc C.comp_cod_arr χ.dom_determines_component)
by (simp add: C.comp_assoc)
thus "(λj. if J.arr j then f ⋅ χ j else C.null) ∈ cocones (C.cod f)" by auto
qed
qed
lemma cocones_map_ide:
assumes "χ ∈ cocones a"
shows "cocones_map a χ = χ"
proof -
interpret χ: cocone J C D a χ using assms by auto
show ?thesis
using assms χ.A.value_is_ide χ.preserves_hom C.comp_cod_arr χ.extensionality
by auto
qed
lemma cocones_map_comp:
assumes "C.seq g f"
shows "cocones_map (g ⋅ f) = restrict (cocones_map g o cocones_map f) (cocones (C.dom f))"
proof (intro restr_eqI)
show "cocones (C.dom (g ⋅ f)) = cocones (C.dom f)" using assms by simp
show "⋀χ. χ ∈ cocones (C.dom (g ⋅ f)) ⟹
(λj. if J.arr j then (g ⋅ f) ⋅ χ j else C.null) =
(cocones_map g o cocones_map f) χ"
proof -
fix χ
assume χ: "χ ∈ cocones (C.dom (g ⋅ f))"
show "(λj. if J.arr j then (g ⋅ f) ⋅ χ j else C.null) = (cocones_map g o cocones_map f) χ"
proof -
have "((cocones_map g) o (cocones_map f)) χ = cocones_map g (cocones_map f χ)"
by force
also have "... = (λj. if J.arr j
then g ⋅ (λj. if J.arr j then f ⋅ χ j else C.null) j
else C.null)"
proof
fix j
have "cocone (C.cod f) (cocones_map f χ)"
using assms χ cocones_map_mapsto by (elim C.seqE, force)
thus "cocones_map g (cocones_map f χ) j =
(if J.arr j then g ⋅ (λj. if J.arr j then f ⋅ χ j else C.null) j else C.null)"
using χ assms by auto
qed
also have "... = (λj. if J.arr j then (g ⋅ f) ⋅ χ j else C.null)"
using C.comp_assoc by fastforce
finally show ?thesis by auto
qed
qed
qed
end
text‹
Changing the apex of a cocone by post-composing with an arrow @{term f} commutes
with changing the diagram of a cocone by pre-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 natural_transformation_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χ.extensionality 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
section "Colimits"
subsection "Colimit Cocones"
text‹
A \emph{colimit cocone} for a diagram @{term D} is a cocone @{term χ} over @{term D}
with the couniversal property that any other cocone @{term χ'} over the diagram @{term D}
factors uniquely through @{term χ}.
›
locale colimit_cocone =
C: category C +
J: category J +
D: diagram J C D +
cocone 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_couniversal: "cocone J C D a' χ' ⟹ ∃!f. «f : a → a'» ∧ D.cocones_map f χ = χ'"
begin
lemma is_cocone [simp]:
shows "χ ∈ D.cocones a"
using cocone_axioms by simp
definition induced_arrow :: "'c ⇒ ('j ⇒ 'c) ⇒ 'c"
where "induced_arrow a' χ' = (THE f. «f : a → a'» ∧ D.cocones_map f χ = χ')"
lemma induced_arrowI:
assumes χ': "χ' ∈ D.cocones a'"
shows "«induced_arrow a' χ' : a → a'»"
and "D.cocones_map (induced_arrow a' χ') χ = χ'"
proof -
have "∃!f. «f : a → a'» ∧ D.cocones_map f χ = χ'"
using assms χ' is_couniversal by simp
hence 1: "«induced_arrow a' χ' : a → a'» ∧ D.cocones_map (induced_arrow a' χ') χ = χ'"
using theI' [of "λf. «f : a → a'» ∧ D.cocones_map f χ = χ'"] induced_arrow_def
by presburger
show "«induced_arrow a' χ' : a → a'»" using 1 by simp
show "D.cocones_map (induced_arrow a' χ') χ = χ'" using 1 by simp
qed
lemma cocones_map_induced_arrow:
shows "induced_arrow a' ∈ D.cocones a' → C.hom a a'"
and "⋀χ'. χ' ∈ D.cocones a' ⟹ D.cocones_map (induced_arrow a' χ') χ = χ'"
using induced_arrowI by auto
lemma induced_arrow_cocones_map:
assumes "C.ide a'"
shows "(λf. D.cocones_map f χ) ∈ C.hom a a' → D.cocones a'"
and "⋀f. «f : a → a'» ⟹ induced_arrow a' (D.cocones_map f χ) = f"
proof -
have a': "C.ide a'" using assms by (simp add: cone.ide_apex)
have cocone_χ: "cocone J C D a χ" ..
show "(λf. D.cocones_map f χ) ∈ C.hom a a' → D.cocones a'"
using cocone_χ D.cocones_map_mapsto by blast
fix f
assume f: "«f : a → a'»"
show "induced_arrow a' (D.cocones_map f χ) = f"
proof -
have "D.cocones_map f χ ∈ D.cocones a'"
using f cocone_χ D.cocones_map_mapsto by blast
hence "∃!f'. «f' : a → a'» ∧ D.cocones_map f' χ = D.cocones_map f χ"
using assms is_couniversal by auto
thus ?thesis
using f induced_arrow_def
the1_equality
[of "λf'. «f' : a → a'» ∧ D.cocones_map f' χ = D.cocones_map f χ"]
by presburger
qed
qed
text‹
For a colimit cocone @{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 cocones
with apex @{term a'}.
›
lemma bij_betw_hom_and_cocones:
assumes "C.ide a'"
shows "bij_betw (λf. D.cocones_map f χ) (C.hom a a') (D.cocones a')"
proof (intro bij_betwI)
show "(λf. D.cocones_map f χ) ∈ C.hom a a' → D.cocones a'"
using assms induced_arrow_cocones_map by blast
show "induced_arrow a' ∈ D.cocones a' → C.hom a a'"
using assms cocones_map_induced_arrow by blast
show "⋀f. f ∈ C.hom a a' ⟹ induced_arrow a' (D.cocones_map f χ) = f"
using assms induced_arrow_cocones_map by blast
show "⋀χ'. χ' ∈ D.cocones a' ⟹ D.cocones_map (induced_arrow a' χ') χ = χ'"
using assms cocones_map_induced_arrow by blast
qed
lemma induced_arrow_eqI:
assumes "D.cocone a' χ'" and "«f : a → a'»" and "D.cocones_map f χ = χ'"
shows "induced_arrow a' χ' = f"
using assms is_couniversal induced_arrow_def
the1_equality [of "λf. f ∈ C.hom a a' ∧ D.cocones_map f χ = χ'" f]
by simp
lemma induced_arrow_self:
shows "induced_arrow a χ = a"
proof -
have "«a : a → a» ∧ D.cocones_map a χ = χ"
using ide_apex cocone_axioms D.cocones_map_ide by force
thus ?thesis using induced_arrow_eqI cocone_axioms by auto
qed
end
context diagram
begin
abbreviation colimit_cocone
where "colimit_cocone a χ ≡ Colimit.colimit_cocone J C D a χ"
text‹
A diagram @{term D} has object @{term a} as a colimit if @{term a} is the apex
of some colimit cocone over @{term D}.
›
abbreviation has_as_colimit :: "'c ⇒ bool"
where "has_as_colimit a ≡ (∃χ. colimit_cocone a χ)"
abbreviation has_colimit
where "has_colimit ≡ (∃a. has_as_colimit a)"
definition some_colimit :: 'c
where "some_colimit = (SOME a. has_as_colimit a)"
definition some_colimit_cocone :: "'j ⇒ 'c"
where "some_colimit_cocone = (SOME χ. colimit_cocone some_colimit χ)"
lemma colimit_cocone_some_colimit_cocone:
assumes has_colimit
shows "colimit_cocone some_colimit some_colimit_cocone"
proof -
have "∃a. has_as_colimit a" using assms by simp
hence "has_as_colimit some_colimit"
using some_colimit_def someI_ex [of "λa. ∃χ. colimit_cocone a χ"] by simp
thus "colimit_cocone some_colimit some_colimit_cocone"
using assms some_colimit_cocone_def someI_ex [of "λχ. colimit_cocone some_colimit χ"]
by simp
qed
lemma has_colimitE:
assumes has_colimit
obtains a χ where "colimit_cocone a χ"
using assms someI_ex by blast
end
section "Special Kinds of Coimits"
subsection "Coproducts"
text‹
A \emph{coproduct} in a category @{term C} is a colimit of a discrete diagram in @{term C}.
›
context discrete_diagram
begin
abbreviation mkCocone
where "mkCocone F ≡ (λj. if J.arr j then F j else C.null)"
lemma cocone_mkCocone:
assumes "C.ide a" and "⋀j. J.arr j ⟹ «F j : D j → a»"
shows "cocone a (mkCocone F)"
proof -
interpret A: constant_functor J C a
using assms(1) by unfold_locales auto
show "cocone a (mkCocone F)"
using assms(2) is_discrete
apply unfold_locales
apply auto
apply (metis C.in_homE C.comp_cod_arr)
using C.comp_arr_ide by fastforce
qed
lemma mkCocone_cocone:
assumes "cocone a π"
shows "mkCocone π = π"
proof -
interpret π: cocone J C D a π
using assms by auto
show "mkCocone π = π" using π.extensionality by auto
qed
end
locale coproduct_cocone =
J: category J +
C: category C +
D: discrete_diagram J C D +
colimit_cocone 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"
begin
lemma is_cocone:
shows "D.cocone a π" ..
lemma is_couniversal':
assumes "C.ide b" and "⋀j. J.arr j ⟹ «F j: D j → b»"
shows "∃!f. «f : a → b» ∧ (∀j. J.arr j ⟶ f ⋅ π j = F j)"
proof -
let ?χ = "D.mkCocone F"
interpret B: constant_functor J C b
using assms(1) by unfold_locales auto
have cocone_χ: "D.cocone b ?χ"
using assms D.is_discrete D.cocone_mkCocone by blast
interpret χ: cocone J C D b ?χ using cocone_χ by auto
have "∃!f. «f : a → b» ∧ D.cocones_map f π = ?χ"
using cocone_χ is_couniversal by force
moreover have
"⋀f. «f : a → b» ⟹ D.cocones_map f π = ?χ ⟷ (∀j. J.arr j ⟶ f ⋅ π j = F j)"
proof -
fix f
assume f: "«f : a → b»"
show "D.cocones_map f π = ?χ ⟷ (∀j. J.arr j ⟶ f ⋅ π j = F j)"
proof
assume 1: "D.cocones_map f π = ?χ"
show "∀j. J.arr j ⟶ f ⋅ π j = F j"
proof -
have "⋀j. J.arr j ⟹ f ⋅ π j = F j"
proof -
fix j
assume j: "J.arr j"
have "f ⋅ π j = D.cocones_map f π j"
using j f cocone_axioms by force
also have "... = F j" using j 1 by simp
finally show "f ⋅ π j = F j" by auto
qed
thus ?thesis by auto
qed
next
assume 1: "∀j. J.arr j ⟶ f ⋅ π j = F j"
show "D.cocones_map f π = ?χ"
using 1 f is_cocone χ.extensionality D.is_discrete is_cocone cocone_χ by auto
qed
qed
ultimately show ?thesis by blast
qed
abbreviation induced_arrow' :: "'c ⇒ ('j ⇒ 'c) ⇒ 'c"
where "induced_arrow' b F ≡ induced_arrow b (D.mkCocone F)"
lemma induced_arrowI':
assumes "C.ide b" and "⋀j. J.arr j ⟹ «F j : D j → b»"
shows "⋀j. J.arr j ⟹ induced_arrow' b F ⋅ π j = F j"
proof -
interpret B: constant_functor J C b
using assms(1) by unfold_locales auto
interpret χ: cocone J C D b ‹D.mkCocone F›
using assms D.cocone_mkCocone by blast
have cocone_χ: "D.cocone b (D.mkCocone F)" ..
hence 1: "D.cocones_map (induced_arrow' b F) π = D.mkCocone F"
using induced_arrowI by blast
fix j
assume j: "J.arr j"
have "induced_arrow' b F ⋅ π j = D.cocones_map (induced_arrow' b F) π j"
using induced_arrowI(1) cocone_χ is_cocone extensionality by force
also have "... = F j"
using j 1 by auto
finally show "induced_arrow' b F ⋅ π j = F j"
by auto
qed
end
context discrete_diagram
begin
lemma coproduct_coconeI:
assumes "colimit_cocone a π"
shows "coproduct_cocone J C D a π"
by (meson assms discrete_diagram_axioms functor_axioms functor_def
coproduct_cocone.intro)
end
context category
begin
definition has_as_coproduct
where "has_as_coproduct J D a ≡ (∃π. coproduct_cocone J C D a π)"
abbreviation has_coproduct
where "has_coproduct J D ≡ ∃a. has_as_coproduct J D a"
lemma coproduct_is_ide:
assumes "has_as_coproduct J D a"
shows "ide a"
proof -
obtain π where π: "coproduct_cocone J C D a π"
using assms has_as_coproduct_def by blast
interpret π: coproduct_cocone J C D a π
using π by auto
show ?thesis using π.ide_apex by auto
qed
text‹
The reason why we assume @{term "I ≠ UNIV"} in the following is the same as
for products.
›
definition has_coproducts
where "has_coproducts (I :: 'i set) ≡
I ≠ UNIV ∧
(∀J D. discrete_diagram J C D ∧ Collect (partial_composition.arr J) = I
⟶ (∃a. has_as_coproduct J D a))"
lemma has_coproductE:
assumes "has_coproduct J D"
obtains a π where "coproduct_cocone J C D a π"
using assms has_as_coproduct_def by metis
end
subsection "Coequalizers"
text‹
An \emph{coequalizer} in a category @{term C} is a colimit of a parallel pair
of arrows in @{term C}.
›
context parallel_pair_diagram
begin
definition mkCocone
where " mkCocone e ≡ λj. if J.arr j then if j = J.One then e else e ⋅ f0 else C.null"
abbreviation is_coequalized_by
where "is_coequalized_by e ≡ C.seq e f0 ∧ e ⋅ f0 = e ⋅ f1"
abbreviation has_as_coequalizer
where "has_as_coequalizer e ≡ colimit_cocone (C.cod e) (mkCocone e)"
lemma cocone_mkCocone:
assumes "is_coequalized_by e"
shows "cocone (C.cod e) (mkCocone e)"
proof -
interpret E: constant_functor J.comp C ‹C.cod e›
using assms by unfold_locales auto
show "cocone (C.cod e) (mkCocone e)"
proof (unfold_locales)
show "⋀j. ¬ J.arr j ⟹ mkCocone e j = C.null"
using assms mkCocone_def by auto
show "⋀j. J.arr j ⟹ C.arr (mkCocone e j)"
using assms mkCocone_def by auto
show "⋀j. J.arr j ⟹ mkCocone e (J.cod j) ⋅ map j = mkCocone e j"
using assms mkCocone_def C.comp_arr_dom extensionality map_def is_parallel
apply auto
using parallel_pair.arr_char by auto
show "⋀j. J.arr j ⟹ E.map j ⋅ mkCocone e (J.dom j) = mkCocone e j"
using assms mkCocone_def C.comp_cod_arr
apply auto[1]
using parallel_pair.arr_char by fastforce
qed
qed
lemma is_coequalized_by_cocone:
assumes "cocone a χ"
shows "is_coequalized_by (χ (J.One))"
proof -
interpret χ: cocone J.comp C map a χ
using assms by auto
show ?thesis
by (metis (no_types, lifting) J.arr_char J.cod_char J.dom_char χ.cocone_axioms
χ.naturality2 χ.preserves_arr cocone.dom_determines_component map_simp(3-4))
qed
lemma mkCocone_cocone:
assumes "cocone a χ"
shows "mkCocone (χ J.One) = χ"
proof -
interpret χ: cocone J.comp C map a χ
using assms by auto
have 1: "is_coequalized_by (χ J.One)"
using assms is_coequalized_by_cocone by blast
show ?thesis
proof
fix j
have "j = J.One ⟹ mkCocone (χ J.One) j = χ j"
using mkCocone_def χ.extensionality by simp
moreover have "j = J.Zero ∨ j = J.j0 ∨ j = J.j1 ⟹ mkCocone (χ J.One) j = χ j"
using J.arr_char J.cod_char J.dom_char J.seq_char mkCocone_def
χ.naturality1 χ.naturality2 χ.A.map_simp map_def
by (metis (lifting) map_simp(3))
ultimately have "J.arr j ⟹ mkCocone (χ J.One) j = χ j"
using J.arr_char by auto
thus "mkCocone (χ J.One) j = χ j"
using mkCocone_def χ.extensionality by fastforce
qed
qed
end
locale coequalizer_cocone =
J: parallel_pair +
C: category C +
D: parallel_pair_diagram C f0 f1 +
colimit_cocone J.comp C D.map "C.cod e" "D.mkCocone e"
for C :: "'c comp" (infixr ‹⋅› 55)
and f0 :: 'c
and f1 :: 'c
and e :: 'c
begin
lemma coequalizes:
shows "D.is_coequalized_by e"
proof
show "C.seq e f0"
proof (intro C.seqI)
show "C.arr e" using ide_apex C.arr_cod_iff_arr by fastforce
show "C.arr f0"
using D.map_simp D.preserves_arr J.arr_char by metis
show "C.dom e = C.cod f0"
using J.arr_char J.ide_char D.mkCocone_def D.map_simp preserves_dom by force
qed
show "e ⋅ f0 = e ⋅ f1"
using D.map_simp D.mkCocone_def J.arr_char naturality by force
qed
lemma is_couniversal':
assumes "D.is_coequalized_by e'"
shows "∃!h. «h : C.cod e → C.cod e'» ∧ h ⋅ e = e'"
proof -
have "D.cocone (C.cod e') (D.mkCocone e')"
using assms D.cocone_mkCocone by blast
moreover have 0: "D.cocone (C.cod e) (D.mkCocone e)" ..
ultimately have 1: "∃!h. «h : C.cod e → C.cod e'» ∧
D.cocones_map h (D.mkCocone e) = D.mkCocone e'"
using is_couniversal [of "C.cod e'" "D.mkCocone e'"] by auto
have 2: "⋀h. «h : C.cod e → C.cod e'» ⟹
D.cocones_map h (D.mkCocone e) = D.mkCocone e' ⟷ h ⋅ e = e'"
proof -
fix h
assume h: "«h : C.cod e → C.cod e'»"
show "D.cocones_map h (D.mkCocone e) = D.mkCocone e' ⟷ h ⋅ e = e'"
proof
assume 3: "D.cocones_map h (D.mkCocone e) = D.mkCocone e'"
show "h ⋅ e = e'"
proof -
have "e' = D.mkCocone e' J.One"
using D.mkCocone_def J.arr_char by simp
also have "... = D.cocones_map h (D.mkCocone e) J.One"
using 3 by simp
also have "... = h ⋅ e"
using 0 h D.mkCocone_def J.arr_char by auto
finally show ?thesis by auto
qed
next
assume e': "h ⋅ e = e'"
show "D.cocones_map h (D.mkCocone e) = D.mkCocone e'"
proof
fix j
have "¬J.arr j ⟹ D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j"
using h cocone_axioms D.mkCocone_def by auto
moreover have "j = J.One ⟹ D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j"
using h e' is_cocone D.mkCocone_def J.arr_char [of J.One] by force
moreover have
"J.arr j ∧ j ≠ J.One ⟹ D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j"
using C.comp_assoc D.mkCocone_def is_cocone e' h by auto
ultimately show "D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j" by blast
qed
qed
qed
thus ?thesis using 1 by blast
qed
lemma induced_arrowI':
assumes "D.is_coequalized_by e'"
shows "«induced_arrow (C.cod e') (D.mkCocone e') : C.cod e → C.cod e'»"
and "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e = e'"
proof -
interpret A': constant_functor J.comp C ‹C.cod e'›
using assms by (unfold_locales, auto)
have cocone: "D.cocone (C.cod e') (D.mkCocone e')"
using assms D.cocone_mkCocone [of e'] by blast
have "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e =
D.cocones_map (induced_arrow (C.cod e') (D.mkCocone e')) (D.mkCocone e) J.One"
using cocone induced_arrowI(1) D.mkCocone_def J.arr_char is_cocone by force
also have "... = e'"
proof -
have "D.cocones_map (induced_arrow (C.cod e') (D.mkCocone e')) (D.mkCocone e) =
D.mkCocone e'"
using cocone induced_arrowI by blast
thus ?thesis
using J.arr_char D.mkCocone_def by simp
qed
finally have 1: "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e = e'"
by auto
show "«induced_arrow (C.cod e') (D.mkCocone e') : C.cod e → C.cod e'»"
using 1 cocone induced_arrowI by simp
show "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e = e'"
using 1 cocone induced_arrowI by simp
qed
end
context category
begin
definition has_as_coequalizer
where "has_as_coequalizer f0 f1 e ≡
par f0 f1 ∧ parallel_pair_diagram.has_as_coequalizer C f0 f1 e"
definition has_coequalizers
where "has_coequalizers = (∀f0 f1. par f0 f1 ⟶ (∃e. has_as_coequalizer f0 f1 e))"
lemma has_as_coequalizerI [intro]:
assumes "par f g" and "seq e f" and "e ⋅ f = e ⋅ g"
and "⋀e'. ⟦seq e' f; e' ⋅ f = e' ⋅ g⟧ ⟹ ∃!h. h ⋅ e = e'"
shows "has_as_coequalizer f g e"
proof (unfold has_as_coequalizer_def, intro conjI)
show "arr f" and "arr g" and "dom f = dom g" and "cod f = cod g"
using assms(1) by auto
interpret J: parallel_pair .
interpret D: parallel_pair_diagram C f g
using assms(1) by unfold_locales
show "D.has_as_coequalizer e"
proof -
let ?χ = "D.mkCocone e"
let ?a = "cod e"
interpret χ: cocone J.comp C D.map ?a ?χ
using assms(2-3) D.cocone_mkCocone [of e] by simp
interpret χ: colimit_cocone J.comp C D.map ?a ?χ
proof
fix a' χ'
assume χ': "D.cocone a' χ'"
interpret χ': cocone J.comp C D.map a' χ'
using χ' by blast
have 0: "seq (χ' J.One) f"
using J.ide_char J.arr_char χ'.preserves_hom
by (meson D.is_coequalized_by_cocone χ')
have 1: "∃!h. h ⋅ e = χ' J.One"
using assms 0 χ' D.is_coequalized_by_cocone by blast
obtain h where h: "h ⋅ e = χ' J.One"
using 1 by blast
have 2: "D.is_coequalized_by e"
using assms(2-3) by blast
have "∃h. «h : cod e → a'» ∧ D.cocones_map h (D.mkCocone e) = χ'"
proof
show "«h : cod e → a'» ∧ D.cocones_map h (D.mkCocone e) = χ'"
proof
show 3: "«h : cod e → a'»"
using h χ'.preserves_cod
by (metis (no_types, lifting) χ'.A.map_simp χ'.preserves_reflects_arr
0 cod_comp seqE in_homI J.cod_simp(2))
show "D.cocones_map h (D.mkCocone e) = χ'"
proof
fix j
have "D.cocone (dom h) (D.mkCocone e)"
using 2 3 D.cocone_mkCocone by auto
thus "D.cocones_map h (D.mkCocone e) j = χ' j"
using h 2 3 D.cocone_mkCocone [of e] J.arr_char D.mkCocone_def comp_assoc
apply (cases "J.arr j")
apply simp_all
apply (metis (no_types, lifting) D.mkCocone_cocone χ')
using χ'.extensionality
by presburger
qed
qed
qed
moreover have "⋀h'. «h' : cod e → a'» ∧
D.cocones_map h' (D.mkCocone e) = χ' ⟹ h' = h"
proof (elim conjE)
fix h'
assume h': "«h' : cod e → a'»"
assume eq: "D.cocones_map h' (D.mkCocone e) = χ'"
have "h' ⋅ e = χ' J.One"
using 0 D.mkCocone_def χ.cocone_axioms eq h' by fastforce
moreover have "∃!h. h ⋅ e = χ' J.One"
using assms(2,4) 1 seqI by blast
ultimately show "h' = h"
using h by auto
qed
ultimately show "∃!h. «h : cod e → a'» ∧ D.cocones_map h (D.mkCocone e) = χ'"
by blast
qed
show "D.has_as_coequalizer e"
using assms χ.colimit_cocone_axioms by blast
qed
qed
lemma has_as_coequalizerE [elim]:
assumes "has_as_coequalizer f g e"
and "⟦seq e f; e ⋅ f = e ⋅ g; ⋀e'. ⟦seq e' f; e' ⋅ f = e' ⋅ g⟧ ⟹ ∃!h. h ⋅ e = e'⟧ ⟹ T"
shows T
proof -
interpret D: parallel_pair_diagram C f g
using assms has_as_coequalizer_def parallel_pair_diagram_axioms_def
by (metis category_axioms parallel_pair_diagram_def)
have "D.has_as_coequalizer e"
using assms has_as_coequalizer_def by blast
interpret coequalizer_cocone C f g e
by (simp add: ‹D.has_as_coequalizer e› category_axioms coequalizer_cocone_def
D.parallel_pair_diagram_axioms)
show T
by (metis (lifting) HOL.ext assms(2) cod_comp coequalizes in_homI is_couniversal' seqE)
qed
end
end