Theory Prebicategory
text ‹
The objective of this section is to construct a formalization of bicategories that is
compatible with our previous formulation of categories \<^cite>‹"Category3-AFP"›
and that permits us to carry over unchanged as much of the work done on categories as possible.
For these reasons, we conceive of a bicategory in what might be regarded as a somewhat
unusual fashion. Rather than a traditional development, which would typically define
a bicategory to be essentially ``a `category' whose homs themselves have the structure
of categories,'' here we regard a bicategory as ``a (vertical) category that has been
equipped with a suitable (horizontal) weak composition.'' Stated another way, we think
of a bicategory as a generalization of a monoidal category in which the tensor product is
a partial operation, rather than a total one. Our definition of bicategory can thus
be summarized as follows: a bicategory is a (vertical) category that has been equipped
with idempotent endofunctors ‹src› and ‹trg› that assign to each arrow its ``source''
and ``target'' subject to certain commutativity constraints,
a partial binary operation ‹⋆› of horizontal composition that is suitably functorial on
the ``hom-categories'' determined by the assignment of sources and targets,
``associativity'' isomorphisms ‹«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ (g ⋆ h)»› for each horizontally
composable triple of vertical identities ‹f›, ‹g›, ‹h›, subject to the usual naturality
and coherence conditions, and for each ``object'' ‹a› (defined to be an arrow that is
its own source and target) a ``unit isomorphism'' ‹«𝗂[a] : a ⋆ a ⇒ a»›.
As is the case for monoidal categories, the unit isomorphisms and associator isomorphisms
together enable a canonical definition of left and right ``unit'' isomorphisms
‹«𝗅[f] : a ⋆ f ⇒ f»› and ‹«𝗋[f] : f ⋆ a ⇒ f»› when ‹f› is a vertical identity
horizontally composable on the left or right by ‹a›, and it can be shown that these are
the components of natural transformations.
The definition of bicategory just sketched shares with a more traditional version the
requirement that assignments of source and target are given as basic data, and these
assignments determine horizontal composability in the sense that arrows ‹μ› and ‹ν›
are composable if the chosen source of ‹μ› coincides with the chosen target of ‹ν›.
Thus it appears, at least on its face, that composability of arrows depends on an assignment
of sources and targets. We are interested in establishing whether this is essential or
whether bicategories can be formalized in a completely ``object-free'' fashion.
It turns out that we can obtain such an object-free formalization through a rather direct
generalization of the approach we used in the formalization of categories.
Specifically, we define a \emph{weak composition} to be a partial binary operation ‹⋆›
on the arrow type of a ``vertical'' category ‹V›, such that the domain of definition of this
operation is itself a category (of ``horizontally composable pairs of arrows''),
the operation is functorial, and it is subject to certain matching conditions which include
those satisfied by a category.
From the axioms for a weak composition we can prove the existence of ``hom-categories'',
which are subcategories of ‹V› consisting of arrows horizontally composable on the
left or right by a specified vertical identity.
A \emph{weak unit} is defined to be a vertical identity ‹a› such that ‹a ⋆ a ≅ a›
and is such that the mappings ‹a ⋆ ‐› and ‹‐ ⋆ a› are fully faithful endofunctors
of the subcategories of ‹V› consisting of the arrows for which they are defined.
We define the \emph{sources} of an arrow ‹μ› to be the weak units that are horizontally
composable with ‹μ› on the right, and the \emph{targets} of ‹μ› to be the weak units
that are horizontally composable with ‹μ› on the left.
An \emph{associative weak composition} is defined to be a weak composition that is equipped
with ``associator'' isomorphisms ‹«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ (g ⋆ h)»› for horizontally
composable vertical identities ‹f›, ‹g›, ‹h›, subject to the usual naturality and coherence
conditions.
A \emph{prebicategory} is defined to be an associative weak composition for which every
arrow has a source and a target. We show that the sets of sources and targets of each
arrow in a prebicategory is an isomorphism class of weak units, and that horizontal
composability of arrows ‹μ› and ‹ν› is characterized by the set of sources of ‹μ› being
equal to the set of targets of ‹ν›.
We show that prebicategories are essentially ``bicategories without objects''.
Given a prebicategory, we may choose an arbitrary representative of each
isomorphism class of weak units and declare these to be ``objects''
(this is analogous to choosing a particular unit object in a monoidal category).
For each object we may choose a particular \emph{unit isomorphism} ‹«𝗂[a] : a ⋆ a ⇒ a»›.
This choice, together with the associator isomorphisms, enables a canonical definition
of left and right unit isomorphisms ‹«𝗅[f] : a ⋆ f ⇒ f»› and ‹«𝗋[f] : f ⋆ a ⇒ f»›
when ‹f› is a vertical identity horizontally composable on the left or right by ‹a›,
and it can be shown that these are the components of natural isomorphisms.
We may then define ``the source'' of an arrow to be the chosen representative of the
set of its sources and ``the target'' to be the chosen representative of the set of its
targets. We show that the resulting structure is a bicategory, in which horizontal
composability as given by the weak composition coincides with the ``syntactic'' version
determined by the chosen sources and targets.
Conversely, a bicategory determines a prebicategory, essentially by forgetting
the sources, targets and unit isomorphisms.
These results make it clear that the assignment of sources and targets to arrows in
a bicategory is basically a convenience and that horizontal composability of arrows
is not dependent on a particular choice.
›
theory Prebicategory
imports Category3.EquivalenceOfCategories Category3.Subcategory IsomorphismClass
begin
section "Weak Composition"
text ‹
In this section we define a locale ‹weak_composition›, which formalizes a functorial
operation of ``horizontal'' composition defined on an underlying ``vertical'' category.
The definition is expressed without the presumption of the existence of any sort
of ``objects'' that determine horizontal composability. Rather, just as we did
in showing that the @{locale partial_magma} locale supported the definition of ``identity
arrow'' as a kind of unit for vertical composition which ultimately served as a basis
for the definition of ``domain'' and ``codomain'' of an arrow, here we show that the
‹weak_composition› locale supports a definition of \emph{weak unit} for horizontal
composition which can ultimately be used to define the \emph{sources} and \emph{targets}
of an arrow with respect to horizontal composition.
In particular, the definition of weak composition involves axioms that relate horizontal
and vertical composability. As a consequence of these axioms, for any fixed arrow ‹μ›,
the sets of arrows horizontally composable on the left and on the right with ‹μ›
form subcategories with respect to vertical composition. We define the
sources of ‹μ› to be the weak units that are composable with ‹μ› on the right,
and the targets of ‹μ› to be the weak units that are composable with ‹μ›
on the left. Weak units are then characterized as arrows that are members
of the set of their own sources (or, equivalently, of their own targets).
›
subsection "Definition"
locale weak_composition =
category V +
VxV: product_category V V +
VoV: subcategory VxV.comp ‹λμν. fst μν ⋆ snd μν ≠ null› +
"functor" VoV.comp V ‹λμν. fst μν ⋆ snd μν›
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a comp" (infixr "⋆" 53) +
assumes left_connected: "seq ν ν' ⟹ ν ⋆ μ ≠ null ⟷ ν' ⋆ μ ≠ null"
and right_connected: "seq μ μ' ⟹ ν ⋆ μ ≠ null ⟷ ν ⋆ μ' ≠ null"
and match_1: "⟦ ν ⋆ μ ≠ null; (ν ⋆ μ) ⋆ τ ≠ null ⟧ ⟹ μ ⋆ τ ≠ null"
and match_2: "⟦ ν ⋆ (μ ⋆ τ) ≠ null; μ ⋆ τ ≠ null ⟧ ⟹ ν ⋆ μ ≠ null"
and match_3: "⟦ μ ⋆ τ ≠ null; ν ⋆ μ ≠ null ⟧ ⟹ (ν ⋆ μ) ⋆ τ ≠ null"
and match_4: "⟦ μ ⋆ τ ≠ null; ν ⋆ μ ≠ null ⟧ ⟹ ν ⋆ (μ ⋆ τ) ≠ null"
begin
text ‹
We think of the arrows of the vertical category as ``2-cells'' and the vertical identities
as ``1-cells''. In the formal development, the predicate @{term arr} (``arrow'')
will have its normal meaning with respect to the vertical composition, hence @{term "arr μ"}
will mean, essentially, ``‹μ› is a 2-cell''. This is somewhat unfortunate, as it is
traditional when discussing bicategories to use the term ``arrow'' to refer to the 1-cells.
However, we are trying to carry over all the formalism that we have already developed for
categories and apply it to bicategories with as little change and redundancy as possible.
It becomes too confusing to try to repurpose the name @{term arr} to mean @{term ide} and
to introduce a replacement for the name @{term arr}, so we will simply tolerate the
situation. In informal text, we will prefer the terms ``2-cell'' and ``1-cell'' over
(vertical) ``arrow'' and ``identity'' when there is a chance for confusion.
We do, however, make the following adjustments in notation for @{term in_hom} so that
it is distinguished from the notion @{term in_hhom} (``in horizontal hom'') to be
introduced subsequently.
›
no_notation in_hom ("«_ : _ → _»")
notation in_hom ("«_ : _ ⇒ _»")
lemma is_partial_magma:
shows "partial_magma H"
proof
show "∃!n. ∀f. n ⋆ f = n ∧ f ⋆ n = n"
proof
show 1: "∀f. null ⋆ f = null ∧ f ⋆ null = null"
using is_extensional VoV.inclusion VoV.arr_char⇩S⇩b⇩C by force
show "⋀n. ∀f. n ⋆ f = n ∧ f ⋆ n = n ⟹ n = null"
using 1 VoV.arr_char⇩S⇩b⇩C is_extensional not_arr_null by metis
qed
qed
interpretation H: partial_magma H
using is_partial_magma by auto
interpretation H: partial_composition H
..
lemma is_partial_composition:
shows "partial_composition H"
..
text ‹
Either ‹match_1› or ‹match_2› seems essential for the next result, which states
that the nulls for the horizontal and vertical compositions coincide.
›
lemma null_agreement [simp]:
shows "H.null = null"
by (metis VoV.inclusion VxV.not_arr_null match_1 H.null_is_zero(1))
lemma composable_implies_arr:
assumes "ν ⋆ μ ≠ null"
shows "arr μ" and "arr ν"
using assms is_extensional VoV.arr_char⇩S⇩b⇩C VoV.inclusion by auto
lemma hcomp_null [simp]:
shows "null ⋆ μ = null" and "μ ⋆ null = null"
using H.null_is_zero by auto
lemma hcomp_simps⇩W⇩C [simp]:
assumes "ν ⋆ μ ≠ null"
shows "arr (ν ⋆ μ)" and "dom (ν ⋆ μ) = dom ν ⋆ dom μ" and "cod (ν ⋆ μ) = cod ν ⋆ cod μ"
using assms preserves_arr preserves_dom preserves_cod VoV.arr_char⇩S⇩b⇩C VoV.inclusion
VoV.dom_simp VoV.cod_simp
by force+
lemma ide_hcomp⇩W⇩C:
assumes "ide f" and "ide g" and "g ⋆ f ≠ null"
shows "ide (g ⋆ f)"
using assms preserves_ide VoV.ide_char⇩S⇩b⇩C by force
lemma hcomp_in_hom⇩W⇩C [intro]:
assumes "ν ⋆ μ ≠ null"
shows "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
using assms by auto
text ‹
Horizontal composability of arrows is determined by horizontal composability of
their domains and codomains (defined with respect to vertical composition).
›
lemma hom_connected:
shows "ν ⋆ μ ≠ null ⟷ dom ν ⋆ μ ≠ null"
and "ν ⋆ μ ≠ null ⟷ ν ⋆ dom μ ≠ null"
and "ν ⋆ μ ≠ null ⟷ cod ν ⋆ μ ≠ null"
and "ν ⋆ μ ≠ null ⟷ ν ⋆ cod μ ≠ null"
proof -
show "ν ⋆ μ ≠ null ⟷ dom ν ⋆ μ ≠ null"
using left_connected [of ν "dom ν" μ] composable_implies_arr arr_dom_iff_arr by force
show "ν ⋆ μ ≠ null ⟷ cod ν ⋆ μ ≠ null"
using left_connected [of "cod ν" ν μ] composable_implies_arr arr_cod_iff_arr by force
show "ν ⋆ μ ≠ null ⟷ ν ⋆ dom μ ≠ null"
using right_connected [of μ "dom μ" ν] composable_implies_arr arr_dom_iff_arr by force
show "ν ⋆ μ ≠ null ⟷ ν ⋆ cod μ ≠ null"
using right_connected [of "cod μ" μ ν] composable_implies_arr arr_cod_iff_arr by force
qed
lemma isomorphic_implies_equicomposable:
assumes "f ≅ g"
shows "τ ⋆ f ≠ null ⟷ τ ⋆ g ≠ null"
and "f ⋆ σ ≠ null ⟷ g ⋆ σ ≠ null"
using assms isomorphic_def hom_connected by auto
lemma interchange:
assumes "seq ν μ" and "seq τ σ"
shows "(ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
proof -
have "μ ⋆ σ = null ⟹ ?thesis"
by (metis assms null_is_zero(2) dom_comp hom_connected(1-2))
moreover have "μ ⋆ σ ≠ null ⟹ ?thesis"
proof -
assume μσ: "μ ⋆ σ ≠ null"
have 1: "VoV.arr (μ, σ)"
using μσ VoV.arr_char⇩S⇩b⇩C by auto
have ντ: "(ν, τ) ∈ VoV.hom (VoV.cod (μ, σ)) (VoV.cod (ν, τ))"
proof -
have "VoV.arr (ν, τ)"
using assms 1 hom_connected VoV.arr_char⇩S⇩b⇩C
by (elim seqE, auto, metis)
thus ?thesis
using assms μσ VoV.dom_char⇩S⇩b⇩C VoV.cod_char⇩S⇩b⇩C by fastforce
qed
show ?thesis
proof -
have "VoV.seq (ν, τ) (μ, σ)"
using assms 1 μσ ντ VoV.seqI by blast
thus ?thesis
using assms 1 μσ ντ VoV.comp_char preserves_comp [of "(ν, τ)" "(μ, σ)"] VoV.seqI
by fastforce
qed
qed
ultimately show ?thesis by blast
qed
lemma paste_1:
shows "ν ⋆ μ = (cod ν ⋆ μ) ⋅ (ν ⋆ dom μ)"
using interchange composable_implies_arr comp_arr_dom comp_cod_arr
hom_connected(2-3)
by (metis null_is_zero(2))
lemma paste_2:
shows "ν ⋆ μ = (ν ⋆ cod μ) ⋅ (dom ν ⋆ μ)"
using interchange composable_implies_arr comp_arr_dom comp_cod_arr
hom_connected(1,4)
by (metis null_is_zero(2))
lemma whisker_left:
assumes "seq ν μ" and "ide f"
shows "f ⋆ (ν ⋅ μ) = (f ⋆ ν) ⋅ (f ⋆ μ)"
using assms interchange [of f f ν μ] hom_connected by auto
lemma whisker_right:
assumes "seq ν μ" and "ide f"
shows "(ν ⋅ μ) ⋆ f = (ν ⋆ f) ⋅ (μ ⋆ f)"
using assms interchange [of ν μ f f] hom_connected by auto
subsection "Hom-Subcategories"
definition left
where "left τ ≡ λμ. τ ⋆ μ ≠ null"
definition right
where "right σ ≡ λμ. μ ⋆ σ ≠ null"
lemma right_iff_left:
shows "right σ τ ⟷ left τ σ"
using right_def left_def by simp
lemma left_respects_isomorphic:
assumes "f ≅ g"
shows "left f = left g"
using assms isomorphic_implies_equicomposable left_def by auto
lemma right_respects_isomorphic:
assumes "f ≅ g"
shows "right f = right g"
using assms isomorphic_implies_equicomposable right_def by auto
lemma left_iff_left_inv:
assumes "iso μ"
shows "left τ μ ⟷ left τ (inv μ)"
using assms left_def inv_in_hom hom_connected(2) hom_connected(4) [of τ "inv μ"]
by auto
lemma right_iff_right_inv:
assumes "iso μ"
shows "right σ μ ⟷ right σ (inv μ)"
using assms right_def inv_in_hom hom_connected(1) hom_connected(3) [of "inv μ" σ]
by auto
lemma left_hom_is_subcategory:
assumes "arr μ"
shows "subcategory V (left μ)"
using composable_implies_arr hom_connected(2,4)
apply (unfold left_def, unfold_locales)
apply auto
by (metis cod_comp seqI)
lemma right_hom_is_subcategory:
assumes "arr μ"
shows "subcategory V (right μ)"
using composable_implies_arr hom_connected(1,3)
apply (unfold right_def, unfold_locales)
apply auto
by (metis cod_comp seqI)
abbreviation Left
where "Left a ≡ subcategory.comp V (left a)"
abbreviation Right
where "Right a ≡ subcategory.comp V (right a)"
text ‹
We define operations of composition on the left or right with a fixed 1-cell,
and show that such operations are functorial in case that 1-cell is
horizontally self-composable.
›
definition H⇩L
where "H⇩L g ≡ λμ. g ⋆ μ"
definition H⇩R
where "H⇩R f ≡ λμ. μ ⋆ f"
text ‹
Note that ‹match_3› and ‹match_4› are required for the next results.
›
lemma endofunctor_H⇩L:
assumes "ide g" and "g ⋆ g ≠ null"
shows "endofunctor (Left g) (H⇩L g)"
proof -
interpret L: subcategory V ‹left g› using assms left_hom_is_subcategory by simp
have *: "⋀μ. L.arr μ ⟹ H⇩L g μ = g ⋆ μ"
using assms H⇩L_def by simp
have preserves_arr: "⋀μ. L.arr μ ⟹ L.arr (H⇩L g μ)"
using assms * L.arr_char⇩S⇩b⇩C left_def match_4 by force
show "endofunctor L.comp (H⇩L g)"
using assms *
apply unfold_locales
using H⇩L_def L.arr_char⇩S⇩b⇩C L.null_char left_def
apply force
using preserves_arr
apply blast
apply (metis L.dom_simp L.not_arr_null L.null_char hcomp_simps⇩W⇩C(2) ide_char
preserves_arr H⇩L_def)
apply (metis H⇩L_def L.arrE L.cod_simp hcomp_simps⇩W⇩C(3) ide_char left_def preserves_arr)
by (metis L.comp_def L.comp_simp L.seq_char⇩S⇩b⇩C hcomp_simps⇩W⇩C(1) whisker_left preserves_arr)
qed
lemma endofunctor_H⇩R:
assumes "ide f" and "f ⋆ f ≠ null"
shows "endofunctor (Right f) (H⇩R f)"
proof -
interpret R: subcategory V ‹right f› using assms right_hom_is_subcategory by simp
have *: "⋀μ. R.arr μ ⟹ H⇩R f μ = μ ⋆ f"
using assms H⇩R_def by simp
have preserves_arr: "⋀μ. R.arr μ ⟹ R.arr (H⇩R f μ)"
using assms * R.arr_char⇩S⇩b⇩C right_def match_3 by force
show "endofunctor R.comp (H⇩R f)"
using assms *
apply unfold_locales
using H⇩R_def R.arr_char⇩S⇩b⇩C R.null_char right_def
apply force
using preserves_arr
apply blast
apply (metis R.dom_simp R.not_arr_null R.null_char hcomp_simps⇩W⇩C(2) ide_char
preserves_arr H⇩R_def)
apply (metis H⇩R_def R.arrE R.cod_simp hcomp_simps⇩W⇩C(3) ide_char right_def preserves_arr)
by (metis R.comp_def R.comp_simp R.seq_char⇩S⇩b⇩C hcomp_simps⇩W⇩C(1) whisker_right preserves_arr)
qed
end
locale left_hom =
weak_composition V H +
S: subcategory V ‹left ω›
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a comp" (infixr "⋆" 53)
and ω :: 'a +
assumes arr_ω: "arr ω"
begin
no_notation in_hom ("«_ : _ → _»")
notation in_hom ("«_ : _ ⇒ _»")
notation S.comp (infixr "⋅⇩S" 55)
notation S.in_hom ("«_ : _ ⇒⇩S _»")
lemma right_hcomp_closed:
assumes "«μ : x ⇒⇩S y»" and "«ν : c ⇒ d»" and "μ ⋆ ν ≠ null"
shows "«μ ⋆ ν : x ⋆ c ⇒⇩S y ⋆ d»"
using assms arr_ω S.arr_char⇩S⇩b⇩C S.dom_simp S.cod_simp left_def match_4
by (elim S.in_homE, intro S.in_homI) auto
lemma interchange:
assumes "S.seq ν μ" and "S.seq τ σ" and "μ ⋆ σ ≠ null"
shows "(ν ⋅⇩S μ) ⋆ (τ ⋅⇩S σ) = (ν ⋆ τ) ⋅⇩S (μ ⋆ σ)"
proof -
have 1: "ν ⋆ τ ≠ null"
using assms hom_connected(1) [of ν σ] hom_connected(2) [of ν τ] hom_connected(3-4)
S.dom_simp S.cod_simp
by force
have "(ν ⋅⇩S μ) ⋆ (τ ⋅⇩S σ) = (ν ⋅ μ) ⋆ (τ ⋅ σ)"
using assms S.comp_char S.seq_char⇩S⇩b⇩C by metis
also have "... = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
using assms interchange S.seq_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C by simp
also have "... = (ν ⋆ τ) ⋅⇩S (μ ⋆ σ)"
using assms 1
by (metis S.arr_char⇩S⇩b⇩C S.comp_char S.seq_char⇩S⇩b⇩C ext match_4 left_def)
finally show ?thesis by blast
qed
lemma inv_char:
assumes "S.arr φ" and "iso φ"
shows "S.inverse_arrows φ (inv φ)"
and "S.inv φ = inv φ"
proof -
have 1: "S.arr (inv φ)"
using assms S.arr_char⇩S⇩b⇩C left_iff_left_inv
by (intro S.arrI⇩S⇩b⇩C) meson
show "S.inv φ = inv φ"
using assms 1 S.inv_char⇩S⇩b⇩C S.iso_char⇩S⇩b⇩C by blast
thus "S.inverse_arrows φ (inv φ)"
using assms 1 S.iso_char⇩S⇩b⇩C S.inv_is_inverse by metis
qed
lemma iso_char:
assumes "S.arr φ"
shows "S.iso φ ⟷ iso φ"
using assms S.iso_char⇩S⇩b⇩C inv_char by auto
end
locale right_hom =
weak_composition V H +
S: subcategory V ‹right ω›
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a comp" (infixr "⋆" 53)
and ω :: 'a +
assumes arr_ω: "arr ω"
begin
no_notation in_hom ("«_ : _ → _»")
notation in_hom ("«_ : _ ⇒ _»")
notation S.comp (infixr "⋅⇩S" 55)
notation S.in_hom ("«_ : _ ⇒⇩S _»")
lemma left_hcomp_closed:
assumes "«μ : x ⇒⇩S y»" and "«ν : c ⇒ d»" and "ν ⋆ μ ≠ null"
shows "«ν ⋆ μ : c ⋆ x ⇒⇩S d ⋆ y»"
using assms arr_ω S.arr_char⇩S⇩b⇩C S.dom_simp S.cod_simp right_def match_3
by (elim S.in_homE, intro S.in_homI) auto
lemma interchange:
assumes "S.seq ν μ" and "S.seq τ σ" and "μ ⋆ σ ≠ null"
shows "(ν ⋅⇩S μ) ⋆ (τ ⋅⇩S σ) = (ν ⋆ τ) ⋅⇩S (μ ⋆ σ)"
proof -
have 1: "ν ⋆ τ ≠ null"
using assms hom_connected(1) [of ν σ] hom_connected(2) [of ν τ] hom_connected(3-4)
S.dom_simp S.cod_simp
by fastforce
have "(ν ⋅⇩S μ) ⋆ (τ ⋅⇩S σ) = (ν ⋅ μ) ⋆ (τ ⋅ σ)"
using assms S.comp_char S.seq_char⇩S⇩b⇩C by metis
also have "... = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
using assms interchange S.seq_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C by simp
also have "... = (ν ⋆ τ) ⋅⇩S (μ ⋆ σ)"
using assms 1
by (metis S.arr_char⇩S⇩b⇩C S.comp_char S.seq_char⇩S⇩b⇩C ext match_3 right_def)
finally show ?thesis by blast
qed
lemma inv_char:
assumes "S.arr φ" and "iso φ"
shows "S.inverse_arrows φ (inv φ)"
and "S.inv φ = inv φ"
proof -
have 1: "S.arr (inv φ)"
using assms S.arr_char⇩S⇩b⇩C right_iff_right_inv
by (intro S.arrI⇩S⇩b⇩C) meson
show "S.inv φ = inv φ"
using assms 1 S.inv_char⇩S⇩b⇩C S.iso_char⇩S⇩b⇩C by blast
thus "S.inverse_arrows φ (inv φ)"
using assms 1 S.iso_char⇩S⇩b⇩C S.inv_is_inverse by metis
qed
lemma iso_char:
assumes "S.arr φ"
shows "S.iso φ ⟷ iso φ"
using assms S.iso_char⇩S⇩b⇩C inv_char by auto
end
subsection "Weak Units"
text ‹
We now define a \emph{weak unit} to be an arrow ‹a› such that:
\begin{enumerate}
\item ‹a ⋆ a› is isomorphic to ‹a›
(and hence ‹a› is a horizontally self-composable 1-cell).
\item Horizontal composition on the left with ‹a› is a fully faithful endofunctor of the
subcategory of arrows that are composable on the left with ‹a›.
\item Horizontal composition on the right with ‹a› is fully faithful endofunctor of the
subcategory of arrows that are composable on the right with ‹a›.
\end{enumerate}
›
context weak_composition
begin
definition weak_unit :: "'a ⇒ bool"
where "weak_unit a ≡ a ⋆ a ≅ a ∧
fully_faithful_functor (Left a) (Left a) (H⇩L a) ∧
fully_faithful_functor (Right a) (Right a) (H⇩R a)"
lemma weak_unit_self_composable:
assumes "weak_unit a"
shows "ide a" and "ide (a ⋆ a)" and "a ⋆ a ≠ null"
proof -
obtain φ where φ: "«φ : a ⋆ a ⇒ a» ∧ iso φ"
using assms weak_unit_def isomorphic_def by blast
have 1: "arr φ" using φ by blast
show "ide a" using φ ide_cod by blast
thus "ide (a ⋆ a)" using φ ide_dom by force
thus "a ⋆ a ≠ null" using not_arr_null ideD(1) by metis
qed
lemma weak_unit_self_right:
assumes "weak_unit a"
shows "right a a"
using assms weak_unit_self_composable right_def by simp
lemma weak_unit_self_left:
assumes "weak_unit a"
shows "left a a"
using assms weak_unit_self_composable left_def by simp
lemma weak_unit_in_vhom:
assumes "weak_unit a"
shows "«a : a ⇒ a»"
using assms weak_unit_self_composable left_def by auto
text ‹
If ‹a› is a weak unit, then there exists a ``unit isomorphism'' ‹«ι : a ⋆ a ⇒ a»›.
It need not be unique, but we may choose one arbitrarily.
›
definition some_unit
where "some_unit a ≡ SOME ι. iso ι ∧ «ι : a ⋆ a ⇒ a»"
lemma iso_some_unit:
assumes "weak_unit a"
shows "iso (some_unit a)"
and "«some_unit a : a ⋆ a ⇒ a»"
proof -
let ?P = "λι. iso ι ∧ «ι : a ⋆ a ⇒ a»"
have "∃ι. ?P ι"
using assms weak_unit_def by auto
hence 1: "?P (some_unit a)"
using someI_ex [of ?P] some_unit_def by simp
show "iso (some_unit a)" using 1 by blast
show "«some_unit a : a ⋆ a ⇒ a»" using 1 by blast
qed
text ‹
The \emph{sources} of an arbitrary arrow ‹μ› are the weak units that are composable with ‹μ›
on the right. Similarly, the \emph{targets} of ‹μ› are the weak units that are composable
with ‹μ› on the left.
›
definition sources
where "sources μ ≡ {a. weak_unit a ∧ μ ⋆ a ≠ null}"
lemma sourcesI [intro]:
assumes "weak_unit a" and "μ ⋆ a ≠ null"
shows "a ∈ sources μ"
using assms sources_def by blast
lemma sourcesD [dest]:
assumes "a ∈ sources μ"
shows "ide a" and "weak_unit a" and "μ ⋆ a ≠ null"
using assms sources_def weak_unit_self_composable by auto
definition targets
where "targets μ ≡ {b. weak_unit b ∧ b ⋆ μ ≠ null}"
lemma targetsI [intro]:
assumes "weak_unit b" and "b ⋆ μ ≠ null"
shows "b ∈ targets μ"
using assms targets_def by blast
lemma targetsD [dest]:
assumes "b ∈ targets μ"
shows "ide b" and "weak_unit b" and "b ⋆ μ ≠ null"
using assms targets_def weak_unit_self_composable by auto
lemma sources_dom [simp]:
assumes "arr μ"
shows "sources (dom μ) = sources μ"
using assms hom_connected(1) by blast
lemma sources_cod [simp]:
assumes "arr μ"
shows "sources (cod μ) = sources μ"
using assms hom_connected(3) by blast
lemma targets_dom [simp]:
assumes "arr μ"
shows "targets (dom μ) = targets μ"
using assms hom_connected(2) by blast
lemma targets_cod [simp]:
assumes "arr μ"
shows "targets (cod μ) = targets μ"
using assms hom_connected(4) by blast
lemma weak_unit_iff_self_source:
shows "weak_unit a ⟷ a ∈ sources a"
using weak_unit_self_composable by auto
lemma weak_unit_iff_self_target:
shows "weak_unit b ⟷ b ∈ targets b"
using weak_unit_self_composable by auto
abbreviation (input) in_hhom⇩W⇩C ("«_ : _ →⇩W⇩C _»")
where "in_hhom⇩W⇩C μ f g ≡ arr μ ∧ f ∈ sources μ ∧ g ∈ targets μ"
lemma sources_hcomp:
assumes "ν ⋆ μ ≠ null"
shows "sources (ν ⋆ μ) = sources μ"
using assms match_1 match_3 null_agreement by blast
lemma targets_hcomp:
assumes "ν ⋆ μ ≠ null"
shows "targets (ν ⋆ μ) = targets ν"
using assms match_2 match_4 null_agreement by blast
lemma H⇩R_preserved_along_iso:
assumes "weak_unit a" and "a ≅ a'"
shows "endofunctor (Right a) (H⇩R a')"
proof -
have a: "ide a ∧ weak_unit a" using assms isomorphic_def by auto
have a': "ide a'" using assms isomorphic_def by auto
interpret R: subcategory V ‹right a› using a right_hom_is_subcategory by simp
have *: "⋀μ. R.arr μ ⟹ H⇩R a' μ = μ ⋆ a'"
using assms H⇩R_def by simp
have preserves_arr: "⋀μ. R.arr μ ⟹ R.arr (H⇩R a' μ)"
using assms a' * R.arr_char⇩S⇩b⇩C right_def weak_unit_def weak_unit_self_composable
isomorphic_implies_equicomposable R.ide_char match_3 hcomp_simps⇩W⇩C(1)
null_agreement
by metis
show "endofunctor R.comp (H⇩R a')"
proof
show "⋀μ. ¬ R.arr μ ⟹ H⇩R a' μ = R.null"
using assms R.arr_char⇩S⇩b⇩C R.null_char right_def H⇩R_def null_agreement
right_respects_isomorphic
by metis
fix μ
assume "R.arr μ"
hence μ: "R.arr μ ∧ arr μ ∧ right a μ ∧ right a' μ ∧ μ ⋆ a ≠ null ∧ μ ⋆ a' ≠ null"
using assms R.arr_char⇩S⇩b⇩C right_respects_isomorphic composable_implies_arr null_agreement
right_def
by metis
show "R.arr (H⇩R a' μ)" using μ preserves_arr by blast
show "R.dom (H⇩R a' μ) = H⇩R a' (R.dom μ)"
using a' μ * R.arr_char⇩S⇩b⇩C R.dom_char⇩S⇩b⇩C preserves_arr hom_connected(1) right_def
by simp
show "R.cod (H⇩R a' μ) = H⇩R a' (R.cod μ)"
using a' μ * R.arr_char⇩S⇩b⇩C R.cod_char⇩S⇩b⇩C preserves_arr hom_connected(3) right_def
by simp
next
fix μ ν
assume μν: "R.seq ν μ"
have μ: "R.arr μ ∧ arr μ ∧ right a μ ∧ right a' μ ∧ μ ⋆ a ≠ null ∧ μ ⋆ a' ≠ null"
using assms μν R.arr_char⇩S⇩b⇩C right_respects_isomorphic composable_implies_arr
null_agreement right_def
by (elim R.seqE) metis
have ν: "«ν : R.cod μ → R.cod ν» ∧ arr ν ∧
right a ν ∧ H ν a ≠ null ∧ right a' ν ∧ H ν a' ≠ null"
by (metis "*" R.cod_simp R.comp_def R.inclusion R.not_arr_null R.null_char R.seqE
μν in_homI preserves_arr right_def)
show "H⇩R a' (R.comp ν μ) = R.comp (H⇩R a' ν) (H⇩R a' μ)"
proof -
have 1: "R.arr (H⇩R a' ν)"
using ν preserves_arr by blast
have 2: "seq (ν ⋆ a') (μ ⋆ a')"
using a' μ ν R.arr_char⇩S⇩b⇩C R.inclusion R.dom_char⇩S⇩b⇩C R.cod_char⇩S⇩b⇩C
isomorphic_implies_equicomposable
by auto
show ?thesis
using a' μ ν μν 1 2 preserves_arr H⇩R_def R.dom_simp R.cod_simp R.comp_char
R.seq_char⇩S⇩b⇩C R.inclusion whisker_right
by metis
qed
qed
qed
lemma H⇩L_preserved_along_iso:
assumes "weak_unit a" and "a ≅ a'"
shows "endofunctor (Left a) (H⇩L a')"
proof -
have a: "ide a ∧ weak_unit a" using assms isomorphic_def by auto
have a': "ide a'" using assms isomorphic_def by auto
interpret L: subcategory V ‹left a› using a left_hom_is_subcategory by simp
have *: "⋀μ. L.arr μ ⟹ H⇩L a' μ = a' ⋆ μ"
using assms H⇩L_def by simp
have preserves_arr: "⋀μ. L.arr μ ⟹ L.arr (H⇩L a' μ)"
using assms a' * L.arr_char⇩S⇩b⇩C left_def weak_unit_def weak_unit_self_composable
isomorphic_implies_equicomposable L.ide_char match_4 hcomp_simps⇩W⇩C(1)
null_agreement
by metis
show "endofunctor L.comp (H⇩L a')"
proof
show "⋀μ. ¬ L.arr μ ⟹ H⇩L a' μ = L.null"
using assms L.arr_char⇩S⇩b⇩C L.null_char left_def H⇩L_def null_agreement
left_respects_isomorphic
by metis
fix μ
assume "L.arr μ"
hence μ: "L.arr μ ∧ arr μ ∧ left a μ ∧ left a' μ ∧ a ⋆ μ ≠ null ∧ a' ⋆ μ ≠ null"
using assms L.arr_char⇩S⇩b⇩C left_respects_isomorphic composable_implies_arr null_agreement
left_def
by metis
show "L.arr (H⇩L a' μ)" using μ preserves_arr by blast
show "L.dom (H⇩L a' μ) = H⇩L a' (L.dom μ)"
using a' μ * L.arr_char⇩S⇩b⇩C L.dom_char⇩S⇩b⇩C preserves_arr hom_connected(2) left_def
by simp
show "L.cod (H⇩L a' μ) = H⇩L a' (L.cod μ)"
using a' μ * L.arr_char⇩S⇩b⇩C L.cod_char⇩S⇩b⇩C preserves_arr hom_connected(4) left_def
by simp
next
fix μ ν
assume μν: "L.seq ν μ"
have "L.arr μ"
using μν by (elim L.seqE, auto)
hence μ: "L.arr μ ∧ arr μ ∧ left a μ ∧ left a' μ ∧ a ⋆ μ ≠ null ∧ a' ⋆ μ ≠ null"
using assms L.arr_char⇩S⇩b⇩C left_respects_isomorphic composable_implies_arr null_agreement
left_def
by metis
have ν: "«ν : L.cod μ ⇒ L.cod ν» ∧ arr ν ∧
left a ν ∧ a ⋆ ν ≠ null ∧ left a' ν ∧ a' ⋆ ν ≠ null"
by (metis (mono_tags, opaque_lifting) L.arrE L.cod_simp L.seq_char⇩S⇩b⇩C μν assms(2)
in_homI seqE left_def left_respects_isomorphic)
show "H⇩L a' (L.comp ν μ) = L.comp (H⇩L a' ν) (H⇩L a' μ)"
proof -
have 1: "L.arr (H⇩L a' ν)"
using ν preserves_arr by blast
have 2: "seq (a' ⋆ ν) (a' ⋆ μ)"
using a' μ ν L.arr_char⇩S⇩b⇩C L.inclusion L.dom_char⇩S⇩b⇩C L.cod_char⇩S⇩b⇩C
isomorphic_implies_equicomposable
by auto
show ?thesis
using a' μ ν μν 1 2 preserves_arr H⇩L_def L.dom_simp L.cod_simp L.comp_char
L.seq_char⇩S⇩b⇩C L.inclusion whisker_left
by metis
qed
qed
qed
end
subsection "Regularity"
text ‹
We call a weak composition \emph{regular} if ‹f ⋆ a ≅ f› whenever ‹a› is a source of
1-cell ‹f›, and ‹b ⋆ f ≅ f› whenever ‹b› is a target of ‹f›. A consequence of regularity
is that horizontal composability of 2-cells is fully determined by their sets of
sources and targets.
›
locale regular_weak_composition =
weak_composition +
assumes comp_ide_source: "⟦ a ∈ sources f; ide f ⟧ ⟹ f ⋆ a ≅ f"
and comp_target_ide: "⟦ b ∈ targets f; ide f ⟧ ⟹ b ⋆ f ≅ f"
begin
lemma sources_determine_composability:
assumes "a ∈ sources τ"
shows "τ ⋆ μ ≠ null ⟷ a ⋆ μ ≠ null"
proof -
have *: "⋀τ. ide τ ∧ a ∈ sources τ ⟹ τ ⋆ μ ≠ null ⟷ a ⋆ μ ≠ null"
using assms comp_ide_source isomorphic_implies_equicomposable match_1 match_3
by (meson sourcesD(3))
show ?thesis
proof -
have "arr τ" using assms composable_implies_arr by auto
thus ?thesis
using assms * [of "dom τ"] hom_connected(1) by auto
qed
qed
lemma targets_determine_composability:
assumes "b ∈ targets μ"
shows "τ ⋆ μ ≠ null ⟷ τ ⋆ b ≠ null"
proof -
have *: "⋀μ. ide μ ∧ b ∈ targets μ ⟹ τ ⋆ μ ≠ null ⟷ τ ⋆ b ≠ null"
using assms comp_target_ide isomorphic_implies_equicomposable match_2 match_4
by (meson targetsD(3))
show ?thesis
proof -
have "arr μ" using assms composable_implies_arr by auto
thus ?thesis
using assms * [of "dom μ"] hom_connected(2) by auto
qed
qed
lemma composable_if_connected:
assumes "sources ν ∩ targets μ ≠ {}"
shows "ν ⋆ μ ≠ null"
using assms targets_determine_composability by blast
lemma connected_if_composable:
assumes "ν ⋆ μ ≠ null"
shows "sources ν = targets μ"
using assms sources_determine_composability targets_determine_composability by blast
lemma iso_hcomp⇩R⇩W⇩C:
assumes "iso μ" and "iso ν" and "sources ν ∩ targets μ ≠ {}"
shows "iso (ν ⋆ μ)"
and "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
proof -
have μ: "arr μ ∧ «μ : dom μ ⇒ cod μ» ∧
iso μ ∧ «inv μ : cod μ ⇒ dom μ»"
using assms inv_in_hom arr_iff_in_hom iso_is_arr by auto
have ν: "arr ν ∧ «ν : dom ν ⇒ cod ν» ∧
iso ν ∧ «inv ν : cod ν ⇒ dom ν»"
using assms inv_in_hom by blast
have 1: "sources (inv ν) ∩ targets (inv μ) ≠ {}"
using assms μ ν sources_dom sources_cod targets_dom targets_cod arr_inv cod_inv
by metis
show "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
using assms 1 μ ν inv_in_hom inv_is_inverse comp_inv_arr
interchange [of "inv ν" ν "inv μ" μ] composable_if_connected
ide_hcomp⇩W⇩C sources_dom targets_dom interchange [of ν "inv ν" μ "inv μ"]
ide_hcomp⇩W⇩C sources_cod targets_cod ide_compE ide_dom comp_arr_inv'
inverse_arrowsE seqI' inverse_arrowsI
by metis
thus "iso (ν ⋆ μ)" by auto
qed
lemma inv_hcomp⇩R⇩W⇩C:
assumes "iso μ" and "iso ν" and "sources ν ∩ targets μ ≠ {}"
shows "inv (ν ⋆ μ) = inv ν ⋆ inv μ"
using assms iso_hcomp⇩R⇩W⇩C(2) [of μ ν] inverse_arrow_unique [of "H ν μ"] inv_is_inverse
by auto
end
subsection "Associativity"
text ‹
An \emph{associative weak composition} consists of a weak composition that has been
equipped with an \emph{associator} isomorphism: ‹«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»›
for each composable triple ‹(f, g, h)› of 1-cells, subject to naturality and
coherence conditions.
›
locale associative_weak_composition =
weak_composition +
fixes 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
assumes assoc_in_vhom⇩A⇩W⇩C:
"⟦ ide f; ide g; ide h; f ⋆ g ≠ null; g ⋆ h ≠ null ⟧ ⟹
«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
and assoc_naturality⇩A⇩W⇩C:
"⟦ τ ⋆ μ ≠ null; μ ⋆ ν ≠ null ⟧ ⟹
𝖺[cod τ, cod μ, cod ν] ⋅ ((τ ⋆ μ) ⋆ ν) = (τ ⋆ μ ⋆ ν) ⋅ 𝖺[dom τ, dom μ, dom ν]"
and iso_assoc⇩A⇩W⇩C: "⟦ ide f; ide g; ide h; f ⋆ g ≠ null; g ⋆ h ≠ null ⟧ ⟹ iso 𝖺[f, g, h]"
and pentagon⇩A⇩W⇩C:
"⟦ ide f; ide g; ide h; ide k; sources f ∩ targets g ≠ {};
sources g ∩ targets h ≠ {}; sources h ∩ targets k ≠ {} ⟧ ⟹
(f ⋆ 𝖺[g, h, k]) ⋅ 𝖺[f, g ⋆ h, k] ⋅ (𝖺[f, g, h] ⋆ k) = 𝖺[f, g, h ⋆ k] ⋅ 𝖺[f ⋆ g, h, k]"
begin
lemma assoc_in_hom⇩A⇩W⇩C:
assumes "ide f" and "ide g" and "ide h"
and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
shows "sources 𝖺[f, g, h] = sources h" and "targets 𝖺[f, g, h] = targets f"
and "«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
proof -
show 1: "«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
using assms assoc_in_vhom⇩A⇩W⇩C by simp
show "sources 𝖺[f, g, h] = sources h"
using assms 1 sources_dom [of "𝖺[f, g, h]"] sources_hcomp match_3
by (elim in_homE, auto)
show "targets 𝖺[f, g, h] = targets f"
using assms 1 targets_cod [of "𝖺[f, g, h]"] targets_hcomp match_4
by (elim in_homE, auto)
qed
lemma assoc_simps⇩A⇩W⇩C [simp]:
assumes "ide f" and "ide g" and "ide h"
and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
shows "arr 𝖺[f, g, h]"
and "dom 𝖺[f, g, h] = (f ⋆ g) ⋆ h"
and "cod 𝖺[f, g, h] = f ⋆ g ⋆ h"
proof -
have 1: "«𝖺[f, g, h] : (f ⋆ g) ⋆ h ⇒ f ⋆ g ⋆ h»"
using assms assoc_in_hom⇩A⇩W⇩C by auto
show "arr 𝖺[f, g, h]" using 1 by auto
show "dom 𝖺[f, g, h] = (f ⋆ g) ⋆ h" using 1 by auto
show "cod 𝖺[f, g, h] = f ⋆ g ⋆ h" using 1 by auto
qed
lemma assoc'_in_hom⇩A⇩W⇩C:
assumes "ide f" and "ide g" and "ide h"
and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
shows "sources (inv 𝖺[f, g, h]) = sources h" and "targets (inv 𝖺[f, g, h]) = targets f"
and "«inv 𝖺[f, g, h] : f ⋆ g ⋆ h ⇒ (f ⋆ g) ⋆ h»"
proof -
show 1: "«inv 𝖺[f, g, h] : f ⋆ g ⋆ h ⇒ (f ⋆ g) ⋆ h»"
using assms assoc_in_hom⇩A⇩W⇩C iso_assoc⇩A⇩W⇩C inv_in_hom by auto
show "sources (inv 𝖺[f, g, h]) = sources h"
using assms 1 sources_hcomp [of "f ⋆ g" h] sources_cod match_3 null_agreement
by (elim in_homE, metis)
show "targets (inv 𝖺[f, g, h]) = targets f"
using assms 1 targets_hcomp [of f "g ⋆ h"] targets_dom match_4 null_agreement
by (elim in_homE, metis)
qed
lemma assoc'_simps⇩A⇩W⇩C [simp]:
assumes "ide f" and "ide g" and "ide h"
and "f ⋆ g ≠ null" and "g ⋆ h ≠ null"
shows "arr (inv 𝖺[f, g, h])"
and "dom (inv 𝖺[f, g, h]) = f ⋆ g ⋆ h"
and "cod (inv 𝖺[f, g, h]) = (f ⋆ g) ⋆ h"
proof -
have 1: "«inv 𝖺[f, g, h] : f ⋆ g ⋆ h ⇒ (f ⋆ g) ⋆ h»"
using assms assoc'_in_hom⇩A⇩W⇩C by auto
show "arr (inv 𝖺[f, g, h])" using 1 by auto
show "dom (inv 𝖺[f, g, h]) = f ⋆ g ⋆ h" using 1 by auto
show "cod (inv 𝖺[f, g, h]) = (f ⋆ g) ⋆ h" using 1 by auto
qed
lemma assoc'_naturality⇩A⇩W⇩C:
assumes "τ ⋆ μ ≠ null" and "μ ⋆ ν ≠ null"
shows "inv 𝖺[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν) = ((τ ⋆ μ) ⋆ ν) ⋅ inv 𝖺[dom τ, dom μ, dom ν]"
proof -
have τμν: "arr τ ∧ arr μ ∧ arr ν"
using assms composable_implies_arr by simp
have 0: "dom τ ⋆ dom μ ≠ null ∧ dom μ ⋆ dom ν ≠ null ∧
cod τ ⋆ cod μ ≠ null ∧ cod μ ⋆ cod ν ≠ null"
using assms τμν hom_connected by simp
have 1: "«τ ⋆ μ ⋆ ν : dom τ ⋆ dom μ ⋆ dom ν ⇒ cod τ ⋆ cod μ ⋆ cod ν»"
using assms match_4 by auto
have 2: "«(τ ⋆ μ) ⋆ ν : (dom τ ⋆ dom μ) ⋆ dom ν ⇒ (cod τ ⋆ cod μ) ⋆ cod ν»"
using assms match_3 by auto
have "(inv 𝖺[cod τ, cod μ, cod ν] ⋅ (τ ⋆ μ ⋆ ν)) ⋅ 𝖺[dom τ, dom μ, dom ν] = (τ ⋆ μ) ⋆ ν"
proof -
have "(τ ⋆ μ) ⋆ ν = (inv 𝖺[cod τ, cod μ, cod ν] ⋅ 𝖺[cod τ, cod μ, cod ν]) ⋅ ((τ ⋆ μ) ⋆ ν)"
using 0 2 τμν assoc_in_hom⇩A⇩W⇩C iso_assoc⇩A⇩W⇩C comp_inv_arr inv_is_inverse comp_cod_arr
by auto
thus ?thesis
using assms τμν 0 2 assoc_naturality⇩A⇩W⇩C comp_assoc by metis
qed
thus ?thesis
using 0 1 2 τμν iso_assoc⇩A⇩W⇩C assoc'_in_hom⇩A⇩W⇩C inv_in_hom invert_side_of_triangle(2)
by auto
qed
end
subsection "Unitors"
text ‹
For an associative weak composition with a chosen unit isomorphism ‹ι : a ⋆ a ⇒ a›,
where ‹a› is a weak unit, horizontal composition on the right by ‹a› is a fully faithful
endofunctor ‹R› of the subcategory of arrows composable on the right with ‹a›, and is
consequently an endo-equivalence of that subcategory. This equivalence, together with the
associator isomorphisms and unit isomorphism ‹ι›, canonically associate, with each
identity arrow ‹f› composable on the right with ‹a›, a \emph{right unit} isomorphism
‹«𝗋[f] : f ⋆ a ⇒ f»›. These isomorphisms are the components of a natural isomorphism
from ‹R› to the identity functor.
›
locale right_hom_with_unit =
associative_weak_composition V H 𝖺 +
right_hom V H a
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a comp" (infixr "⋆" 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
and ι :: 'a
and a :: 'a +
assumes weak_unit_a: "weak_unit a"
and ι_in_hom: "«ι : a ⋆ a ⇒ a»"
and iso_ι: "iso ι"
begin
abbreviation R
where "R ≡ H⇩R a"
interpretation R: endofunctor S.comp R
using weak_unit_a weak_unit_self_composable endofunctor_H⇩R by simp
interpretation R: fully_faithful_functor S.comp S.comp R
using weak_unit_a weak_unit_def by simp
lemma fully_faithful_functor_R:
shows "fully_faithful_functor S.comp S.comp R"
..
definition runit ("𝗋[_]")
where "runit f ≡ THE μ. «μ : R f ⇒⇩S f» ∧ R μ = (f ⋆ ι) ⋅⇩S 𝖺[f, a, a]"
lemma iso_unit:
shows "S.iso ι" and "«ι : a ⋆ a ⇒⇩S a»"
proof -
show "«ι : a ⋆ a ⇒⇩S a»"
using weak_unit_a S.ide_char S.arr_char⇩S⇩b⇩C right_def weak_unit_self_composable
S.ideD(1) R.preserves_arr H⇩R_def S.in_hom_char⇩S⇩b⇩C right_def
ι_in_hom S.ideD(1) hom_connected(3) in_homE
by metis
thus "S.iso ι"
using iso_ι iso_char by blast
qed
lemma characteristic_iso:
assumes "S.ide f"
shows "«𝖺[f, a, a] : (f ⋆ a) ⋆ a ⇒⇩S f ⋆ a ⋆ a»"
and "«f ⋆ ι : f ⋆ a ⋆ a ⇒⇩S f ⋆ a»"
and "«(f ⋆ ι) ⋅⇩S 𝖺[f, a, a] : R (R f) ⇒⇩S R f»"
and "S.iso ((f ⋆ ι) ⋅⇩S 𝖺[f, a, a])"
proof -
have f: "S.ide f ∧ ide f"
using assms S.ide_char⇩S⇩b⇩C by simp
have a: "weak_unit a ∧ ide a ∧ S.ide a"
using weak_unit_a S.ide_char⇩S⇩b⇩C weak_unit_def S.arr_char⇩S⇩b⇩C right_def
weak_unit_self_composable
by metis
have fa: "f ⋆ a ≠ null ∧ (f ⋆ a) ⋆ a ≠ null ∧ ((f ⋆ a) ⋆ a) ⋆ a ≠ null"
using assms S.ideD(1) R.preserves_arr H⇩R_def S.not_arr_null S.null_char
by metis
have aa: "a ⋆ a ≠ null"
using a S.ideD(1) R.preserves_arr H⇩R_def S.not_arr_null weak_unit_self_composable
by auto
have f_ia: "f ⋆ ι ≠ null"
using assms S.ide_char right_def S.arr_char⇩S⇩b⇩C hom_connected(4) ι_in_hom by auto
show assoc_in_hom: "«𝖺[f, a, a] : (f ⋆ a) ⋆ a ⇒⇩S f ⋆ a ⋆ a»"
using a f fa hom_connected(1) [of "𝖺[f, a, a]" a] S.arr_char⇩S⇩b⇩C right_def
match_3 match_4 S.in_hom_char⇩S⇩b⇩C weak_unit_self_composable
by auto
show 1: "«f ⋆ ι : f ⋆ a ⋆ a ⇒⇩S f ⋆ a»"
using a f fa iso_unit left_hcomp_closed
by (simp add: f_ia ide_in_hom)
have unit_part: "«f ⋆ ι : f ⋆ a ⋆ a ⇒⇩S f ⋆ a» ∧ S.iso (f ⋆ ι)"
proof -
have "S.iso (f ⋆ ι)"
using a f fa f_ia 1 VoV.arr_char⇩S⇩b⇩C VxV.inv_simp
inv_in_hom hom_connected(2) [of f "inv ι"] VoV.arr_char⇩S⇩b⇩C VoV.iso_char⇩S⇩b⇩C
preserves_iso iso_char iso_ι S.dom_simp S.cod_simp
by auto
thus ?thesis using 1 by blast
qed
show "S.iso ((f ⋆ ι) ⋅⇩S 𝖺[f, a, a])"
using assms a f fa aa hom_connected(1) [of "𝖺[f, a, a]" a] right_def
iso_assoc⇩A⇩W⇩C iso_char S.arr_char⇩S⇩b⇩C unit_part assoc_in_hom isos_compose
S.isos_compose S.seqI' by auto
show "«(f ⋆ ι) ⋅⇩S 𝖺[f, a, a] : R (R f) ⇒⇩S R f»"
unfolding H⇩R_def using unit_part assoc_in_hom by blast
qed
lemma runit_char:
assumes "S.ide f"
shows "«𝗋[f] : R f ⇒⇩S f»" and "R 𝗋[f] = (f ⋆ ι) ⋅⇩S 𝖺[f, a, a]"
and "∃!μ. «μ : R f ⇒⇩S f» ∧ R μ = (f ⋆ ι) ⋅⇩S 𝖺[f, a, a]"
proof -
let ?P = "λμ. «μ : R f ⇒⇩S f» ∧ R μ = (f ⋆ ι) ⋅⇩S 𝖺[f, a, a]"
show "∃!μ. ?P μ"
proof -
have "∃μ. ?P μ"
using assms S.ide_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C R.preserves_ide characteristic_iso(3) R.is_full
by auto
moreover have "∀μ μ'. ?P μ ∧ ?P μ' ⟶ μ = μ'"
using R.is_faithful S.in_homE by metis
ultimately show ?thesis by blast
qed
hence "?P (THE μ. ?P μ)"
using theI' [of ?P] by fastforce
hence 1: "?P 𝗋[f]"
unfolding runit_def by blast
show "«𝗋[f] : R f ⇒⇩S f»" using 1 by fast
show "R 𝗋[f] = (f ⋆ ι) ⋅⇩S 𝖺[f, a, a]" using 1 by fast
qed
lemma iso_runit:
assumes "S.ide f"
shows "S.iso 𝗋[f]"
using assms characteristic_iso(4) runit_char R.reflects_iso by metis
lemma runit_eqI:
assumes "«f : a ⇒⇩S b»" and "«μ : R f ⇒⇩S f»"
and "R μ = ((f ⋆ ι) ⋅⇩S 𝖺[f, a, a])"
shows "μ = 𝗋[f]"
using assms S.ide_cod runit_char [of f] by blast
lemma runit_naturality:
assumes "S.arr μ"
shows "𝗋[S.cod μ] ⋅⇩S R μ = μ ⋅⇩S 𝗋[S.dom μ]"
proof -
have 1: "«𝗋[S.cod μ] ⋅⇩S R μ : R (S.dom μ) ⇒⇩S S.cod μ»"
using assms runit_char(1) S.ide_cod by blast
have 2: "S.par (𝗋[S.cod μ] ⋅⇩S R μ) (μ ⋅⇩S 𝗋[S.dom μ])"
using assms 1 S.ide_dom runit_char(1)
by (metis S.comp_in_homI' S.in_homE)
moreover have "R (𝗋[S.cod μ] ⋅⇩S R μ) = R (μ ⋅⇩S 𝗋[S.dom μ])"
proof -
have 3: "«μ ⋆ a ⋆ a : S.dom μ ⋆ a ⋆ a ⇒⇩S S.cod μ ⋆ a ⋆ a»"
using assms weak_unit_a R.preserves_hom H⇩R_def S.arr_iff_in_hom S.arr_char⇩S⇩b⇩C
by (metis match_4 weak_unit_in_vhom weak_unit_self_right S.in_hom_char⇩S⇩b⇩C
left_hcomp_closed S.not_arr_null S.null_char)
have 4: "R (𝗋[S.cod μ] ⋅⇩S R μ) = R 𝗋[S.cod μ] ⋅⇩S R (R μ)"
using assms 1 R.as_nat_trans.preserves_comp_2 by blast
also have 5: "... = ((S.cod μ ⋆ ι) ⋅⇩S 𝖺[S.cod μ, a, a]) ⋅⇩S ((μ ⋆ a) ⋆ a)"
using assms R.preserves_arr runit_char S.ide_cod H⇩R_def by auto
also have 6: "... = (S.cod μ ⋆ ι) ⋅⇩S 𝖺[S.cod μ, a, a] ⋅⇩S ((μ ⋆ a) ⋆ a)"
using assms S.comp_assoc by simp
also have "... = (S.cod μ ⋆ ι) ⋅⇩S (μ ⋆ a ⋆ a) ⋅⇩S 𝖺[S.dom μ, a, a]"
proof -
have "(μ ⋆ a ⋆ a) ⋅⇩S 𝖺[S.dom μ, a, a] = 𝖺[S.cod μ, a, a] ⋅⇩S ((μ ⋆ a) ⋆ a)"
proof -
have "(μ ⋆ a ⋆ a) ⋅⇩S 𝖺[S.dom μ, a, a] = (μ ⋆ a ⋆ a) ⋅ 𝖺[S.dom μ, a, a]"
using assms 3 S.ide_dom characteristic_iso(1) S.in_hom_char⇩S⇩b⇩C
S.comp_char S.dom_simp
by fastforce
also have "... = 𝖺[S.cod μ, a, a] ⋅ ((μ ⋆ a) ⋆ a)"
using assms weak_unit_a assoc_naturality⇩A⇩W⇩C [of μ a a] S.dom_simp S.cod_simp
weak_unit_self_composable S.arr_char⇩S⇩b⇩C right_def
by simp
also have "... = 𝖺[S.cod μ, a, a] ⋅⇩S ((μ ⋆ a) ⋆ a)"
using S.in_hom_char⇩S⇩b⇩C S.comp_char
by (metis 2 4 5 6 R.preserves_arr S.seq_char⇩S⇩b⇩C)
finally show ?thesis by blast
qed
thus ?thesis by argo
qed
also have "... = ((S.cod μ ⋆ ι) ⋅⇩S (μ ⋆ a ⋆ a)) ⋅⇩S 𝖺[S.dom μ, a, a]"
using S.comp_assoc by auto
also have "... = ((μ ⋆ a) ⋅⇩S (S.dom μ ⋆ ι)) ⋅⇩S 𝖺[S.dom μ, a, a]"
proof -
have "μ ⋆ a ⋆ a ≠ null"
using 3 S.not_arr_null by auto
moreover have "S.dom μ ⋆ ι ≠ null"
using assms S.not_arr_null
by (metis S.dom_char⇩S⇩b⇩C ι_in_hom calculation hom_connected(1-2) in_homE)
ultimately have "(S.cod μ ⋆ ι) ⋅⇩S (μ ⋆ a ⋆ a) = (μ ⋆ a) ⋅⇩S (S.dom μ ⋆ ι)"
using assms weak_unit_a iso_unit S.comp_arr_dom S.comp_cod_arr
interchange [of "S.cod μ" μ ι "a ⋆ a"] interchange [of μ "S.dom μ" a ι]
by auto
thus ?thesis by argo
qed
also have "... = (μ ⋆ a) ⋅⇩S (S.dom μ ⋆ ι) ⋅⇩S 𝖺[S.dom μ, a, a]"
using S.comp_assoc by auto
also have "... = R μ ⋅⇩S R 𝗋[S.dom μ]"
using assms runit_char(2) S.ide_dom H⇩R_def by auto
also have "... = R (μ ⋅⇩S 𝗋[S.dom μ])"
using assms S.arr_iff_in_hom [of μ] runit_char(1) S.ide_dom by fastforce
finally show ?thesis by blast
qed
ultimately show "𝗋[S.cod μ] ⋅⇩S (R μ) = μ ⋅⇩S 𝗋[S.dom μ]"
using R.is_faithful by blast
qed
abbreviation 𝔯
where "𝔯 μ ≡ if S.arr μ then μ ⋅⇩S 𝗋[S.dom μ] else null"
interpretation 𝔯: natural_transformation S.comp S.comp R S.map 𝔯
proof -
interpret 𝔯: transformation_by_components S.comp S.comp R S.map runit
using runit_char(1) runit_naturality by unfold_locales simp_all
have "𝔯.map = 𝔯"
using 𝔯.is_extensional 𝔯.map_def 𝔯.naturality 𝔯.map_simp_ide S.ide_dom S.ide_cod
S.map_def
by auto
thus "natural_transformation S.comp S.comp R S.map 𝔯"
using 𝔯.natural_transformation_axioms by auto
qed
lemma natural_transformation_𝔯:
shows "natural_transformation S.comp S.comp R S.map 𝔯" ..
interpretation 𝔯: natural_isomorphism S.comp S.comp R S.map 𝔯
using S.ide_is_iso iso_runit runit_char(1) S.isos_compose
by unfold_locales force
lemma natural_isomorphism_𝔯:
shows "natural_isomorphism S.comp S.comp R S.map 𝔯" ..
interpretation R: equivalence_functor S.comp S.comp R
using natural_isomorphism_𝔯 R.isomorphic_to_identity_is_equivalence by blast
lemma equivalence_functor_R:
shows "equivalence_functor S.comp S.comp R"
..
lemma runit_commutes_with_R:
assumes "S.ide f"
shows "𝗋[R f] = R 𝗋[f]"
using assms runit_char(1) R.preserves_hom [of "𝗋[f]" "R f" f]
runit_naturality iso_runit S.iso_is_section
S.section_is_mono S.monoE
by (metis S.in_homE S.seqI')
end
text ‹
Symmetric results hold for the subcategory of all arrows composable on the left with
a specified weak unit ‹b›. This yields the \emph{left unitors}.
›
locale left_hom_with_unit =
associative_weak_composition V H 𝖺 +
left_hom V H b
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a comp" (infixr "⋆" 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
and ι :: 'a
and b :: 'a +
assumes weak_unit_b: "weak_unit b"
and ι_in_hom: "«ι : b ⋆ b ⇒ b»"
and iso_ι: "iso ι"
begin
abbreviation L
where "L ≡ H⇩L b"
interpretation L: endofunctor S.comp L
using weak_unit_b weak_unit_self_composable endofunctor_H⇩L by simp
interpretation L: fully_faithful_functor S.comp S.comp L
using weak_unit_b weak_unit_def by simp
lemma fully_faithful_functor_L:
shows "fully_faithful_functor S.comp S.comp L"
..
definition lunit ("𝗅[_]")
where "lunit f ≡ THE μ. «μ : L f ⇒⇩S f» ∧ L μ = (ι ⋆ f) ⋅⇩S (inv 𝖺[b, b, f])"
lemma iso_unit:
shows "S.iso ι" and "«ι : b ⋆ b ⇒⇩S b»"
proof -
show "«ι : b ⋆ b ⇒⇩S b»"
using weak_unit_b S.ide_char S.arr_char⇩S⇩b⇩C left_def weak_unit_self_composable
S.ideD(1) L.preserves_arr H⇩L_def S.in_hom_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C left_def
ι_in_hom S.ideD(1) hom_connected(4) in_homE
by metis
thus "S.iso ι"
using iso_ι iso_char by blast
qed
lemma characteristic_iso:
assumes "S.ide f"
shows "«inv 𝖺[b, b, f] : b ⋆ b ⋆ f ⇒⇩S (b ⋆ b) ⋆ f»"
and "«ι ⋆ f : (b ⋆ b) ⋆ f ⇒⇩S b ⋆ f»"
and "«(ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f] : L (L f) ⇒⇩S L f»"
and "S.iso ((ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f])"
proof -
have f: "S.ide f ∧ ide f"
using assms S.ide_char⇩S⇩b⇩C by simp
have b: "weak_unit b ∧ ide b ∧ S.ide b"
using weak_unit_b S.ide_char⇩S⇩b⇩C weak_unit_def S.arr_char⇩S⇩b⇩C left_def
weak_unit_self_composable
by metis
have bf: "b ⋆ f ≠ null ∧ b ⋆ b ⋆ b ⋆ f ≠ null"
using assms S.ideD(1) L.preserves_arr H⇩L_def S.not_arr_null S.null_char
by metis
have bb: "b ⋆ b ≠ null"
using b S.ideD(1) L.preserves_arr H⇩L_def S.not_arr_null weak_unit_self_composable
by auto
have ib_f: "ι ⋆ f ≠ null"
using assms S.ide_char left_def S.arr_char⇩S⇩b⇩C hom_connected(3) ι_in_hom
by auto
show assoc_in_hom: "«inv 𝖺[b, b, f] : b ⋆ b ⋆ f ⇒⇩S (b ⋆ b) ⋆ f»"
using b f bf bb hom_connected(2) [of b "inv 𝖺[b, b, f]"] left_def
by (metis S.arrI⇩S⇩b⇩C S.cod_closed S.in_hom_char⇩S⇩b⇩C assoc'_in_hom⇩A⇩W⇩C(3) assoc'_simps⇩A⇩W⇩C(2-3))
show 1: "«ι ⋆ f : (b ⋆ b) ⋆ f ⇒⇩S b ⋆ f»"
using b f bf right_hcomp_closed
by (simp add: ib_f ide_in_hom iso_unit(2))
have unit_part: "«ι ⋆ f : (b ⋆ b) ⋆ f ⇒⇩S b ⋆ f» ∧ S.iso (ι ⋆ f)"
proof -
have "S.iso (ι ⋆ f)"
using b f bf ib_f 1 VoV.arr_char⇩S⇩b⇩C VxV.inv_simp
inv_in_hom hom_connected(1) [of "inv ι" f] VoV.arr_char⇩S⇩b⇩C VoV.iso_char⇩S⇩b⇩C
preserves_iso iso_char iso_ι S.dom_simp S.cod_simp
by auto
thus ?thesis using 1 by blast
qed
show "S.iso ((ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f])"
using assms b f bf bb hom_connected(2) [of b "inv 𝖺[b, b, f]"] left_def
iso_assoc⇩A⇩W⇩C iso_char S.arr_char⇩S⇩b⇩C unit_part assoc_in_hom isos_compose
S.isos_compose S.seqI' by auto
show "«(ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f] : L (L f) ⇒⇩S L f»"
unfolding H⇩L_def using unit_part assoc_in_hom by blast
qed
lemma lunit_char:
assumes "S.ide f"
shows "«𝗅[f] : L f ⇒⇩S f»" and "L 𝗅[f] = (ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f]"
and "∃!μ. «μ : L f ⇒⇩S f» ∧ L μ = (ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f]"
proof -
let ?P = "λμ. «μ : L f ⇒⇩S f» ∧ L μ = (ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f]"
show "∃!μ. ?P μ"
proof -
have "∃μ. ?P μ"
proof -
have 1: "S.ide f"
using assms S.ide_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C by simp
moreover have "S.ide (L f)"
using 1 L.preserves_ide by simp
ultimately show ?thesis
using assms characteristic_iso(3) L.is_full by blast
qed
moreover have "∀μ μ'. ?P μ ∧ ?P μ' ⟶ μ = μ'"
using L.is_faithful S.in_homE by metis
ultimately show ?thesis by blast
qed
hence "?P (THE μ. ?P μ)"
using theI' [of ?P] by fastforce
hence 1: "?P 𝗅[f]"
unfolding lunit_def by blast
show "«𝗅[f] : L f ⇒⇩S f»" using 1 by fast
show "L 𝗅[f] = (ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f]" using 1 by fast
qed
lemma iso_lunit:
assumes "S.ide f"
shows "S.iso 𝗅[f]"
using assms characteristic_iso(4) lunit_char L.reflects_iso by metis
lemma lunit_eqI:
assumes "«f : a ⇒⇩S b»" and "«μ : L f ⇒⇩S f»"
and "L μ = ((ι ⋆ f) ⋅⇩S inv 𝖺[b, b, f])"
shows "μ = 𝗅[f]"
using assms S.ide_cod lunit_char [of f] by blast
lemma lunit_naturality:
assumes "S.arr μ"
shows "𝗅[S.cod μ] ⋅⇩S L μ = μ ⋅⇩S 𝗅[S.dom μ]"
proof -
have 1: "«𝗅[S.cod μ] ⋅⇩S L μ : L (S.dom μ) ⇒⇩S S.cod μ»"
using assms lunit_char(1) [of "S.cod μ"] S.ide_cod by blast
have "S.par (𝗅[S.cod μ] ⋅⇩S L μ) (μ ⋅⇩S 𝗅[S.dom μ])"
using assms 1 S.ide_dom lunit_char(1)
by (metis S.comp_in_homI' S.in_homE)
moreover have "L (𝗅[S.cod μ] ⋅⇩S L μ) = L (μ ⋅⇩S 𝗅[S.dom μ])"
proof -
have 2: "«b ⋆ b ⋆ μ : b ⋆ b ⋆ S.dom μ ⇒⇩S b ⋆ b ⋆ S.cod μ»"
using assms weak_unit_b L.preserves_hom H⇩L_def S.arr_iff_in_hom [of μ] S.arr_char⇩S⇩b⇩C
by simp
have 3: "«(b ⋆ b) ⋆ μ : (b ⋆ b) ⋆ S.dom μ ⇒⇩S (b ⋆ b) ⋆ S.cod μ»"
using assms weak_unit_b L.preserves_hom H⇩L_def S.arr_iff_in_hom S.arr_char⇩S⇩b⇩C
by (metis match_3 weak_unit_in_vhom weak_unit_self_left S.in_hom_char⇩S⇩b⇩C
S.not_arr_null S.null_char right_hcomp_closed)
have "L (𝗅[S.cod μ] ⋅⇩S L μ) = L 𝗅[S.cod μ] ⋅⇩S L (L μ)"
using assms 1 L.as_nat_trans.preserves_comp_2 by blast
also have "... = ((ι ⋆ S.cod μ) ⋅⇩S inv 𝖺[b, b, S.cod μ]) ⋅⇩S (b ⋆ b ⋆ μ)"
using assms L.preserves_arr lunit_char S.ide_cod H⇩L_def by auto
also have "... = (ι ⋆ S.cod μ) ⋅⇩S inv 𝖺[b, b, S.cod μ] ⋅⇩S (b ⋆ b ⋆ μ)"
using S.comp_assoc by auto
also have "... = (ι ⋆ S.cod μ) ⋅⇩S ((b ⋆ b) ⋆ μ) ⋅⇩S inv 𝖺[b, b, S.dom μ]"
proof -
have "inv 𝖺[b, b, S.cod μ] ⋅⇩S (b ⋆ b ⋆ μ) = ((b ⋆ b) ⋆ μ) ⋅⇩S inv 𝖺[b, b, S.dom μ]"
proof -
have "((b ⋆ b) ⋆ μ) ⋅⇩S inv 𝖺[b, b, S.dom μ] = ((b ⋆ b) ⋆ μ) ⋅ inv 𝖺[b, b, S.dom μ]"
using assms 3 S.in_hom_char⇩S⇩b⇩C S.comp_char [of "(b ⋆ b) ⋆ μ" "inv 𝖺[b, b, S.dom μ]"]
by (metis S.ide_dom characteristic_iso(1) ext)
also have "... = inv 𝖺[b, b, S.cod μ] ⋅ (b ⋆ b ⋆ μ)"
using assms weak_unit_b assoc'_naturality⇩A⇩W⇩C [of b b μ] S.dom_simp S.cod_simp
weak_unit_self_composable S.arr_char⇩S⇩b⇩C left_def
by simp
also have "... = inv 𝖺[b, b, S.cod μ] ⋅⇩S (b ⋆ b ⋆ μ)"
using assms 2 S.in_hom_char⇩S⇩b⇩C S.comp_char
by (metis S.comp_simp S.ide_cod S.seqI' characteristic_iso(1))
finally show ?thesis by argo
qed
thus ?thesis by argo
qed
also have "... = ((ι ⋆ S.cod μ) ⋅⇩S ((b ⋆ b) ⋆ μ)) ⋅⇩S inv 𝖺[b, b, S.dom μ]"
using S.comp_assoc by auto
also have "... = ((b ⋆ μ) ⋅⇩S (ι ⋆ S.dom μ)) ⋅⇩S inv 𝖺[b, b, S.dom μ]"
proof -
have "(b ⋆ b) ⋆ μ ≠ null"
using 3 S.not_arr_null by (elim S.in_homE, auto)
moreover have "ι ⋆ S.dom μ ≠ null"
using assms S.not_arr_null
by (metis S.dom_char⇩S⇩b⇩C ι_in_hom calculation hom_connected(1-2) in_homE)
ultimately have "(ι ⋆ S.cod μ) ⋅⇩S ((b ⋆ b) ⋆ μ) = (b ⋆ μ) ⋅⇩S (ι ⋆ S.dom μ)"
using assms weak_unit_b iso_unit S.comp_arr_dom S.comp_cod_arr
interchange [of ι "b ⋆ b" "S.cod μ" μ ] interchange [of b ι μ "S.dom μ"]
by auto
thus ?thesis by argo
qed
also have "... = (b ⋆ μ) ⋅⇩S (ι ⋆ S.dom μ) ⋅⇩S inv 𝖺[b, b, S.dom μ]"
using S.comp_assoc by auto
also have "... = L μ ⋅⇩S L 𝗅[S.dom μ]"
using assms lunit_char(2) S.ide_dom H⇩L_def by auto
also have "... = L (μ ⋅⇩S 𝗅[S.dom μ])"
using assms S.arr_iff_in_hom [of μ] lunit_char(1) S.ide_dom S.seqI
by fastforce
finally show ?thesis by blast
qed
ultimately show "𝗅[S.cod μ] ⋅⇩S L μ = μ ⋅⇩S 𝗅[S.dom μ]"
using L.is_faithful by blast
qed
abbreviation 𝔩
where "𝔩 μ ≡ if S.arr μ then μ ⋅⇩S 𝗅[S.dom μ] else null"
interpretation 𝔩: natural_transformation S.comp S.comp L S.map 𝔩
proof -
interpret 𝔩: transformation_by_components S.comp S.comp L S.map lunit
using lunit_char(1) lunit_naturality by (unfold_locales, simp_all)
have "𝔩.map = 𝔩"
using 𝔩.is_extensional 𝔩.map_def 𝔩.naturality 𝔩.map_simp_ide S.ide_dom S.ide_cod
S.map_def
by auto
thus "natural_transformation S.comp S.comp L S.map 𝔩"
using 𝔩.natural_transformation_axioms by auto
qed
lemma natural_transformation_𝔩:
shows "natural_transformation S.comp S.comp L S.map 𝔩" ..
interpretation 𝔩: natural_isomorphism S.comp S.comp L S.map 𝔩
using S.ide_is_iso iso_lunit lunit_char(1) S.isos_compose
by (unfold_locales, force)
lemma natural_isomorphism_𝔩:
shows "natural_isomorphism S.comp S.comp L S.map 𝔩" ..
interpretation L: equivalence_functor S.comp S.comp L
using natural_isomorphism_𝔩 L.isomorphic_to_identity_is_equivalence by blast
lemma equivalence_functor_L:
shows "equivalence_functor S.comp S.comp L"
..
lemma lunit_commutes_with_L:
assumes "S.ide f"
shows "𝗅[L f] = L 𝗅[f]"
using assms lunit_char(1) L.preserves_hom [of "𝗅[f]" "L f" f]
lunit_naturality iso_lunit S.iso_is_section
S.section_is_mono S.monoE
by (metis S.in_homE S.seqI')
end
subsection "Prebicategories"
text ‹
A \emph{prebicategory} is an associative weak composition satisfying the additional assumption
that every arrow has a source and a target.
›
locale prebicategory =
associative_weak_composition +
assumes arr_has_source: "arr μ ⟹ sources μ ≠ {}"
and arr_has_target: "arr μ ⟹ targets μ ≠ {}"
begin
lemma arr_iff_has_src:
shows "arr μ ⟷ sources μ ≠ {}"
using arr_has_source composable_implies_arr by auto
lemma arr_iff_has_trg:
shows "arr μ ⟷ targets μ ≠ {}"
using arr_has_target composable_implies_arr by auto
end
text ‹
The horizontal composition of a prebicategory is regular.
›
sublocale prebicategory ⊆ regular_weak_composition V H
proof
show "⋀a f. a ∈ sources f ⟹ ide f ⟹ f ⋆ a ≅ f"
proof -
fix a f
assume a: "a ∈ sources f" and f: "ide f"
interpret Right_a: subcategory V ‹right a›
using a right_hom_is_subcategory weak_unit_self_composable by force
interpret Right_a: right_hom_with_unit V H 𝖺 ‹some_unit a› a
using a iso_some_unit by (unfold_locales, auto)
show "f ⋆ a ≅ f"
proof -
have "Right_a.ide f"
using a f Right_a.ide_char⇩S⇩b⇩C Right_a.arr_char⇩S⇩b⇩C right_def by auto
hence "Right_a.iso (Right_a.runit f) ∧ (Right_a.runit f) ∈ Right_a.hom (f ⋆ a) f"
using Right_a.iso_runit Right_a.runit_char(1) H⇩R_def by simp
hence "iso (Right_a.runit f) ∧ (Right_a.runit f) ∈ hom (f ⋆ a) f"
using Right_a.iso_char Right_a.hom_char by auto
thus ?thesis using f isomorphic_def by auto
qed
qed
show "⋀b f. b ∈ targets f ⟹ ide f ⟹ b ⋆ f ≅ f"
proof -
fix b f
assume b: "b ∈ targets f" and f: "ide f"
interpret Left_b: subcategory V ‹left b›
using b left_hom_is_subcategory weak_unit_self_composable by force
interpret Left_b: left_hom_with_unit V H 𝖺 ‹some_unit b› b
using b iso_some_unit by (unfold_locales, auto)
show "b ⋆ f ≅ f"
proof -
have "Left_b.ide f"
using b f Left_b.ide_char⇩S⇩b⇩C Left_b.arr_char⇩S⇩b⇩C left_def by auto
hence "Left_b.iso (Left_b.lunit f) ∧ (Left_b.lunit f) ∈ Left_b.hom (b ⋆ f) f"
using b f Left_b.iso_lunit Left_b.lunit_char(1) H⇩L_def by simp
hence "iso (Left_b.lunit f) ∧ (Left_b.lunit f) ∈ hom (b ⋆ f) f"
using Left_b.iso_char Left_b.hom_char by auto
thus ?thesis using isomorphic_def by auto
qed
qed
qed
text ‹
The regularity allows us to show that, in a prebicategory, all sources of
a given arrow are isomorphic, and similarly for targets.
›
context prebicategory
begin
lemma sources_are_isomorphic:
assumes "a ∈ sources μ" and "a' ∈ sources μ"
shows "a ≅ a'"
proof -
have μ: "arr μ" using assms composable_implies_arr by auto
have "⋀f. ⟦ ide f; a ∈ sources f; a' ∈ sources f ⟧ ⟹ a ≅ a'"
using μ assms(1) comp_ide_source comp_target_ide [of a a']
weak_unit_self_composable(1) [of a] weak_unit_self_composable(1) [of a']
isomorphic_transitive isomorphic_symmetric
sources_determine_composability sourcesD(2-3)
by (metis (full_types) connected_if_composable)
moreover have "ide (dom μ) ∧ a ∈ sources (dom μ) ∧ a' ∈ sources (dom μ)"
using assms μ sources_dom by auto
ultimately show ?thesis by auto
qed
lemma targets_are_isomorphic:
assumes "b ∈ targets μ" and "b' ∈ targets μ"
shows "b ≅ b'"
proof -
have μ: "arr μ" using assms composable_implies_arr by auto
have "⋀f. ⟦ ide f; b ∈ targets f; b' ∈ targets f ⟧ ⟹ b ≅ b'"
by (metis connected_if_composable sources_are_isomorphic targetsD(3))
moreover have "ide (dom μ) ∧ b ∈ targets (dom μ) ∧ b' ∈ targets (dom μ)"
using assms μ targets_dom [of μ] by auto
ultimately show ?thesis by auto
qed
text ‹
In fact, we now show that the sets of sources and targets of a 2-cell are
isomorphism-closed, and hence are isomorphism classes.
We first show that the notion ``weak unit'' is preserved under isomorphism.
›
interpretation H: partial_composition H
using is_partial_composition by auto
lemma isomorphism_respects_weak_units:
assumes "weak_unit a" and "a ≅ a'"
shows "weak_unit a'"
proof -
obtain φ where φ: "iso φ ∧ «φ : a ⇒ a'»"
using assms by auto
interpret Left_a: subcategory V ‹left a›
using assms left_hom_is_subcategory by fastforce
interpret Left_a: left_hom_with_unit V H 𝖺 ‹some_unit a› a
using assms iso_some_unit weak_unit_self_composable
apply unfold_locales by auto
interpret Right_a: subcategory V "right a"
using assms right_hom_is_subcategory by fastforce
interpret Right_a: right_hom_with_unit V H 𝖺 ‹some_unit a› a
using assms iso_some_unit weak_unit_self_composable
apply unfold_locales by auto
have a': "ide a' ∧ a ⋆ a' ≠ null ∧ a' ⋆ a ≠ null ∧ a' ⋆ a' ≠ null ∧
φ ⋆ a' ≠ null ∧ Left_a.ide a'"
by (metis (no_types, lifting) Left_a.left_hom_axioms Right_a.weak_unit_a φ assms(2)
ide_cod hom_connected(1) in_homE isomorphic_implies_equicomposable(1)
left_def left_hom_def subcategory.ideI⇩S⇩b⇩C isomorphic_implies_equicomposable(2)
weak_unit_self_composable(3))
have iso: "a' ⋆ a' ≅ a'"
proof -
have 1: "Right a' = Right a"
using assms right_respects_isomorphic by simp
interpret Right_a': subcategory V ‹right a'›
using assms right_hom_is_subcategory by fastforce
interpret Ra': endofunctor ‹Right a'› ‹H⇩R a'›
using assms a' endofunctor_H⇩R by auto
let ?ψ = "Left_a.lunit a' ⋅ inv (φ ⋆ a')"
have "iso ?ψ ∧ «?ψ : a' ⋆ a' ⇒ a'»"
proof -
have "iso (Left_a.lunit a') ∧ «Left_a.lunit a' : a ⋆ a' ⇒ a'»"
using a' Left_a.lunit_char(1) Left_a.iso_lunit Left_a.iso_char
Left_a.in_hom_char⇩S⇩b⇩C H⇩L_def
by auto
moreover have "iso (φ ⋆ a') ∧ «φ ⋆ a' : a ⋆ a' ⇒ a' ⋆ a'»"
using a' φ 1 Right_a'.arr_char⇩S⇩b⇩C Right_a'.in_hom_char⇩S⇩b⇩C Right_a.iso_char
right_def Ra'.preserves_iso Ra'.preserves_hom Right_a'.iso_char⇩S⇩b⇩C
Ra'.preserves_dom Ra'.preserves_cod Right_a'.arr_iff_in_hom H⇩R_def
by metis
ultimately show ?thesis
using isos_compose by blast
qed
thus ?thesis using isomorphic_def by auto
qed
text ‹
We show that horizontal composition on the left and right by @{term a'}
is naturally isomorphic to the identity functor. This follows from the fact
that if @{term a} is isomorphic to @{term a'}, then horizontal composition with @{term a}
is naturally isomorphic to horizontal composition with @{term a'}, hence the latter is
naturally isomorphic to the identity if the former is.
This is conceptually simple, but there are tedious composability details to handle.
›
have 1: "Left a' = Left a ∧ Right a' = Right a"
using assms left_respects_isomorphic right_respects_isomorphic by simp
interpret L: fully_faithful_functor ‹Left a› ‹Left a› ‹H⇩L a›
using assms weak_unit_def by simp
interpret L': endofunctor ‹Left a› ‹H⇩L a'›
using a' 1 endofunctor_H⇩L [of a'] by auto
interpret Φ: natural_isomorphism ‹Left a› ‹Left a› ‹H⇩L a› ‹H⇩L a'› ‹H⇩L φ›
proof
fix μ
show "¬ Left_a.arr μ ⟹ H⇩L φ μ = Left_a.null"
using left_def φ H⇩L_def hom_connected(1) Left_a.null_char null_agreement
Left_a.arr_char⇩S⇩b⇩C
by auto
assume "Left_a.arr μ"
hence μ: "Left_a.arr μ ∧ arr μ ∧ a ⋆ μ ≠ null"
using Left_a.arr_char⇩S⇩b⇩C left_def composable_implies_arr by simp
have 2: "φ ⋆ μ ≠ null"
using assms φ μ Left_a.arr_char⇩S⇩b⇩C left_def hom_connected by auto
show "Left_a.dom (H⇩L φ μ) = H⇩L a (Left_a.dom μ)"
using assms 2 φ μ Left_a.arr_char⇩S⇩b⇩C left_def hom_connected(2) [of a φ]
weak_unit_self_composable match_4 Left_a.dom_char⇩S⇩b⇩C H⇩L_def by auto
show "Left_a.cod (H⇩L φ μ) = H⇩L a' (Left_a.cod μ)"
using assms 2 φ μ Left_a.arr_char⇩S⇩b⇩C left_def hom_connected(2) [of a φ]
weak_unit_self_composable match_4 Left_a.cod_char⇩S⇩b⇩C H⇩L_def
by auto
show "Left_a.comp (H⇩L a' μ) (H⇩L φ (Left_a.dom μ)) = H⇩L φ μ"
proof -
have "Left_a.comp (H⇩L a' μ) (H⇩L φ (Left_a.dom μ)) =
Left_a.comp (a' ⋆ μ) (φ ⋆ dom μ)"
using assms 1 2 φ μ Left_a.dom_char⇩S⇩b⇩C left_def H⇩L_def by simp
also have "... = (a' ⋆ μ) ⋅ (φ ⋆ dom μ)"
proof -
have "Left_a.seq (a' ⋆ μ) (φ ⋆ dom μ)"
proof (intro Left_a.seqI)
show 3: "Left_a.arr (φ ⋆ dom μ)"
using assms 2 φ μ Left_a.arr_char⇩S⇩b⇩C left_def
by (metis H⇩L_def L'.preserves_arr hcomp_simps⇩W⇩C(1) in_homE right_connected
paste_1)
show 4: "Left_a.arr (a' ⋆ μ)"
using μ H⇩L_def L'.preserves_arr by auto
show "Left_a.dom (a' ⋆ μ) = Left_a.cod (φ ⋆ dom μ)"
using a' φ μ 2 3 4 Left_a.dom_char⇩S⇩b⇩C Left_a.cod_char⇩S⇩b⇩C
by (metis Left_a.seqE Left_a.seq_char⇩S⇩b⇩C hcomp_simps⇩W⇩C(1) in_homE paste_1)
qed
thus ?thesis using Left_a.comp_char Left_a.arr_char⇩S⇩b⇩C left_def by auto
qed
also have "... = a' ⋅ φ ⋆ μ ⋅ dom μ"
using a' φ μ interchange hom_connected by auto
also have "... = φ ⋆ μ"
using φ μ comp_arr_dom comp_cod_arr by auto
finally show ?thesis using H⇩L_def by simp
qed
show "Left_a.comp (H⇩L φ (Left_a.cod μ)) (Left_a.L μ) = H⇩L φ μ"
proof -
have "Left_a.comp (H⇩L φ (Left_a.cod μ)) (Left_a.L μ) = Left_a.comp (φ ⋆ cod μ) (a ⋆ μ)"
using assms 1 2 φ μ Left_a.cod_char⇩S⇩b⇩C left_def H⇩L_def by simp
also have "... = (φ ⋆ cod μ) ⋅ (a ⋆ μ)"
proof -
have "Left_a.seq (φ ⋆ cod μ) (a ⋆ μ)"
proof (intro Left_a.seqI)
show 3: "Left_a.arr (φ ⋆ cod μ)"
using φ μ 2 Left_a.arr_char⇩S⇩b⇩C left_def
by (metis (no_types, lifting) H⇩L_def L.preserves_arr hcomp_simps⇩W⇩C(1)
in_homE right_connected paste_2)
show 4: "Left_a.arr (a ⋆ μ)"
using assms μ Left_a.arr_char⇩S⇩b⇩C left_def
using H⇩L_def L.preserves_arr by auto
show "Left_a.dom (φ ⋆ cod μ) = Left_a.cod (a ⋆ μ)"
using assms φ μ 2 3 4 Left_a.dom_char⇩S⇩b⇩C Left_a.cod_char⇩S⇩b⇩C
by (metis Left_a.seqE Left_a.seq_char⇩S⇩b⇩C hcomp_simps⇩W⇩C(1) in_homE paste_2)
qed
thus ?thesis using Left_a.comp_char Left_a.arr_char⇩S⇩b⇩C left_def by auto
qed
also have "... = φ ⋅ a ⋆ cod μ ⋅ μ"
using φ μ interchange hom_connected by auto
also have "... = φ ⋆ μ"
using φ μ comp_arr_dom comp_cod_arr by auto
finally show ?thesis using H⇩L_def by simp
qed
next
fix μ
assume μ: "Left_a.ide μ"
have 1: "φ ⋆ μ ≠ null"
using assms φ μ Left_a.ide_char Left_a.arr_char⇩S⇩b⇩C left_def hom_connected by auto
show "Left_a.iso (H⇩L φ μ)"
proof -
have "iso (φ ⋆ μ)"
proof -
have "a ∈ sources φ ∩ targets μ"
using assms φ μ 1 hom_connected weak_unit_self_composable
Left_a.ide_char Left_a.arr_char⇩S⇩b⇩C left_def connected_if_composable
by auto
thus ?thesis
using φ μ Left_a.ide_char⇩S⇩b⇩C ide_is_iso iso_hcomp⇩R⇩W⇩C(1) by blast
qed
moreover have "left a (φ ⋆ μ)"
using assms 1 φ weak_unit_self_composable hom_connected(2) [of a φ]
left_def match_4 null_agreement
by auto
ultimately show ?thesis
using Left_a.iso_char Left_a.arr_char⇩S⇩b⇩C left_iff_left_inv Left_a.inv_char H⇩L_def
by metis
qed
qed
interpret L': equivalence_functor ‹Left a'› ‹Left a'› ‹H⇩L a'›
proof -
have "naturally_isomorphic (Left a') (Left a') (H⇩L a') (identity_functor.map (Left a'))"
proof -
have "naturally_isomorphic (Left a) (Left a) (H⇩L a')
(identity_functor.map (Left a))"
by (meson Left_a.natural_isomorphism_𝔩 Φ.natural_isomorphism_axioms
naturally_isomorphic_def naturally_isomorphic_symmetric
naturally_isomorphic_transitive)
thus ?thesis
using 1 by auto
qed
thus "equivalence_functor (Left a') (Left a') (H⇩L a')"
using 1 L'.isomorphic_to_identity_is_equivalence naturally_isomorphic_def
by fastforce
qed
text ‹
Now we do the same for ‹R'›.
›
interpret R: fully_faithful_functor ‹Right a› ‹Right a› ‹H⇩R a›
using assms weak_unit_def by simp
interpret R': endofunctor ‹Right a› ‹H⇩R a'›
using a' 1 endofunctor_H⇩R [of a'] by auto
interpret Ψ: natural_isomorphism ‹Right a› ‹Right a› ‹H⇩R a› ‹H⇩R a'› ‹H⇩R φ›
proof
fix μ
show "¬ Right_a.arr μ ⟹ H⇩R φ μ = Right_a.null"
using right_def φ H⇩R_def hom_connected Right_a.null_char Right_a.arr_char⇩S⇩b⇩C
by auto
assume "Right_a.arr μ"
hence μ: "Right_a.arr μ ∧ arr μ ∧ μ ⋆ a ≠ null"
using Right_a.arr_char⇩S⇩b⇩C right_def composable_implies_arr by simp
have 2: "μ ⋆ φ ≠ null"
using assms φ μ Right_a.arr_char⇩S⇩b⇩C right_def hom_connected by auto
show "Right_a.dom (H⇩R φ μ) = H⇩R a (Right_a.dom μ)"
by (metis "2" H⇩R_def R'.is_extensional Right_a.dom_simp Right_a.null_char
‹Right_a.arr μ› φ a' hcomp_simps⇩W⇩C(2) in_homE match_3)
show "Right_a.cod (H⇩R φ μ) = H⇩R a' (Right_a.cod μ)"
using assms 2 a' φ μ Right_a.arr_char⇩S⇩b⇩C right_def hom_connected(3) [of φ a]
weak_unit_self_composable match_3 Right_a.cod_char⇩S⇩b⇩C H⇩R_def
by auto
show "Right_a.comp (H⇩R a' μ) (H⇩R φ (Right_a.dom μ)) = H⇩R φ μ"
proof -
have "Right_a.comp (H⇩R a' μ) (H⇩R φ (Right_a.dom μ)) =
Right_a.comp (μ ⋆ a') (dom μ ⋆ φ)"
using assms 1 2 φ μ Right_a.dom_char⇩S⇩b⇩C right_def H⇩R_def by simp
also have "... = (μ ⋆ a') ⋅ (dom μ ⋆ φ)"
proof -
have "Right_a.seq (μ ⋆ a') (dom μ ⋆ φ)"
proof (intro Right_a.seqI)
show 3: "Right_a.arr (dom μ ⋆ φ)"
using assms 2 φ μ Right_a.arr_char⇩S⇩b⇩C right_def
by (metis H⇩R_def R'.preserves_arr hcomp_simps⇩W⇩C(1) in_homE left_connected
paste_2)
show 4: "Right_a.arr (μ ⋆ a')"
using μ H⇩R_def R'.preserves_arr by auto
show "Right_a.dom (μ ⋆ a') = Right_a.cod (dom μ ⋆ φ)"
using a' φ μ 2 3 4 Right_a.dom_char⇩S⇩b⇩C Right_a.cod_char⇩S⇩b⇩C
by (metis Right_a.seqE Right_a.seq_char⇩S⇩b⇩C hcomp_simps⇩W⇩C(1) in_homE paste_2)
qed
thus ?thesis using Right_a.comp_char Right_a.arr_char⇩S⇩b⇩C right_def by auto
qed
also have "... = μ ⋅ dom μ ⋆ a' ⋅ φ"
using a' φ μ interchange hom_connected by auto
also have "... = μ ⋆ φ"
using φ μ comp_arr_dom comp_cod_arr by auto
finally show ?thesis using H⇩R_def by simp
qed
show "Right_a.comp (H⇩R φ (Right_a.cod μ)) (Right_a.R μ) = H⇩R φ μ"
proof -
have "Right_a.comp (H⇩R φ (Right_a.cod μ)) (Right_a.R μ)
= Right_a.comp (cod μ ⋆ φ) (μ ⋆ a)"
using assms 1 2 φ μ Right_a.cod_char⇩S⇩b⇩C right_def H⇩R_def by simp
also have "... = (cod μ ⋆ φ) ⋅ (μ ⋆ a)"
proof -
have "Right_a.seq (cod μ ⋆ φ) (μ ⋆ a)"
proof (intro Right_a.seqI)
show 3: "Right_a.arr (cod μ ⋆ φ)"
using φ μ 2 Right_a.arr_char⇩S⇩b⇩C right_def
by (metis (no_types, lifting) H⇩R_def R.preserves_arr hcomp_simps⇩W⇩C(1)
in_homE left_connected paste_1)
show 4: "Right_a.arr (μ ⋆ a)"
using assms μ Right_a.arr_char⇩S⇩b⇩C right_def
using H⇩R_def R.preserves_arr by auto
show "Right_a.dom (cod μ ⋆ φ) = Right_a.cod (μ ⋆ a)"
using assms φ μ 2 3 4 Right_a.dom_char⇩S⇩b⇩C Right_a.cod_char⇩S⇩b⇩C
by (metis Right_a.seqE Right_a.seq_char⇩S⇩b⇩C hcomp_simps⇩W⇩C(1) in_homE paste_1)
qed
thus ?thesis using Right_a.comp_char Right_a.arr_char⇩S⇩b⇩C right_def by auto
qed
also have "... = cod μ ⋅ μ ⋆ φ ⋅ a"
using φ μ interchange hom_connected by auto
also have "... = μ ⋆ φ"
using φ μ comp_arr_dom comp_cod_arr by auto
finally show ?thesis using H⇩R_def by simp
qed
next
fix μ
assume μ: "Right_a.ide μ"
have 1: "μ ⋆ φ ≠ null"
using assms φ μ Right_a.ide_char Right_a.arr_char⇩S⇩b⇩C right_def hom_connected by auto
show "Right_a.iso (H⇩R φ μ)"
proof -
have "iso (μ ⋆ φ)"
proof -
have "a ∈ targets φ ∩ sources μ"
using assms φ μ 1 hom_connected weak_unit_self_composable
Right_a.ide_char Right_a.arr_char⇩S⇩b⇩C right_def connected_if_composable
by (metis (full_types) IntI targetsI)
thus ?thesis
using φ μ Right_a.ide_char⇩S⇩b⇩C ide_is_iso iso_hcomp⇩R⇩W⇩C(1) by blast
qed
moreover have "right a (μ ⋆ φ)"
using assms 1 φ weak_unit_self_composable hom_connected(1) [of φ a]
right_def match_3 null_agreement
by auto
ultimately show ?thesis
using Right_a.iso_char Right_a.arr_char⇩S⇩b⇩C right_iff_right_inv
Right_a.inv_char H⇩R_def
by metis
qed
qed
interpret R': equivalence_functor ‹Right a'› ‹Right a'› ‹H⇩R a'›
proof -
have "naturally_isomorphic (Right a') (Right a') (H⇩R a')
(identity_functor.map (Right a'))"
proof -
have "naturally_isomorphic (Right a) (Right a) (H⇩R a') Right_a.map"
by (meson Right_a.natural_isomorphism_𝔯 Ψ.natural_isomorphism_axioms
naturally_isomorphic_def naturally_isomorphic_symmetric
naturally_isomorphic_transitive)
thus ?thesis
using 1 by auto
qed
thus "equivalence_functor (Right a') (Right a') (H⇩R a')"
using 1 R'.isomorphic_to_identity_is_equivalence naturally_isomorphic_def
by fastforce
qed
show "weak_unit a'"
using weak_unit_def iso L'.fully_faithful_functor_axioms R'.fully_faithful_functor_axioms
by blast
qed
lemma sources_iso_closed:
assumes "a ∈ sources μ" and "a ≅ a'"
shows "a' ∈ sources μ"
using assms isomorphism_respects_weak_units isomorphic_implies_equicomposable
by blast
lemma targets_iso_closed:
assumes "a ∈ targets μ" and "a ≅ a'"
shows "a' ∈ targets μ"
using assms isomorphism_respects_weak_units isomorphic_implies_equicomposable
by blast
lemma sources_eqI:
assumes "sources μ ∩ sources ν ≠ {}"
shows "sources μ = sources ν"
using assms sources_iso_closed sources_are_isomorphic by blast
lemma targets_eqI:
assumes "targets μ ∩ targets ν ≠ {}"
shows "targets μ = targets ν"
using assms targets_iso_closed targets_are_isomorphic by blast
text ‹
The sets of sources and targets of a weak unit are isomorphism classes.
›
lemma sources_char:
assumes "weak_unit a"
shows "sources a = {x. x ≅ a}"
using assms sources_iso_closed weak_unit_iff_self_source sources_are_isomorphic
isomorphic_symmetric
by blast
lemma targets_char:
assumes "weak_unit a"
shows "targets a = {x. x ≅ a}"
using assms targets_iso_closed weak_unit_iff_self_target targets_are_isomorphic
isomorphic_symmetric
by blast
end
section "Horizontal Homs"
text ‹
Here we define a locale that axiomatizes a (vertical) category ‹V› that has been
punctuated into ``horizontal homs'' by the choice of idempotent endofunctors ‹src› and ‹trg›
that assign a specific ``source'' and ``target'' 1-cell to each of its arrows.
The functors ‹src› and ‹trg› are also subject to further conditions that constrain how
they commute with each other.
›
locale horizontal_homs =
category V +
src: endofunctor V src +
trg: endofunctor V trg
for V :: "'a comp" (infixr "⋅" 55)
and src :: "'a ⇒ 'a"
and trg :: "'a ⇒ 'a" +
assumes ide_src [simp]: "arr μ ⟹ ide (src μ)"
and ide_trg [simp]: "arr μ ⟹ ide (trg μ)"
and src_src [simp]: "arr μ ⟹ src (src μ) = src μ"
and trg_trg [simp]: "arr μ ⟹ trg (trg μ) = trg μ"
and trg_src [simp]: "arr μ ⟹ trg (src μ) = src μ"
and src_trg [simp]: "arr μ ⟹ src (trg μ) = trg μ"
begin
no_notation in_hom ("«_ : _ → _»")
notation in_hom ("«_ : _ ⇒ _»")
text ‹
We define an \emph{object} to be an arrow that is its own source
(or equivalently, its own target).
›
definition obj
where "obj a ≡ arr a ∧ src a = a"
lemma obj_def':
shows "obj a ⟷ arr a ∧ trg a = a"
using trg_src src_trg obj_def by metis
lemma objI_src:
assumes "arr a" and "src a = a"
shows "obj a"
using assms obj_def by simp
lemma objI_trg:
assumes "arr a" and "trg a = a"
shows "obj a"
using assms obj_def' by simp
lemma objE [elim]:
assumes "obj a" and "⟦ ide a; src a = a; trg a = a ⟧ ⟹ T"
shows T
using assms obj_def obj_def' ide_src ide_trg by metis
lemma obj_simps :
assumes "obj a"
shows "arr a" and "src a = a" and "trg a = a" and "dom a = a" and "cod a = a"
using assms by auto
lemma obj_src [intro, simp]:
assumes "arr μ"
shows "obj (src μ)"
using assms objI_src by auto
lemma obj_trg [intro, simp]:
assumes "arr μ"
shows "obj (trg μ)"
using assms objI_trg by auto
definition in_hhom ("«_ : _ → _»")
where "in_hhom μ a b ≡ arr μ ∧ src μ = a ∧ trg μ = b"
abbreviation hhom
where "hhom a b ≡ {μ. «μ : a → b»}"
abbreviation (input) hseq⇩H⇩H
where "hseq⇩H⇩H ≡ λμ ν. arr μ ∧ arr ν ∧ src μ = trg ν"
lemma in_hhomI [intro, simp]:
assumes "arr μ" and "src μ = a" and "trg μ = b"
shows "«μ : a → b»"
using assms in_hhom_def by auto
lemma in_hhomE [elim]:
assumes "«μ : a → b»"
and "⟦ arr μ; obj a; obj b; src μ = a; trg μ = b ⟧ ⟹ T"
shows "T"
using assms in_hhom_def by auto
lemma ide_in_hom [intro]:
assumes "ide f"
shows "«f : src f → trg f»" and "«f : f ⇒ f»"
using assms by auto
lemma src_dom [simp]:
shows "src (dom μ) = src μ"
by (metis arr_dom_iff_arr obj_simps(4) obj_src src.is_extensional src.preserves_dom)
lemma src_cod [simp]:
shows "src (cod μ) = src μ"
by (metis arr_cod_iff_arr obj_simps(5) obj_src src.is_extensional src.preserves_cod)
lemma trg_dom [simp]:
shows "trg (dom μ) = trg μ"
by (metis arr_dom_iff_arr ide_char ide_trg trg.is_extensional trg.preserves_dom)
lemma trg_cod [simp]:
shows "trg (cod μ) = trg μ"
by (metis arr_cod_iff_arr ide_char ide_trg trg.is_extensional trg.preserves_cod)
lemma dom_src [simp]:
shows "dom (src μ) = src μ"
by (metis dom_null ideD(2) ide_src src.is_extensional)
lemma cod_src [simp]:
shows "cod (src μ) = src μ"
by (metis cod_null ideD(3) ide_src src.is_extensional)
lemma dom_trg [simp]:
shows "dom (trg μ) = trg μ"
by (metis dom_null ideD(2) ide_trg trg.is_extensional)
lemma cod_trg [simp]:
shows "cod (trg μ) = trg μ"
by (metis cod_null ideD(3) ide_trg trg.is_extensional)
lemma vcomp_in_hhom [intro, simp]:
assumes "seq ν μ" and "src ν = a" and "trg ν = b"
shows "«ν ⋅ μ : a → b»"
using assms src_cod [of "ν ⋅ μ"] trg_cod [of "ν ⋅ μ"] by auto
lemma src_vcomp [simp]:
assumes "seq ν μ"
shows "src (ν ⋅ μ) = src ν"
using assms src_cod [of "ν ⋅ μ"] by auto
lemma trg_vcomp [simp]:
assumes "seq ν μ"
shows "trg (ν ⋅ μ) = trg ν"
using assms trg_cod [of "ν ⋅ μ"] by auto
lemma vseq_implies_hpar:
assumes "seq ν μ"
shows "src ν = src μ" and "trg ν = trg μ"
using assms src_dom [of "ν ⋅ μ"] trg_dom [of "ν ⋅ μ"] src_cod [of "ν ⋅ μ"]
trg_cod [of "ν ⋅ μ"]
by auto
lemma vconn_implies_hpar:
assumes "«μ : f ⇒ g»"
shows "src μ = src f" and "trg μ = trg f" and "src g = src f" and "trg g = trg f"
using assms by auto
lemma src_inv [simp]:
assumes "iso μ"
shows "src (inv μ) = src μ"
using assms inv_in_hom iso_is_arr src_dom src_cod iso_inv_iso dom_inv by metis
lemma trg_inv [simp]:
assumes "iso μ"
shows "trg (inv μ) = trg μ"
using assms inv_in_hom iso_is_arr trg_dom trg_cod iso_inv_iso cod_inv by metis
lemma inv_in_hhom [intro, simp]:
assumes "iso μ" and "src μ = a" and "trg μ = b"
shows "«inv μ : a → b»"
using assms iso_is_arr by simp
lemma hhom_is_subcategory:
shows "subcategory V (λμ. «μ : a → b»)"
using src_dom trg_dom src_cod trg_cod by (unfold_locales, auto)
lemma isomorphic_objects_are_equal:
assumes "obj a" and "obj b" and "a ≅ b"
shows "a = b"
using assms isomorphic_def
by (metis dom_inv in_homE objE src_dom src_inv)
text ‹
Having the functors ‹src› and ‹trg› allows us to form categories VV and VVV
of formally horizontally composable pairs and triples of arrows.
›
sublocale VxV: product_category V V ..
sublocale VV: subcategory VxV.comp ‹λμν. hseq⇩H⇩H (fst μν) (snd μν)›
by (unfold_locales, auto)
lemma subcategory_VV:
shows "subcategory VxV.comp (λμν. hseq⇩H⇩H (fst μν) (snd μν))"
..
sublocale VxVxV: product_category V VxV.comp ..
sublocale VVV: subcategory VxVxV.comp
‹λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
src (fst τμν) = trg (fst (snd τμν))›
using VV.arr_char⇩S⇩b⇩C
by (unfold_locales, auto)
lemma subcategory_VVV:
shows "subcategory VxVxV.comp
(λτμν. arr (fst τμν) ∧ VV.arr (snd τμν) ∧
src (fst τμν) = trg (fst (snd τμν)))"
..
end
subsection "Prebicategories with Homs"
text ‹
A \emph{weak composition with homs} consists of a weak composition that is
equipped with horizontal homs in such a way that the chosen source and
target of each 2-cell ‹μ› in fact lie in the set of sources and targets,
respectively, of ‹μ›, such that horizontal composition respects the
chosen sources and targets, and such that if 2-cells ‹μ› and ‹ν› are
horizontally composable, then the chosen target of ‹μ› coincides with
the chosen source of ‹ν›.
›
locale weak_composition_with_homs =
weak_composition +
horizontal_homs +
assumes src_in_sources: "arr μ ⟹ src μ ∈ sources μ"
and trg_in_targets: "arr μ ⟹ trg μ ∈ targets μ"
and src_hcomp': "ν ⋆ μ ≠ null ⟹ src (ν ⋆ μ) = src μ"
and trg_hcomp': "ν ⋆ μ ≠ null ⟹ trg (ν ⋆ μ) = trg ν"
and seq_if_composable: "ν ⋆ μ ≠ null ⟹ src ν = trg μ"
locale prebicategory_with_homs =
prebicategory +
weak_composition_with_homs
begin
lemma composable_char⇩P⇩B⇩H:
shows "ν ⋆ μ ≠ null ⟷ arr μ ∧ arr ν ∧ src ν = trg μ"
using trg_in_targets src_in_sources composable_if_connected sourcesD(3)
targets_determine_composability seq_if_composable composable_implies_arr
by metis
lemma hcomp_in_hom⇩P⇩B⇩H:
assumes "«μ : a →⇩W⇩C b»" and "«ν : b →⇩W⇩C c»"
shows "«ν ⋆ μ : a →⇩W⇩C c»"
and "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
proof -
show "«ν ⋆ μ : a →⇩W⇩C c»"
using assms sources_determine_composability sources_hcomp targets_hcomp by auto
thus "«ν ⋆ μ : dom ν ⋆ dom μ ⇒ cod ν ⋆ cod μ»"
using assms by auto
qed
text ‹
In a prebicategory with homs, if ‹a› is an object (i.e. ‹src a = a› and ‹trg a = a›),
then ‹a› is a weak unit. The converse need not hold: there can be weak units that the
‹src› and ‹trg› mappings send to other 1-cells in the same isomorphism class.
›
lemma obj_is_weak_unit:
assumes "obj a"
shows "weak_unit a"
proof -
have "a ∈ sources a"
using assms objE src_in_sources ideD(1) by metis
thus ?thesis by auto
qed
end
subsection "Choosing Homs"
text ‹
Every prebicategory extends to a prebicategory with homs, by choosing an arbitrary
representative of each isomorphism class of weak units to serve as an object.
``The source'' of a 2-cell is defined to be the chosen representative of the set of
all its sources (which is an isomorphism class), and similarly for ``the target''.
›
context prebicategory
begin
definition rep
where "rep f ≡ SOME f'. f' ∈ { f'. f ≅ f' }"
definition some_src
where "some_src μ ≡ if arr μ then rep (SOME a. a ∈ sources μ) else null"
definition some_trg
where "some_trg μ ≡ if arr μ then rep (SOME b. b ∈ targets μ) else null"
lemma isomorphic_ide_rep:
assumes "ide f"
shows "f ≅ rep f"
proof -
have "∃f'. f' ∈ { f'. f ≅ f' }"
using assms isomorphic_reflexive by blast
thus ?thesis using rep_def someI_ex by simp
qed
lemma rep_rep:
assumes "ide f"
shows "rep (rep f) = rep f"
proof -
have "rep f ∈ { f'. f ≅ f' }"
using assms isomorphic_ide_rep by simp
have "{ f'. f ≅ f' } = { f'. rep f ≅ f' }"
proof -
have "⋀f'. f ≅ f' ⟷ rep f ≅ f'"
proof
fix f'
assume f': "f ≅ f'"
show "rep f ≅ f'"
proof -
obtain φ where φ: "φ ∈ hom f f' ∧ iso φ"
using f' by auto
obtain ψ where ψ: "ψ ∈ hom f (rep f) ∧ iso ψ"
using assms isomorphic_ide_rep by blast
have "inv ψ ∈ hom (rep f) f ∧ iso (inv ψ)"
using ψ by simp
hence "iso (V φ (inv ψ)) ∧ V φ (inv ψ) ∈ hom (rep f) f'"
using φ isos_compose by auto
thus ?thesis using isomorphic_def by auto
qed
next
fix f'
assume f': "rep f ≅ f'"
show "f ≅ f'"
using assms f' isomorphic_ide_rep isos_compose isomorphic_def
by (meson isomorphic_transitive)
qed
thus ?thesis by auto
qed
hence "rep (rep f) = (SOME f'. f' ∈ { f'. f ≅ f' })"
using assms rep_def by fastforce
also have "... = rep f"
using assms rep_def by simp
finally show ?thesis by simp
qed
lemma some_src_in_sources:
assumes "arr μ"
shows "some_src μ ∈ sources μ"
proof -
have 1: "(SOME a. a ∈ sources μ) ∈ sources μ"
using assms arr_iff_has_src someI_ex [of "λa. a ∈ sources μ"] by blast
moreover have "ide (SOME a. a ∈ sources μ)"
using 1 weak_unit_self_composable by auto
ultimately show ?thesis
using assms 1 some_src_def sources_iso_closed isomorphic_ide_rep by metis
qed
lemma some_trg_in_targets:
assumes "arr μ"
shows "some_trg μ ∈ targets μ"
proof -
have 1: "(SOME a. a ∈ targets μ) ∈ targets μ"
using assms arr_iff_has_trg someI_ex [of "λa. a ∈ targets μ"] by blast
moreover have "ide (SOME a. a ∈ targets μ)"
using 1 weak_unit_self_composable by auto
ultimately show ?thesis
using assms 1 some_trg_def targets_iso_closed isomorphic_ide_rep by metis
qed
lemma some_src_dom:
assumes "arr μ"
shows "some_src (dom μ) = some_src μ"
using assms some_src_def sources_dom by simp
lemma some_src_cod:
assumes "arr μ"
shows "some_src (cod μ) = some_src μ"
using assms some_src_def sources_cod by simp
lemma some_trg_dom:
assumes "arr μ"
shows "some_trg (dom μ) = some_trg μ"
using assms some_trg_def targets_dom by simp
lemma some_trg_cod:
assumes "arr μ"
shows "some_trg (cod μ) = some_trg μ"
using assms some_trg_def targets_cod by simp
lemma ide_some_src:
assumes "arr μ"
shows "ide (some_src μ)"
using assms some_src_in_sources weak_unit_self_composable by blast
lemma ide_some_trg:
assumes "arr μ"
shows "ide (some_trg μ)"
using assms some_trg_in_targets weak_unit_self_composable by blast
lemma some_src_composable:
assumes "arr τ"
shows "τ ⋆ μ ≠ null ⟷ some_src τ ⋆ μ ≠ null"
using assms some_src_in_sources sources_determine_composability by blast
lemma some_trg_composable:
assumes "arr σ"
shows "μ ⋆ σ ≠ null ⟷ μ ⋆ some_trg σ ≠ null"
using assms some_trg_in_targets targets_determine_composability by blast
lemma sources_some_src:
assumes "arr μ"
shows "sources (some_src μ) = sources μ"
using assms sources_determine_composability some_src_in_sources by blast
lemma targets_some_trg:
assumes "arr μ"
shows "targets (some_trg μ) = targets μ"
using assms targets_determine_composability some_trg_in_targets by blast
lemma src_some_src:
assumes "arr μ"
shows "some_src (some_src μ) = some_src μ"
using assms some_src_def ide_some_src sources_some_src by force
lemma trg_some_trg:
assumes "arr μ"
shows "some_trg (some_trg μ) = some_trg μ"
using assms some_trg_def ide_some_trg targets_some_trg by force
lemma sources_char':
assumes "arr μ"
shows "a ∈ sources μ ⟷ some_src μ ≅ a"
using assms some_src_in_sources sources_iso_closed sources_are_isomorphic by meson
lemma targets_char':
assumes "arr μ"
shows "a ∈ targets μ ⟷ some_trg μ ≅ a"
using assms some_trg_in_targets targets_iso_closed targets_are_isomorphic by meson
text ‹
An arbitrary choice of sources and targets in a prebicategory results in a notion of
formal composability that coincides with the actual horizontal composability
of the prebicategory.
›
lemma composable_char⇩P⇩B:
shows "τ ⋆ σ ≠ null ⟷ arr σ ∧ arr τ ∧ some_src τ = some_trg σ"
proof
assume στ: "τ ⋆ σ ≠ null"
show "arr σ ∧ arr τ ∧ some_src τ = some_trg σ"
using στ composable_implies_arr connected_if_composable some_src_def some_trg_def
by force
next
assume στ: "arr σ ∧ arr τ ∧ some_src τ = some_trg σ"
show "τ ⋆ σ ≠ null"
using στ some_src_in_sources some_trg_composable by force
qed
text ‹
A 1-cell is its own source if and only if it is its own target.
›
lemma self_src_iff_self_trg:
assumes "ide a"
shows "a = some_src a ⟷ a = some_trg a"
proof
assume a: "a = some_src a"
have "weak_unit a ∧ a ⋆ a ≠ null"
using assms a some_src_in_sources [of a] by force
thus "a = some_trg a" using a composable_char⇩P⇩B by simp
next
assume a: "a = some_trg a"
have "weak_unit a ∧ a ⋆ a ≠ null"
using assms a some_trg_in_targets [of a] by force
thus "a = some_src a" using a composable_char⇩P⇩B by simp
qed
lemma some_trg_some_src:
assumes "arr μ"
shows "some_trg (some_src μ) = some_src μ"
using assms ide_some_src some_src_def some_trg_def some_src_in_sources sources_char
targets_char sources_some_src
by force
lemma src_some_trg:
assumes "arr μ"
shows "some_src (some_trg μ) = some_trg μ"
using assms ide_some_trg some_src_def some_trg_def some_trg_in_targets sources_char
targets_char targets_some_trg
by force
lemma some_src_eqI:
assumes "a ∈ sources μ" and "some_src a = a"
shows "some_src μ = a"
using assms sources_char' some_src_def some_src_in_sources sources_are_isomorphic
isomorphic_symmetric isomorphic_transitive
by (metis composable_char⇩P⇩B sourcesD(3))
lemma some_trg_eqI:
assumes "b ∈ targets μ" and "some_trg b = b"
shows "some_trg μ = b"
using assms targets_char' some_trg_def some_trg_in_targets targets_are_isomorphic
isomorphic_symmetric isomorphic_transitive
by (metis composable_char⇩P⇩B targetsD(3))
lemma some_src_comp:
assumes "τ ⋆ σ ≠ null"
shows "some_src (τ ⋆ σ) = some_src σ"
proof (intro some_src_eqI [of "some_src σ" "τ ⋆ σ"])
show "some_src (some_src σ) = some_src σ"
using assms src_some_src composable_implies_arr by simp
show "some_src σ ∈ sources (H τ σ)"
using assms some_src_in_sources composable_char⇩P⇩B
by (simp add: sources_hcomp)
qed
lemma some_trg_comp:
assumes "τ ⋆ σ ≠ null"
shows "some_trg (τ ⋆ σ) = some_trg τ"
proof (intro some_trg_eqI [of "some_trg τ" "τ ⋆ σ"])
show "some_trg (some_trg τ) = some_trg τ"
using assms trg_some_trg composable_implies_arr by simp
show "some_trg τ ∈ targets (H τ σ)"
using assms some_trg_in_targets composable_char⇩P⇩B
by (simp add: targets_hcomp)
qed
text ‹
The mappings that take an arrow to its chosen source or target are endofunctors
of the vertical category, which commute with each other in the manner required
for horizontal homs.
›
interpretation S: endofunctor V some_src
using some_src_def ide_some_src some_src_dom some_src_cod
apply unfold_locales
apply auto[4]
proof -
fix ν μ
assume μν: "seq ν μ"
show "some_src (ν ⋅ μ) = some_src ν ⋅ some_src μ"
using μν some_src_dom [of "ν ⋅ μ"] some_src_dom some_src_cod [of "ν ⋅ μ"]
some_src_cod ide_some_src
by auto
qed
interpretation T: endofunctor V some_trg
using some_trg_def ide_some_trg some_trg_dom some_trg_cod
apply unfold_locales
apply auto[4]
proof -
fix ν μ
assume μν: "seq ν μ"
show "some_trg (ν ⋅ μ) = some_trg ν ⋅ some_trg μ"
using μν some_trg_dom [of "ν ⋅ μ"] some_trg_dom some_trg_cod [of "ν ⋅ μ"]
some_trg_cod ide_some_trg
by auto
qed
interpretation weak_composition_with_homs V H some_src some_trg
apply unfold_locales
using some_src_in_sources some_trg_in_targets
src_some_src trg_some_trg src_some_trg some_trg_some_src
some_src_comp some_trg_comp composable_char⇩P⇩B ide_some_src ide_some_trg
by simp_all
proposition extends_to_weak_composition_with_homs:
shows "weak_composition_with_homs V H some_src some_trg"
..
proposition extends_to_prebicategory_with_homs:
shows "prebicategory_with_homs V H 𝖺 some_src some_trg"
..
end
subsection "Choosing Units"
text ‹
A \emph{prebicategory with units} is a prebicategory equipped with a choice,
for each weak unit ‹a›, of a ``unit isomorphism'' ‹«𝗂[a] : a ⋆ a ⇒ a»›.
›
locale prebicategory_with_units =
prebicategory V H 𝖺 +
weak_composition V H
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a comp" (infixr "⋆" 53)
and 𝖺 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("𝖺[_, _, _]")
and 𝗂 :: "'a ⇒ 'a" ("𝗂[_]") +
assumes unit_in_vhom⇩P⇩B⇩U: "weak_unit a ⟹ «𝗂[a] : a ⋆ a ⇒ a»"
and iso_unit⇩P⇩B⇩U: "weak_unit a ⟹ iso 𝗂[a]"
begin
lemma unit_in_hom⇩P⇩B⇩U:
assumes "weak_unit a"
shows "«𝗂[a] : a →⇩W⇩C a»" and "«𝗂[a] : a ⋆ a ⇒ a»"
proof -
show 1: "«𝗂[a] : a ⋆ a ⇒ a»"
using assms unit_in_vhom⇩P⇩B⇩U by auto
show "«𝗂[a] : a →⇩W⇩C a»"
using assms 1 weak_unit_iff_self_source weak_unit_iff_self_target
sources_cod [of "𝗂[a]"] targets_cod [of "𝗂[a]"]
by (elim in_homE, auto)
qed
lemma unit_simps [simp]:
assumes "weak_unit a"
shows "arr 𝗂[a]" and "dom 𝗂[a] = a ⋆ a" and "cod 𝗂[a] = a"
using assms unit_in_vhom⇩P⇩B⇩U by auto
end
text ‹
Every prebicategory extends to a prebicategory with units, simply by choosing the
unit isomorphisms arbitrarily.
›
context prebicategory
begin
proposition extends_to_prebicategory_with_units:
shows "prebicategory_with_units V H 𝖺 some_unit"
using iso_some_unit by (unfold_locales, auto)
end
subsection "Horizontal Composition"
text ‹
The following locale axiomatizes a (vertical) category ‹V› with horizontal homs,
which in addition has been equipped with a functorial operation ‹H› of
horizontal composition from ‹VV› to ‹V›, assumed to preserve source and target.
›
locale horizontal_composition =
horizontal_homs V src trg +
H: "functor" VV.comp V ‹λμν. H (fst μν) (snd μν)›
for V :: "'a comp" (infixr "⋅" 55)
and H :: "'a ⇒ 'a ⇒ 'a" (infixr "⋆" 53)
and src :: "'a ⇒ 'a"
and trg :: "'a ⇒ 'a" +
assumes src_hcomp: "arr (μ ⋆ ν) ⟹ src (μ ⋆ ν) = src ν"
and trg_hcomp: "arr (μ ⋆ ν) ⟹ trg (μ ⋆ ν) = trg μ"
begin
no_notation in_hom ("«_ : _ → _»")
text ‹
‹H› is a partial composition, which shares its null with ‹V›.
›
lemma is_partial_composition:
shows "partial_composition H" and "partial_magma.null H = null"
proof -
have 1: "∀f. null ⋆ f = null ∧ f ⋆ null = null"
using H.is_extensional VV.arr_char⇩S⇩b⇩C not_arr_null by auto
interpret H: partial_composition H
using 1 VV.arr_char⇩S⇩b⇩C H.is_extensional not_arr_null
by unfold_locales metis
show "partial_composition H" ..
show "H.null = null"
using 1 H.null_def the1_equality [of "λn. ∀f. n ⋆ f = n ∧ f ⋆ n = n"]
by metis
qed
text ‹
\textbf{Note:} The following is ``almost'' ‹H.seq›, but for that we would need
‹H.arr = V.arr›.
This would be unreasonable to expect, in general, as the definition of ‹H.arr› is based
on ``strict'' units rather than weak units.
Later we will show that we do have ‹H.arr = V.arr› if the vertical category is discrete.
›
abbreviation hseq
where "hseq ν μ ≡ arr (ν ⋆ μ)"
lemma hseq_char:
shows "hseq ν μ ⟷ arr μ ∧ arr ν ∧ src ν = trg μ"
proof -
have "hseq ν μ ⟷ VV.arr (ν, μ)"
using H.is_extensional H.preserves_arr by force
also have "... ⟷ arr μ ∧ arr ν ∧ src ν = trg μ"
using VV.arr_char⇩S⇩b⇩C by force
finally show ?thesis by blast
qed
lemma hseq_char':
shows "hseq ν μ ⟷ ν ⋆ μ ≠ null"
using VV.arr_char⇩S⇩b⇩C H.preserves_arr H.is_extensional hseq_char [of ν μ] by auto
lemma hseqI' [intro, simp]:
assumes "arr μ" and "arr ν" and "src ν = trg μ"
shows "hseq ν μ"
using assms hseq_char by simp
lemma hseqI:
assumes "«μ : a → b»" and "«ν : b → c»"
shows "hseq ν μ"
using assms hseq_char by auto
lemma hseqE [elim]:
assumes "hseq ν μ"
and "arr μ ⟹ arr ν ⟹ src ν = trg μ ⟹ T"
shows "T"
using assms hseq_char by simp
lemma hcomp_simps [simp]:
assumes "hseq ν μ"
shows "src (ν ⋆ μ) = src μ" and "trg (ν ⋆ μ) = trg ν"
and "dom (ν ⋆ μ) = dom ν ⋆ dom μ" and "cod (ν ⋆ μ) = cod ν ⋆ cod μ"
using assms VV.arr_char⇩S⇩b⇩C src_hcomp apply blast
using assms VV.arr_char⇩S⇩b⇩C trg_hcomp apply blast
using assms VV.arr_char⇩S⇩b⇩C H.preserves_dom VV.dom_simp apply force
using assms VV.arr_char⇩S⇩b⇩C H.preserves_cod VV.cod_simp by force
lemma ide_hcomp [intro, simp]:
assumes "ide ν" and "ide μ" and "src ν = trg μ"
shows "ide (ν ⋆ μ)"
using assms VV.ide_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C H.preserves_ide [of "(ν, μ)"] by auto
lemma hcomp_in_hhom [intro]:
assumes "«μ : a → b»" and "«ν : b → c»"
shows "«ν ⋆ μ : a → c»"
using assms hseq_char by fastforce
lemma hcomp_in_hhom' :
assumes "arr μ" and "arr ν" and "src μ = a" and "trg ν = c" and "src ν = trg μ"
shows "«ν ⋆ μ : a → c»"
using assms hseq_char by fastforce
lemma hcomp_in_hhomE [elim]:
assumes "«ν ⋆ μ : a → c»"
and "⟦ arr μ; arr ν; src ν = trg μ; src μ = a; trg ν = c ⟧ ⟹ T"
shows T
using assms in_hhom_def by fastforce
lemma hcomp_in_vhom [intro]:
assumes "«μ : f ⇒ g»" and "«ν : h ⇒ k»" and "src h = trg f"
shows "«ν ⋆ μ : h ⋆ f ⇒ k ⋆ g»"
using assms by fastforce
lemma hcomp_in_vhom' :
assumes "hseq ν μ"
and "dom μ = f" and "dom ν = h" and "cod μ = g" and "cod ν = k"
assumes "«μ : f ⇒ g»" and "«ν : h ⇒ k»" and "src h = trg f"
shows "«ν ⋆ μ : h ⋆ f ⇒ k ⋆ g»"
using assms by fastforce
lemma hcomp_in_vhomE [elim]:
assumes "«ν ⋆ μ : f ⇒ g»"
and "⟦ arr μ; arr ν; src ν = trg μ; src μ = src f; src μ = src g;
trg ν = trg f; trg ν = trg g ⟧ ⟹ T"
shows T
using assms in_hom_def
by (metis in_homE hseqE src_cod src_dom src_hcomp trg_cod trg_dom trg_hcomp)
text ‹
A horizontal composition yields a weak composition by simply forgetting
the ‹src› and ‹trg› functors.
›
lemma match_1:
assumes "ν ⋆ μ ≠ null" and "(ν ⋆ μ) ⋆ τ ≠ null"
shows "μ ⋆ τ ≠ null"
using assms H.is_extensional not_arr_null VV.arr_char⇩S⇩b⇩C hseq_char hseq_char' by auto
lemma match_2:
assumes "ν ⋆ (μ ⋆ τ) ≠ null" and "μ ⋆ τ ≠ null"
shows "ν ⋆ μ ≠ null"
using assms H.is_extensional not_arr_null VV.arr_char⇩S⇩b⇩C hseq_char hseq_char' by auto
lemma match_3:
assumes "μ ⋆ τ ≠ null" and "ν ⋆ μ ≠ null"
shows "(ν ⋆ μ) ⋆ τ ≠ null"
using assms H.is_extensional not_arr_null VV.arr_char⇩S⇩b⇩C hseq_char hseq_char' by auto
lemma match_4:
assumes "μ ⋆ τ ≠ null" and "ν ⋆ μ ≠ null"
shows "ν ⋆ (μ ⋆ τ) ≠ null"
using assms H.is_extensional not_arr_null VV.arr_char⇩S⇩b⇩C hseq_char hseq_char' by auto
lemma left_connected:
assumes "seq ν ν'"
shows "ν ⋆ μ ≠ null ⟷ ν' ⋆ μ ≠ null"
using assms H.is_extensional not_arr_null VV.arr_char⇩S⇩b⇩C hseq_char'
by (metis hseq_char seqE vseq_implies_hpar(1))
lemma right_connected:
assumes "seq μ μ'"
shows "H ν μ ≠ null ⟷ H ν μ' ≠ null"
using assms H.is_extensional not_arr_null VV.arr_char⇩S⇩b⇩C hseq_char'
by (metis hseq_char seqE vseq_implies_hpar(2))
proposition is_weak_composition:
shows "weak_composition V H"
proof -
have 1: "(λμν. fst μν ⋆ snd μν ≠ null)
= (λμν. arr (fst μν) ∧ arr (snd μν) ∧ src (fst μν) = trg (snd μν))"
using hseq_char' by auto
interpret VoV: subcategory VxV.comp ‹λμν. fst μν ⋆ snd μν ≠ null›
using 1 VV.subcategory_axioms by simp
interpret H: "functor" VoV.comp V ‹λμν. fst μν ⋆ snd μν›
using H.functor_axioms 1 by simp
show ?thesis
using match_1 match_2 match_3 match_4 left_connected right_connected
by (unfold_locales, metis)
qed
interpretation weak_composition V H
using is_weak_composition by auto
text ‹
It can be shown that ‹arr ((ν ⋅ μ) ⋆ (τ ⋅ σ)) ⟹ (ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)›.
However, we do not have ‹arr ((ν ⋆ τ) ⋅ (μ ⋆ σ)) ⟹ (ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)›,
because it does not follow from ‹arr ((ν ⋆ τ) ⋅ (μ ⋆ σ))› that ‹dom ν = cod μ›
and ‹dom τ = cod σ›, only that ‹dom ν ⋆ dom τ = cod μ ⋆ cod σ›.
So we don't get interchange unconditionally.
›
lemma interchange:
assumes "seq ν μ" and "seq τ σ"
shows "(ν ⋅ μ) ⋆ (τ ⋅ σ) = (ν ⋆ τ) ⋅ (μ ⋆ σ)"
using assms interchange by simp
lemma whisker_right:
assumes "ide f" and "seq ν μ"
shows "(ν ⋅ μ) ⋆ f = (ν ⋆ f) ⋅ (μ ⋆ f)"
using assms whisker_right by simp
lemma whisker_left:
assumes "ide f" and "seq ν μ"
shows "f ⋆ (ν ⋅ μ) = (f ⋆ ν) ⋅ (f ⋆ μ)"
using assms whisker_left by simp
lemma inverse_arrows_hcomp:
assumes "iso μ" and "iso ν" and "src ν = trg μ"
shows "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
proof -
show "inverse_arrows (ν ⋆ μ) (inv ν ⋆ inv μ)"
proof
show "ide ((inv ν ⋆ inv μ) ⋅ (ν ⋆ μ))"
proof -
have "(inv ν ⋆ inv μ) ⋅ (ν ⋆ μ) = dom ν ⋆ dom μ"
using assms interchange iso_is_arr comp_inv_arr'
by (metis arr_dom)
thus ?thesis
using assms iso_is_arr by simp
qed
show "ide ((ν ⋆ μ) ⋅ (inv ν ⋆ inv μ))"
proof -
have "(ν ⋆ μ) ⋅ (inv ν ⋆ inv μ) = cod ν ⋆ cod μ"
using assms interchange iso_is_arr comp_arr_inv'
by (metis arr_cod)
thus ?thesis
using assms iso_is_arr by simp
qed
qed
qed
lemma iso_hcomp [intro, simp]:
assumes "iso μ" and "iso ν" and "src ν = trg μ"
shows "iso (ν ⋆ μ)"
using assms inverse_arrows_hcomp by auto
lemma hcomp_iso_in_hom [intro]:
assumes "iso_in_hom μ f g" and "iso_in_hom ν h k" and "src ν = trg μ"
shows "iso_in_hom (ν ⋆ μ) (h ⋆ f) (k ⋆ g)"
unfolding iso_in_hom_def
using assms hcomp_in_vhom iso_hcomp iso_in_hom_def vconn_implies_hpar(1-2) by auto
lemma isomorphic_implies_ide:
assumes "f ≅ g"
shows "ide f" and "ide g"
using assms isomorphic_def by auto
lemma hcomp_ide_isomorphic:
assumes "ide f" and "g ≅ h" and "src f = trg g"
shows "f ⋆ g ≅ f ⋆ h"
proof -
obtain μ where μ: "iso μ ∧ «μ : g ⇒ h»"
using assms isomorphic_def by auto
have "iso (f ⋆ μ) ∧ «f ⋆ μ : f ⋆ g ⇒ f ⋆ h»"
using assms μ iso_hcomp by auto
thus ?thesis
using isomorphic_def by auto
qed
lemma hcomp_isomorphic_ide:
assumes "f ≅ g" and "ide h" and "src f = trg h"
shows "f ⋆ h ≅ g ⋆ h"
proof -
obtain μ where μ: "iso μ ∧ «μ : f ⇒ g»"
using assms isomorphic_def by auto
have "iso (μ ⋆ h) ∧ «μ ⋆ h : f ⋆ h ⇒ g ⋆ h»"
using assms μ iso_hcomp by auto
thus ?thesis
using isomorphic_def by auto
qed
lemma isomorphic_implies_hpar:
assumes "f ≅ f'"
shows "ide f" and "ide f'" and "src f = src f'" and "trg f = trg f'"
using assms isomorphic_def by auto
lemma inv_hcomp [simp]:
assumes "iso ν" and "iso μ" and "src ν = trg μ"
shows "inv (ν ⋆ μ) = inv ν ⋆ inv μ"
using assms inverse_arrow_unique [of "ν ⋆ μ"] inv_is_inverse inverse_arrows_hcomp
by auto
text ‹
The following define the two ways of using horizontal composition to compose three arrows.
›
definition HoHV
where "HoHV μ ≡ if VVV.arr μ then (fst μ ⋆ fst (snd μ)) ⋆ snd (snd μ) else null"
definition HoVH
where "HoVH μ ≡ if VVV.arr μ then fst μ ⋆ fst (snd μ) ⋆ snd (snd μ) else null"
lemma functor_HoHV:
shows "functor VVV.comp V HoHV"
apply unfold_locales
using VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.dom_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C VVV.comp_char HoHV_def
apply auto[4]
proof -
fix f g
assume fg: "VVV.seq g f"
show "HoHV (VVV.comp g f) = HoHV g ⋅ HoHV f"
proof -
have "VxVxV.comp g f =
(fst g ⋅ fst f, fst (snd g) ⋅ fst (snd f), snd (snd g) ⋅ snd (snd f))"
using fg VVV.seq_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VxVxV.comp_char VxV.comp_char
by (metis (no_types, lifting) VxV.seqE⇩P⇩C VxVxV.seqE⇩P⇩C)
hence "HoHV (VVV.comp g f) =
(fst g ⋅ fst f ⋆ fst (snd g) ⋅ fst (snd f)) ⋆ snd (snd g) ⋅ snd (snd f)"
using HoHV_def VVV.comp_simp fg by auto
also have "... = ((fst g ⋆ fst (snd g)) ⋆ snd (snd g)) ⋅
((fst f ⋆ fst (snd f)) ⋆ snd (snd f))"
using fg VVV.seq_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C interchange
by (metis (no_types, lifting) VxV.seqE⇩P⇩C VxVxV.seqE⇩P⇩C hseqI' src_vcomp trg_vcomp)
also have "... = HoHV g ⋅ HoHV f"
using HoHV_def fg by auto
finally show ?thesis by simp
qed
qed
sublocale HoHV: "functor" VVV.comp V HoHV
using functor_HoHV by simp
lemma functor_HoVH:
shows "functor VVV.comp V HoVH"
apply unfold_locales
using VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VVV.dom_char⇩S⇩b⇩C VVV.cod_char⇩S⇩b⇩C VVV.comp_char
HoHV_def HoVH_def
apply auto[4]
proof -
fix f g
assume fg: "VVV.seq g f"
show "HoVH (VVV.comp g f) = HoVH g ⋅ HoVH f"
proof -
have "VxVxV.comp g f =
(fst g ⋅ fst f, fst (snd g) ⋅ fst (snd f), snd (snd g) ⋅ snd (snd f))"
using fg VVV.seq_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C VxVxV.comp_char VxV.comp_char
by (metis (no_types, lifting) VxV.seqE⇩P⇩C VxVxV.seqE⇩P⇩C)
hence "HoVH (VVV.comp g f) =
fst g ⋅ fst f ⋆ fst (snd g) ⋅ fst (snd f) ⋆ snd (snd g) ⋅ snd (snd f)"
using HoVH_def VVV.comp_simp fg by auto
also have "... = (fst g ⋆ fst (snd g) ⋆ snd (snd g)) ⋅
(fst f ⋆ fst (snd f) ⋆ snd (snd f))"
using fg VVV.seq_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C interchange
by (metis (no_types, lifting) VxV.seqE⇩P⇩C VxVxV.seqE⇩P⇩C hseqI' src_vcomp trg_vcomp)
also have "... = HoVH g ⋅ HoVH f"
using fg VVV.seq_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C HoVH_def VVV.comp_char VV.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting))
finally show ?thesis by simp
qed
qed
sublocale HoVH: "functor" VVV.comp V HoVH
using functor_HoVH by simp
text ‹
The following define horizontal composition of an arrow on the left by its target
and on the right by its source.
›
abbreviation L
where "L ≡ λμ. if arr μ then trg μ ⋆ μ else null"
abbreviation R
where "R ≡ λμ. if arr μ then μ ⋆ src μ else null"
sublocale L: endofunctor V L
using vseq_implies_hpar(2) whisker_left
by (unfold_locales, auto)
lemma endofunctor_L:
shows "endofunctor V L"
..
sublocale R: endofunctor V R
using vseq_implies_hpar(1) whisker_right
by (unfold_locales, auto)
lemma endofunctor_R:
shows "endofunctor V R"
..
end
end