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
definition has_colimits_of_shape
where "has_colimits_of_shape J ≡ ∀D. diagram J C D ⟶ (∃a χ. colimit_cocone J C D a χ)"
definition has_colimits
where "has_colimits (_ :: 'j) ≡ ∀J :: 'j comp. category J ⟶ has_colimits_of_shape J"
lemma has_coproducts_if_has_colimits:
assumes "has_colimits (undefined :: 'j)" and "I ≠ (UNIV :: 'j set)"
shows "has_coproducts I"
proof (unfold has_coproducts_def, intro conjI allI impI)
show "I ≠ UNIV" by fact
fix J D
assume D: "discrete_diagram J C D ∧ Collect (partial_composition.arr J) = I"
interpret D: discrete_diagram J C D
using D by simp
have 1: "∃a. D.has_as_colimit a"
using assms D D.diagram_axioms D.J.category_axioms
by (simp add: has_colimits_of_shape_def has_colimits_def)
show "∃a. has_as_coproduct J D a"
using 1 has_as_coproduct_def D.coproduct_coconeI by blast
qed
lemma has_finite_coproducts_if_has_finite_colimits:
assumes "⋀J :: 'j comp. (finite (Collect (partial_composition.arr J)))
⟹ has_colimits_of_shape J"
and "finite (I :: 'j set)" and "I ≠ UNIV"
shows "has_coproducts I"
proof (unfold has_coproducts_def, intro conjI allI impI)
show "I ≠ UNIV" by fact
fix J D
assume D: "discrete_diagram J C D ∧ Collect (partial_composition.arr J) = I"
interpret D: discrete_diagram J C D
using D by simp
have 1: "∃a. D.has_as_colimit a"
using assms D has_colimits_of_shape_def D.diagram_axioms by auto
show "∃a. has_as_coproduct J D a"
using 1 has_as_coproduct_def D.coproduct_coconeI by blast
qed
lemma has_coproducts_preserved_by_bijection:
assumes "has_coproducts I" and "bij_betw φ I I'" and "I' ≠ UNIV"
shows "has_coproducts I'"
proof (unfold has_coproducts_def, intro conjI allI impI)
show "I' ≠ UNIV" by fact
show "⋀J' D'. discrete_diagram J' C D' ∧ Collect (partial_composition.arr J') = I'
⟹ ∃a. has_as_coproduct J' D' a"
proof -
fix J' D'
assume 1: "discrete_diagram J' C D' ∧ Collect (partial_composition.arr J') = I'"
interpret J': category J'
using 1 by (simp add: discrete_diagram_def)
interpret D': discrete_diagram J' C D'
using 1 by simp
interpret J: discrete_category I ‹SOME x. x ∉ I›
using assms has_coproducts_def [of I] someI_ex [of "λx. x ∉ I"]
by unfold_locales auto
have 2: "Collect J.arr = I ∧ Collect J'.arr = I'"
using 1 by auto
have φ: "bij_betw φ (Collect J.arr) (Collect J'.arr)"
using 2 assms(2) by simp
let ?φ = "λj. if J.arr j then φ j else J'.null"
let ?φ' = "λj'. if J'.arr j' then the_inv_into I φ j' else J.null"
interpret φ: "functor" J.comp J' ?φ
proof -
have "φ ` I = I'"
using φ 2 bij_betw_def [of φ I I'] by simp
hence "⋀j. J.arr j ⟹ J'.arr (?φ j)"
using 1 D'.is_discrete by auto
thus "functor J.comp J' ?φ"
using D'.is_discrete J.is_discrete J.seqE
by unfold_locales auto
qed
interpret φ': "functor" J' J.comp ?φ'
proof -
have "the_inv_into I φ ` I' = I"
using assms(2) φ bij_betw_the_inv_into bij_betw_imp_surj_on by metis
hence "⋀j'. J'.arr j' ⟹ J.arr (?φ' j')"
using 2 D'.is_discrete J.is_discrete by auto
thus "functor J' J.comp ?φ'"
using D'.is_discrete J.is_discrete J'.seqE
by unfold_locales auto
qed
let ?D = "λi. D' (φ i)"
interpret D: discrete_diagram_from_map I C ?D ‹SOME j. j ∉ I›
using assms 1 D'.is_discrete bij_betw_imp_surj_on φ.preserves_ide
by unfold_locales auto
obtain a where a: "has_as_coproduct J.comp D.map a"
using assms D.discrete_diagram_axioms has_coproducts_def [of I] by auto
obtain ι where ι: "coproduct_cocone J.comp C D.map a ι"
using a has_as_coproduct_def by blast
interpret ι: coproduct_cocone J.comp C D.map a ι
using ι by simp
let ?ι' = "ι o ?φ'"
interpret A: constant_functor J' C a
using ι.ide_apex by unfold_locales simp
interpret ι': natural_transformation J' C D' A.map ?ι'
proof -
have "ι.A.map ∘ ?φ' = A.map"
using φ A.map_def φ'.preserves_arr ι.A.extensionality J.not_arr_null by auto
moreover have "D.map ∘ ?φ' = D'"
proof
fix j'
have "J'.arr j' ⟹ (D.map ∘ ?φ') j' = D' j'"
proof -
assume 2: "J'.arr j'"
have 3: "inj_on φ I"
using assms(2) bij_betw_imp_inj_on by auto
have "φ ` I = I'"
by (metis (no_types) assms(2) bij_betw_imp_surj_on)
hence "φ ` I = Collect J'.arr"
using 1 by force
thus ?thesis
using 2 3 D.map_def φ'.preserves_arr f_the_inv_into_f by fastforce
qed
moreover have "¬ J'.arr j' ⟹ (D.map ∘ ?φ') j' = D' j'"
using D.extensionality D'.extensionality
by (simp add: J.Null_not_in_Obj J.null_char)
ultimately show "(D.map ∘ ?φ') j' = D' j'" by blast
qed
ultimately show "natural_transformation J' C D' A.map ?ι'"
using ι.natural_transformation_axioms φ'.as_nat_trans.natural_transformation_axioms
horizontal_composite [of J' J.comp ?φ' ?φ' ?φ' C _ _ ι]
by force
qed
interpret ι': cocone J' C D' a ?ι' ..
interpret ι': coproduct_cocone J' C D' a ?ι'
proof
fix a' χ'
assume χ': "D'.cocone a' χ'"
interpret χ': cocone J' C D' a' χ'
using χ' by simp
show "∃!f. «f : a → a'» ∧ D'.cocones_map f (ι ∘ ?φ') = χ'"
proof -
let ?χ = "χ' o ?φ"
interpret A': constant_functor J.comp C a'
using χ'.ide_apex by unfold_locales simp
interpret χ: natural_transformation J.comp C D.map A'.map ?χ
proof -
have "χ'.A.map ∘ ?φ = A'.map"
using φ φ.preserves_arr A'.map_def χ'.A.extensionality by auto
moreover have "D' ∘ ?φ = D.map"
using φ D.map_def D'.extensionality by auto
ultimately show "natural_transformation J.comp C D.map A'.map ?χ"
using χ'.natural_transformation_axioms
φ.as_nat_trans.natural_transformation_axioms
horizontal_composite [of J.comp J' ?φ ?φ ?φ C _ _ χ']
by force
qed
interpret χ: cocone J.comp C D.map a' ?χ ..
have *: "∃!f. «f : a → a'» ∧ D.cocones_map f ι = ?χ"
using ι.is_couniversal χ.cocone_axioms by simp
show "∃!f. «f : a → a'» ∧ D'.cocones_map f ?ι' = χ'"
proof -
have "∃f. «f : a → a'» ∧ D'.cocones_map f ?ι' = χ'"
proof -
obtain f where f: "«f : a → a'» ∧ D.cocones_map f ι = ?χ"
using * by blast
have "D'.cocones_map f ?ι' = χ'"
proof
fix j'
show "D'.cocones_map f ?ι' j' = χ' j'"
proof (cases "J'.arr j'")
assume j': "¬ J'.arr j'"
show "D'.cocones_map f ?ι' j' = χ' j'"
using f j' χ'.extensionality ι'.cocone_axioms by auto
next
assume j': "J'.arr j'"
show "D'.cocones_map f ?ι' j' = χ' j'"
proof -
have "D'.cocones_map f ?ι' j' = f ⋅ ι (the_inv_into I φ j')"
using f j' ι'.cocone_axioms by auto
also have "... = D.cocones_map f ι (the_inv_into I φ j')"
proof -
have "arr f ∧ dom f = a ∧ cod f = a'"
using f by blast
thus ?thesis
using φ'.preserves_arr ι.is_cocone j' by auto
qed
also have "... = (χ' ∘ ?φ) (the_inv_into I φ j')"
using f by simp
also have "... = χ' j'"
using assms(2) j' 2 bij_betw_def [of φ I I'] bij_betw_imp_inj_on
φ'.preserves_arr f_the_inv_into_f
by fastforce
finally show ?thesis by simp
qed
qed
qed
thus ?thesis using f by blast
qed
moreover have "⋀f f'. ⟦ «f : a → a'»; D'.cocones_map f ?ι' = χ';
«f' : a → a'»; D'.cocones_map f' ?ι' = χ' ⟧
⟹ f = f'"
proof -
fix f f'
assume f: "«f : a → a'»" and f': "«f' : a → a'»"
and fχ': "D'.cocones_map f ?ι' = χ'" and f'χ': "D'.cocones_map f' ?ι' = χ'"
have "D.cocones_map f ι = χ' ∘ ?φ ∧ D.cocones_map f' ι = χ' o ?φ"
proof (intro conjI)
show "D.cocones_map f ι = χ' ∘ ?φ"
proof
fix j
have "¬ J.arr j ⟹ D.cocones_map f ι j = (χ' ∘ ?φ) j"
using f fχ' ι.cocone_axioms χ.extensionality by auto
moreover have "J.arr j ⟹ D.cocones_map f ι j = (χ' ∘ ?φ) j"
proof -
assume j: "J.arr j"
have 1: "j = the_inv_into I φ (φ j)"
using assms(2) j φ the_inv_into_f_f bij_betw_imp_inj_on J.arr_char
by metis
have "D.cocones_map f ι j = D.cocones_map f ι (the_inv_into I φ (φ j))"
using 1 by simp
also have "... = (χ' ∘ ?φ) j"
using f j fχ' 1 ι.cocone_axioms ι'.cocone_axioms φ.preserves_arr by auto
finally show "D.cocones_map f ι j = (χ' ∘ ?φ) j" by blast
qed
ultimately show "D.cocones_map f ι j = (χ' ∘ ?φ) j" by blast
qed
show "D.cocones_map f' ι = χ' ∘ ?φ"
proof
fix j
have "¬ J.arr j ⟹ D.cocones_map f' ι j = (χ' ∘ ?φ) j"
using f' fχ' ι.cocone_axioms χ.extensionality by auto
moreover have "J.arr j ⟹ D.cocones_map f' ι j = (χ' ∘ ?φ) j"
proof -
assume j: "J.arr j"
have 1: "j = the_inv_into I φ (φ j)"
using assms(2) j φ the_inv_into_f_f bij_betw_imp_inj_on J.arr_char
by metis
have "D.cocones_map f' ι j = D.cocones_map f' ι (the_inv_into I φ (φ j))"
using 1 by simp
also have "... = (χ' ∘ ?φ) j"
using f' j f'χ' 1 ι.cocone_axioms ι'.cocone_axioms φ.preserves_arr by auto
finally show "D.cocones_map f' ι j = (χ' ∘ ?φ) j" by blast
qed
ultimately show "D.cocones_map f' ι j = (χ' ∘ ?φ) j" by blast
qed
qed
thus "f = f'"
using f f' * by auto
qed
ultimately show ?thesis by blast
qed
qed
qed
have "has_as_coproduct J' D' a"
using has_as_coproduct_def ι'.coproduct_cocone_axioms by auto
thus "∃a. has_as_coproduct J' D' a" by blast
qed
qed
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
lemma coequalizer_is_epi:
assumes "has_as_coequalizer f g e"
shows "epi e"
proof
show "arr e"
using assms by blast
show "⋀h h'. ⟦seq h e; h ⋅ e = h' ⋅ e⟧ ⟹ h = h'"
using assms has_as_coequalizerE [of f g e]
by (metis comp_assoc match_4)
qed
end
end