Theory NaturalTransformation
chapter NaturalTransformation
theory NaturalTransformation
imports Functor
begin
section "Definition of a Natural Transformation"
text‹
As is the case for functors, the ``object-free'' definition of category
makes it possible to view natural transformations as functions on arrows.
In particular, a natural transformation between functors
@{term F} and @{term G} from @{term A} to @{term B} can be represented by
the map that takes each arrow @{term f} of @{term A} to the diagonal of the
square in @{term B} corresponding to the transformation of @{term "F f"}
to @{term "G f"}. The images of the identities of @{term A} under this
map are the usual components of the natural transformation.
This representation exhibits natural transformations as a kind of generalization
of functors, and in fact we can directly identify functors with identity
natural transformations.
However, functors are still necessary to state the defining conditions for
a natural transformation, as the domain and codomain of a natural transformation
cannot be recovered from the map on arrows that represents it.
Like functors, natural transformations preserve arrows and map non-arrows to null.
Natural transformations also ``preserve'' domain and codomain, but in a more general
sense than functors. The naturality conditions, which express the two ways of factoring
the diagonal of a commuting square, are degenerate in the case of an identity transformation.
›
locale natural_transformation =
A: category A +
B: category B +
F: "functor" A B F +
G: "functor" A B G
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and τ :: "'a ⇒ 'b" +
assumes is_extensional: "¬A.arr f ⟹ τ f = B.null"
and preserves_dom [iff]: "A.arr f ⟹ B.dom (τ f) = F (A.dom f)"
and preserves_cod [iff]: "A.arr f ⟹ B.cod (τ f) = G (A.cod f)"
and is_natural_1 [iff]: "A.arr f ⟹ G f ⋅⇩B τ (A.dom f) = τ f"
and is_natural_2 [iff]: "A.arr f ⟹ τ (A.cod f) ⋅⇩B F f = τ f"
begin
lemma naturality:
assumes "A.arr f"
shows "τ (A.cod f) ⋅⇩B F f = G f ⋅⇩B τ (A.dom f)"
using assms is_natural_1 is_natural_2 by simp
text‹
The following fact for natural transformations provides us with the same advantages
as the corresponding fact for functors.
›
lemma preserves_reflects_arr [iff]:
shows "B.arr (τ f) ⟷ A.arr f"
using is_extensional A.arr_cod_iff_arr B.arr_cod_iff_arr preserves_cod by force
lemma preserves_hom [intro]:
assumes "«f : a →⇩A b»"
shows "«τ f : F a →⇩B G b»"
using assms
by (metis A.in_homE B.arr_cod_iff_arr B.in_homI G.preserves_arr G.preserves_cod
preserves_cod preserves_dom)
lemma preserves_comp_1:
assumes "A.seq f' f"
shows "τ (f' ⋅⇩A f) = G f' ⋅⇩B τ f"
using assms
by (metis A.seqE A.dom_comp B.comp_assoc G.preserves_comp is_natural_1)
lemma preserves_comp_2:
assumes "A.seq f' f"
shows "τ (f' ⋅⇩A f) = τ f' ⋅⇩B F f"
using assms
by (metis A.arr_cod_iff_arr A.cod_comp B.comp_assoc F.preserves_comp is_natural_2)
text‹
A natural transformation that also happens to be a functor is equal to
its own domain and codomain.
›
lemma functor_implies_equals_dom:
assumes "functor A B τ"
shows "F = τ"
proof
interpret τ: "functor" A B τ using assms by auto
fix f
show "F f = τ f"
using assms
by (metis A.dom_cod B.comp_cod_arr F.is_extensional F.preserves_arr F.preserves_cod
τ.preserves_dom is_extensional is_natural_2 preserves_dom)
qed
lemma functor_implies_equals_cod:
assumes "functor A B τ"
shows "G = τ"
proof
interpret τ: "functor" A B τ using assms by auto
fix f
show "G f = τ f"
using assms
by (metis A.cod_dom B.comp_arr_dom G.is_extensional G.preserves_arr
G.preserves_dom B.cod_dom functor_implies_equals_dom is_extensional
is_natural_1 preserves_cod preserves_dom)
qed
end
section "Components of a Natural Transformation"
text‹
The values taken by a natural transformation on identities are the \emph{components}
of the transformation. We have the following basic technique for proving two natural
transformations equal: show that they have the same components.
›
lemma eqI:
assumes "natural_transformation A B F G σ" and "natural_transformation A B F G σ'"
and "⋀a. partial_composition.ide A a ⟹ σ a = σ' a"
shows "σ = σ'"
proof -
interpret A: category A using assms(1) natural_transformation_def by blast
interpret σ: natural_transformation A B F G σ using assms(1) by auto
interpret σ': natural_transformation A B F G σ' using assms(2) by auto
have "⋀f. σ f = σ' f"
using assms(3) σ.is_natural_2 σ'.is_natural_2 σ.is_extensional σ'.is_extensional A.ide_cod
by metis
thus ?thesis by auto
qed
text‹
As equality of natural transformations is determined by equality of components,
a natural transformation may be uniquely defined by specifying its components.
The extension to all arrows is given by @{prop is_natural_1} or equivalently
by @{prop is_natural_2}.
›
locale transformation_by_components =
A: category A +
B: category B +
F: "functor" A B F +
G: "functor" A B G
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and t :: "'a ⇒ 'b" +
assumes maps_ide_in_hom [intro]: "A.ide a ⟹ «t a : F a →⇩B G a»"
and is_natural: "A.arr f ⟹ t (A.cod f) ⋅⇩B F f = G f ⋅⇩B t (A.dom f)"
begin
definition map
where "map f = (if A.arr f then t (A.cod f) ⋅⇩B F f else B.null)"
lemma map_simp_ide [simp]:
assumes "A.ide a"
shows "map a = t a"
using assms map_def B.comp_arr_dom [of "t a"] maps_ide_in_hom by fastforce
lemma is_natural_transformation:
shows "natural_transformation A B F G map"
using map_def is_natural
apply (unfold_locales, simp_all)
apply (metis A.ide_dom B.dom_comp B.seqI
G.preserves_arr G.preserves_dom B.in_homE maps_ide_in_hom)
apply (metis A.ide_dom B.arrI B.cod_comp B.in_homE B.seqI
G.preserves_arr G.preserves_cod G.preserves_dom maps_ide_in_hom)
apply (metis A.ide_dom B.comp_arr_dom B.in_homE maps_ide_in_hom)
by (metis B.comp_assoc A.comp_cod_arr F.preserves_comp)
end
sublocale transformation_by_components ⊆ natural_transformation A B F G map
using is_natural_transformation by auto
lemma transformation_by_components_idem [simp]:
assumes "natural_transformation A B F G τ"
shows "transformation_by_components.map A B F τ = τ"
proof -
interpret τ: natural_transformation A B F G τ using assms by blast
interpret τ': transformation_by_components A B F G τ
by (unfold_locales, auto)
show ?thesis
using assms τ'.map_simp_ide τ'.is_natural_transformation eqI by blast
qed
section "Functors as Natural Transformations"
text‹
A functor is a special case of a natural transformation, in the sense that the same map
that defines the functor also defines an identity natural transformation.
›
lemma functor_is_transformation [simp]:
assumes "functor A B F"
shows "natural_transformation A B F F F"
proof -
interpret "functor" A B F using assms by auto
show "natural_transformation A B F F F"
using is_extensional B.comp_arr_dom B.comp_cod_arr
by (unfold_locales, simp_all)
qed
sublocale "functor" ⊆ as_nat_trans: natural_transformation A B F F F
by (simp add: functor_axioms)
section "Constant Natural Transformations"
text‹
A constant natural transformation is one whose components are all the same arrow.
›
locale constant_transformation =
A: category A +
B: category B +
F: constant_functor A B "B.dom g" +
G: constant_functor A B "B.cod g"
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and g :: 'b +
assumes value_is_arr: "B.arr g"
begin
definition map
where "map f ≡ if A.arr f then g else B.null"
lemma map_simp [simp]:
assumes "A.arr f"
shows "map f = g"
using assms map_def by auto
lemma is_natural_transformation:
shows "natural_transformation A B F.map G.map map"
apply unfold_locales
using map_def value_is_arr B.comp_arr_dom B.comp_cod_arr by auto
lemma is_functor_if_value_is_ide:
assumes "B.ide g"
shows "functor A B map"
apply unfold_locales using assms map_def by auto
end
sublocale constant_transformation ⊆ natural_transformation A B F.map G.map map
using is_natural_transformation by auto
context constant_transformation
begin
lemma equals_dom_if_value_is_ide:
assumes "B.ide g"
shows "map = F.map"
using assms functor_implies_equals_dom is_functor_if_value_is_ide by auto
lemma equals_cod_if_value_is_ide:
assumes "B.ide g"
shows "map = G.map"
using assms functor_implies_equals_dom is_functor_if_value_is_ide by auto
end
section "Vertical Composition"
text‹
Vertical composition is a way of composing natural transformations ‹σ: F → G›
and ‹τ: G → H›, between parallel functors @{term F}, @{term G}, and @{term H}
to obtain a natural transformation from @{term F} to @{term H}.
The composite is traditionally denoted by ‹τ o σ›, however in the present
setting this notation is misleading because it is horizontal composite, rather than
vertical composite, that coincides with composition of natural transformations as
functions on arrows.
›
locale vertical_composite =
A: category A +
B: category B +
F: "functor" A B F +
G: "functor" A B G +
H: "functor" A B H +
σ: natural_transformation A B F G σ +
τ: natural_transformation A B G H τ
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and H :: "'a ⇒ 'b"
and σ :: "'a ⇒ 'b"
and τ :: "'a ⇒ 'b"
begin
text‹
Vertical composition takes an arrow @{term "A.in_hom a b f"} to an arrow in
@{term "B.hom (F a) (G b)"}, which we can obtain by forming either of
the composites @{term "B (τ b) (σ f)"} or @{term "B (τ f) (σ a)"}, which are
equal to each other.
›
definition map
where "map f = (if A.arr f then τ (A.cod f) ⋅⇩B σ f else B.null)"
lemma map_seq:
assumes "A.arr f"
shows "B.seq (τ (A.cod f)) (σ f)"
using assms by auto
lemma map_simp_ide:
assumes "A.ide a"
shows "map a = τ a ⋅⇩B σ a"
using assms map_def by auto
lemma map_simp_1:
assumes "A.arr f"
shows "map f = τ (A.cod f) ⋅⇩B σ f"
using assms by (simp add: map_def)
lemma map_simp_2:
assumes "A.arr f"
shows "map f = τ f ⋅⇩B σ (A.dom f)"
using assms
by (metis B.comp_assoc σ.is_natural_2 σ.naturality τ.is_natural_1 τ.naturality map_simp_1)
lemma is_natural_transformation:
shows "natural_transformation A B F H map"
using map_def map_simp_1 map_simp_2 map_seq B.comp_assoc
apply (unfold_locales, simp_all)
by (metis B.comp_assoc τ.is_natural_1)
end
sublocale vertical_composite ⊆ natural_transformation A B F H map
using is_natural_transformation by auto
text‹
Functors are the identities for vertical composition.
›
lemma vcomp_ide_dom [simp]:
assumes "natural_transformation A B F G τ"
shows "vertical_composite.map A B F τ = τ"
using assms apply (intro eqI)
apply auto[2]
apply (meson functor_is_transformation natural_transformation_def vertical_composite.intro
vertical_composite.is_natural_transformation)
proof -
fix a :: 'a
have "vertical_composite A B F F G F τ"
by (meson assms functor_is_transformation natural_transformation.axioms(1-4)
vertical_composite.intro)
thus "vertical_composite.map A B F τ a = τ a"
using assms natural_transformation.is_extensional natural_transformation.is_natural_2
vertical_composite.map_def
by fastforce
qed
lemma vcomp_ide_cod [simp]:
assumes "natural_transformation A B F G τ"
shows "vertical_composite.map A B τ G = τ"
using assms apply (intro eqI)
apply auto[2]
apply (meson functor_is_transformation natural_transformation_def vertical_composite.intro
vertical_composite.is_natural_transformation)
proof -
fix a :: 'a
assume a: "partial_composition.ide A a"
interpret Goτ: vertical_composite A B F G G τ G
by (meson assms functor_is_transformation natural_transformation.axioms(1-4)
vertical_composite.intro)
show "vertical_composite.map A B τ G a = τ a"
using assms a natural_transformation.is_extensional natural_transformation.is_natural_1
Goτ.map_simp_ide Goτ.B.comp_cod_arr
by simp
qed
text‹
Vertical composition is associative.
›
lemma vcomp_assoc [simp]:
assumes "natural_transformation A B F G ρ"
and "natural_transformation A B G H σ"
and "natural_transformation A B H K τ"
shows "vertical_composite.map A B (vertical_composite.map A B ρ σ) τ
= vertical_composite.map A B ρ (vertical_composite.map A B σ τ)"
proof -
interpret A: category A
using assms(1) natural_transformation_def functor_def by blast
interpret B: category B
using assms(1) natural_transformation_def functor_def by blast
interpret ρ: natural_transformation A B F G ρ using assms(1) by auto
interpret σ: natural_transformation A B G H σ using assms(2) by auto
interpret τ: natural_transformation A B H K τ using assms(3) by auto
interpret ρσ: vertical_composite A B F G H ρ σ ..
interpret στ: vertical_composite A B G H K σ τ ..
interpret ρ_στ: vertical_composite A B F G K ρ στ.map ..
interpret ρσ_τ: vertical_composite A B F H K ρσ.map τ ..
show ?thesis
using ρσ_τ.is_natural_transformation ρ_στ.natural_transformation_axioms
ρσ.map_simp_ide ρσ_τ.map_simp_ide ρ_στ.map_simp_ide στ.map_simp_ide B.comp_assoc
by (intro eqI, auto)
qed
section "Natural Isomorphisms"
text‹
A natural isomorphism is a natural transformation each of whose components
is an isomorphism. Equivalently, a natural isomorphism is a natural transformation
that is invertible with respect to vertical composition.
›
locale natural_isomorphism = natural_transformation A B F G τ
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and τ :: "'a ⇒ 'b" +
assumes components_are_iso [simp]: "A.ide a ⟹ B.iso (τ a)"
begin
lemma inv_naturality:
assumes "A.arr f"
shows "F f ⋅⇩B B.inv (τ (A.dom f)) = B.inv (τ (A.cod f)) ⋅⇩B G f"
using assms is_natural_1 is_natural_2 components_are_iso B.invert_side_of_triangle
B.comp_assoc A.ide_cod A.ide_dom preserves_reflects_arr
by fastforce
text ‹
Natural isomorphisms preserve isomorphisms, in the sense that the sides of
of the naturality square determined by an isomorphism are all isomorphisms,
so the diagonal is, as well.
›
lemma preserves_iso:
assumes "A.iso f"
shows "B.iso (τ f)"
using assms
by (metis A.ide_dom A.iso_is_arr B.isos_compose G.preserves_iso components_are_iso
is_natural_2 naturality preserves_reflects_arr)
end
text ‹
Since the function that represents a functor is formally identical to the function
that represents the corresponding identity natural transformation, no additional locale
is needed for identity natural transformations. However, an identity natural transformation
is also a natural isomorphism, so it is useful for @{locale functor} to inherit from the
@{locale natural_isomorphism} locale.
›
sublocale "functor" ⊆ as_nat_iso: natural_isomorphism A B F F F
apply unfold_locales
using preserves_ide B.ide_is_iso by simp
definition naturally_isomorphic
where "naturally_isomorphic A B F G = (∃τ. natural_isomorphism A B F G τ)"
lemma naturally_isomorphic_respects_full_functor:
assumes "naturally_isomorphic A B F G"
and "full_functor A B F"
shows "full_functor A B G"
proof -
obtain φ where φ: "natural_isomorphism A B F G φ"
using assms naturally_isomorphic_def by blast
interpret φ: natural_isomorphism A B F G φ
using φ by auto
interpret φ.F: full_functor A B F
using assms by auto
write A (infixr "⋅⇩A" 55)
write B (infixr "⋅⇩B" 55)
write φ.A.in_hom ("«_ : _ →⇩A _»")
write φ.B.in_hom ("«_ : _ →⇩B _»")
show "full_functor A B G"
proof
fix a a' g
assume a': "φ.A.ide a'" and a: "φ.A.ide a"
and g: "«g : G a' →⇩B G a»"
show "∃f. «f : a' →⇩A a» ∧ G f = g"
proof -
let ?g' = "φ.B.inv (φ a) ⋅⇩B g ⋅⇩B φ a'"
have g': "«?g' : F a' →⇩B F a»"
using a a' g φ.preserves_hom φ.components_are_iso φ.B.inv_in_hom by force
obtain f' where f': "«f' : a' →⇩A a» ∧ F f' = ?g'"
using a a' g' φ.F.is_full [of a a' ?g'] by blast
moreover have "G f' = g"
by (metis f' φ.A.arrI φ.B.arrI φ.B.inv_inv φ.B.invert_side_of_triangle(1-2)
φ.B.iso_inv_iso φ.G.as_nat_trans.natural_transformation_axioms
φ.components_are_iso φ.naturality a a' category.in_homE f' g'
natural_transformation.axioms(1))
ultimately show ?thesis by auto
qed
qed
qed
lemma naturally_isomorphic_respects_faithful_functor:
assumes "naturally_isomorphic A B F G"
and "faithful_functor A B F"
shows "faithful_functor A B G"
proof -
obtain φ where φ: "natural_isomorphism A B F G φ"
using assms naturally_isomorphic_def by blast
interpret φ: natural_isomorphism A B F G φ
using φ by auto
interpret φ.F: faithful_functor A B F
using assms by auto
show "faithful_functor A B G"
using φ.naturality φ.components_are_iso φ.B.iso_is_section φ.B.section_is_mono
φ.B.monoE φ.F.is_faithful φ.is_natural_1 φ.natural_transformation_axioms
φ.preserves_reflects_arr φ.A.ide_cod
by (unfold_locales, metis)
qed
locale inverse_transformation =
A: category A +
B: category B +
F: "functor" A B F +
G: "functor" A B G +
τ: natural_isomorphism A B F G τ
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and τ :: "'a ⇒ 'b"
begin
interpretation τ': transformation_by_components A B G F ‹λa. B.inv (τ a)›
proof
fix f :: 'a
show "A.ide f ⟹ «B.inv (τ f) : G f →⇩B F f»"
using B.inv_in_hom τ.components_are_iso A.ide_in_hom by blast
show "A.arr f ⟹ B.inv (τ (A.cod f)) ⋅⇩B G f = F f ⋅⇩B B.inv (τ (A.dom f))"
by (metis A.ide_cod A.ide_dom B.invert_opposite_sides_of_square τ.components_are_iso
τ.is_natural_2 τ.naturality τ.preserves_reflects_arr)
qed
definition map
where "map = τ'.map"
lemma map_ide_simp [simp]:
assumes "A.ide a"
shows "map a = B.inv (τ a)"
using assms map_def by fastforce
lemma map_simp:
assumes "A.arr f"
shows "map f = B.inv (τ (A.cod f)) ⋅⇩B G f"
using assms map_def by (simp add: τ'.map_def)
lemma is_natural_transformation:
shows "natural_transformation A B G F map"
by (simp add: τ'.natural_transformation_axioms map_def)
lemma inverts_components:
assumes "A.ide a"
shows "B.inverse_arrows (τ a) (map a)"
using assms τ.components_are_iso B.ide_is_iso B.inv_is_inverse B.inverse_arrows_def map_def
by (metis τ'.map_simp_ide)
end
sublocale inverse_transformation ⊆ natural_transformation A B G F map
using is_natural_transformation by auto
sublocale inverse_transformation ⊆ natural_isomorphism A B G F map
by (simp add: natural_isomorphism.intro natural_isomorphism_axioms.intro
natural_transformation_axioms)
lemma inverse_inverse_transformation [simp]:
assumes "natural_isomorphism A B F G τ"
shows "inverse_transformation.map A B F (inverse_transformation.map A B G τ) = τ"
proof -
interpret τ: natural_isomorphism A B F G τ
using assms by auto
interpret τ': inverse_transformation A B F G τ ..
interpret τ'': inverse_transformation A B G F τ'.map ..
show "τ''.map = τ"
using τ.natural_transformation_axioms τ''.natural_transformation_axioms
by (intro eqI, auto)
qed
locale inverse_transformations =
A: category A +
B: category B +
F: "functor" A B F +
G: "functor" A B G +
τ: natural_transformation A B F G τ +
τ': natural_transformation A B G F τ'
for A :: "'a comp" (infixr "⋅⇩A" 55)
and B :: "'b comp" (infixr "⋅⇩B" 55)
and F :: "'a ⇒ 'b"
and G :: "'a ⇒ 'b"
and τ :: "'a ⇒ 'b"
and τ' :: "'a ⇒ 'b" +
assumes inv: "A.ide a ⟹ B.inverse_arrows (τ a) (τ' a)"
sublocale inverse_transformations ⊆ natural_isomorphism A B F G τ
by (meson B.category_axioms τ.natural_transformation_axioms B.iso_def inv
natural_isomorphism.intro natural_isomorphism_axioms.intro)
sublocale inverse_transformations ⊆ natural_isomorphism A B G F τ'
by (meson category.inverse_arrows_sym category.iso_def inverse_transformations_axioms
inverse_transformations_axioms_def inverse_transformations_def
natural_isomorphism.intro natural_isomorphism_axioms.intro)
lemma inverse_transformations_sym:
assumes "inverse_transformations A B F G σ σ'"
shows "inverse_transformations A B G F σ' σ"
using assms
by (simp add: category.inverse_arrows_sym inverse_transformations_axioms_def
inverse_transformations_def)
lemma inverse_transformations_inverse:
assumes "inverse_transformations A B F G σ σ'"
shows "vertical_composite.map A B σ σ' = F"
and "vertical_composite.map A B σ' σ = G"
proof -
interpret A: category A
using assms(1) inverse_transformations_def natural_transformation_def by blast
interpret inv: inverse_transformations A B F G σ σ' using assms by auto
interpret σσ': vertical_composite A B F G F σ σ' ..
show "vertical_composite.map A B σ σ' = F"
using σσ'.is_natural_transformation inv.F.as_nat_trans.natural_transformation_axioms
σσ'.map_simp_ide inv.B.comp_inv_arr inv.inv
by (intro eqI, simp_all)
interpret inv': inverse_transformations A B G F σ' σ
using assms inverse_transformations_sym by blast
interpret σ'σ: vertical_composite A B G F G σ' σ ..
show "vertical_composite.map A B σ' σ = G"
using σ'σ.is_natural_transformation inv.G.as_nat_trans.natural_transformation_axioms
σ'σ.map_simp_ide inv'.inv inv.B.comp_inv_arr
by (intro eqI, simp_all)
qed
lemma inverse_transformations_compose:
assumes "inverse_transformations A B F G σ σ'"
and "inverse_transformations A B G H τ τ'"
shows "inverse_transformations A B F H
(vertical_composite.map A B σ τ) (vertical_composite.map A B τ' σ')"
proof -
interpret A: category A using assms(1) inverse_transformations_def by blast
interpret B: category B using assms(1) inverse_transformations_def by blast
interpret σσ': inverse_transformations A B F G σ σ' using assms(1) by auto
interpret ττ': inverse_transformations A B G H τ τ' using assms(2) by auto
interpret στ: vertical_composite A B F G H σ τ ..
interpret τ'σ': vertical_composite A B H G F τ' σ' ..
show ?thesis
using B.inverse_arrows_compose σσ'.inv στ.map_simp_ide τ'σ'.map_simp_ide ττ'.inv
by (unfold_locales, auto)
qed
lemma vertical_composite_iso_inverse [simp]:
assumes "natural_isomorphism A B F G τ"
shows "vertical_composite.map A B τ (inverse_transformation.map A B G τ) = F"
proof -
interpret τ: natural_isomorphism A B F G τ using assms by auto
interpret τ': inverse_transformation A B F G τ ..
interpret ττ': vertical_composite A B F G F τ τ'.map ..
show ?thesis
using ττ'.is_natural_transformation τ.F.as_nat_trans.natural_transformation_axioms
τ'.inverts_components τ.B.comp_inv_arr ττ'.map_simp_ide
by (intro eqI, auto)
qed
lemma vertical_composite_inverse_iso [simp]:
assumes "natural_isomorphism A B F G τ"
shows "vertical_composite.map A B (inverse_transformation.map A B G τ) τ = G"
proof -
interpret τ: natural_isomorphism A B F G τ using assms by auto
interpret τ': inverse_transformation A B F G τ ..
interpret τ'τ: vertical_composite A B G F G τ'.map τ ..
show ?thesis
using τ'τ.is_natural_transformation τ.G.as_nat_trans.natural_transformation_axioms
τ'.inverts_components τ'τ.map_simp_ide τ.B.comp_arr_inv
by (intro eqI, auto)
qed
lemma natural_isomorphisms_compose:
assumes "natural_isomorphism A B F G σ" and "natural_isomorphism A B G H τ"
shows "natural_isomorphism A B F H (vertical_composite.map A B σ τ)"
proof -
interpret A: category A
using assms(1) natural_isomorphism_def natural_transformation_def by blast
interpret B: category B
using assms(1) natural_isomorphism_def natural_transformation_def by blast
interpret σ: natural_isomorphism A B F G σ using assms(1) by auto
interpret τ: natural_isomorphism A B G H τ using assms(2) by auto
interpret στ: vertical_composite A B F G H σ τ ..
interpret natural_isomorphism A B F H στ.map
using στ.map_simp_ide by (unfold_locales, auto)
show ?thesis ..
qed
lemma naturally_isomorphic_reflexive:
assumes "functor A B F"
shows "naturally_isomorphic A B F F"
proof -
interpret F: "functor" A B F using assms by auto
have "natural_isomorphism A B F F F" ..
thus ?thesis using naturally_isomorphic_def by blast
qed
lemma naturally_isomorphic_symmetric:
assumes "naturally_isomorphic A B F G"
shows "naturally_isomorphic A B G F"
proof -
obtain φ where φ: "natural_isomorphism A B F G φ"
using assms naturally_isomorphic_def by blast
interpret φ: natural_isomorphism A B F G φ
using φ by auto
interpret ψ: inverse_transformation A B F G φ ..
have "natural_isomorphism A B G F ψ.map" ..
thus ?thesis using naturally_isomorphic_def by blast
qed
lemma naturally_isomorphic_transitive [trans]:
assumes "naturally_isomorphic A B F G"
and "naturally_isomorphic A B G H"
shows "naturally_isomorphic A B F H"
proof -
obtain φ where φ: "natural_isomorphism A B F G φ"
using assms naturally_isomorphic_def by blast
interpret φ: natural_isomorphism A B F G φ
using φ by auto
obtain ψ where ψ: "natural_isomorphism A B G H ψ"
using assms naturally_isomorphic_def by blast
interpret ψ: natural_isomorphism A B G H ψ
using ψ by auto
interpret ψφ: vertical_composite A B F G H φ ψ ..
have "natural_isomorphism A B F H ψφ.map"
using φ ψ natural_isomorphisms_compose by blast
thus ?thesis
using naturally_isomorphic_def by blast
qed
section "Horizontal Composition"
text‹
Horizontal composition is a way of composing parallel natural transformations
@{term σ} from @{term F} to @{term G} and @{term τ} from @{term H} to @{term K},
where functors @{term F} and @{term G} map @{term A} to @{term B} and
@{term H} and @{term K} map @{term B} to @{term C}, to obtain a natural transformation
from @{term "H o F"} to @{term "K o G"}.
Since horizontal composition turns out to coincide with ordinary composition of
natural transformations as functions, there is little point in defining a cumbersome
locale for horizontal composite.
›
lemma horizontal_composite:
assumes "natural_transformation A B F G σ"
and "natural_transformation B C H K τ"
shows "natural_transformation A C (H o F) (K o G) (τ o σ)"
proof -
interpret σ: natural_transformation A B F G σ
using assms(1) by simp
interpret τ: natural_transformation B C H K τ
using assms(2) by simp
interpret HF: composite_functor A B C F H ..
interpret KG: composite_functor A B C G K ..
show "natural_transformation A C (H o F) (K o G) (τ o σ)"
using σ.is_extensional τ.is_extensional
apply (unfold_locales, auto)
apply (metis σ.is_natural_1 σ.preserves_reflects_arr τ.preserves_comp_1)
by (metis σ.is_natural_2 σ.preserves_reflects_arr τ.preserves_comp_2)
qed
lemma hcomp_ide_dom [simp]:
assumes "natural_transformation A B F G τ"
shows "τ o (identity_functor.map A) = τ"
proof -
interpret τ: natural_transformation A B F G τ using assms by auto
show "τ o τ.A.map = τ"
using τ.A.map_def τ.is_extensional by fastforce
qed
lemma hcomp_ide_cod [simp]:
assumes "natural_transformation A B F G τ"
shows "(identity_functor.map B) o τ = τ"
proof -
interpret τ: natural_transformation A B F G τ using assms by auto
show "τ.B.map o τ = τ"
using τ.B.map_def τ.is_extensional by auto
qed
text‹
Horizontal composition of a functor with a vertical composite.
›
lemma whisker_right:
assumes "functor A B F"
and "natural_transformation B C H K τ" and "natural_transformation B C K L τ'"
shows "(vertical_composite.map B C τ τ') o F = vertical_composite.map A C (τ o F) (τ' o F)"
proof -
interpret F: "functor" A B F using assms(1) by auto
interpret τ: natural_transformation B C H K τ using assms(2) by auto
interpret τ': natural_transformation B C K L τ' using assms(3) by auto
interpret τoF: natural_transformation A C ‹H o F› ‹K o F› ‹τ o F›
using τ.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
horizontal_composite
by blast
interpret τ'oF: natural_transformation A C ‹K o F› ‹L o F› ‹τ' o F›
using τ'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
horizontal_composite
by blast
interpret τ'τ: vertical_composite B C H K L τ τ' ..
interpret τ'τoF: natural_transformation A C ‹H o F› ‹L o F› ‹τ'τ.map o F›
using τ'τ.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
horizontal_composite
by blast
interpret τ'oF_τoF: vertical_composite A C ‹H o F› ‹K o F› ‹L o F› ‹τ o F› ‹τ' o F› ..
show ?thesis
using τ'oF_τoF.map_def τ'τ.map_def τ'τoF.is_extensional by auto
qed
text‹
Horizontal composition of a vertical composite with a functor.
›
lemma whisker_left:
assumes "functor B C K"
and "natural_transformation A B F G τ" and "natural_transformation A B G H τ'"
shows "K o (vertical_composite.map A B τ τ') = vertical_composite.map A C (K o τ) (K o τ')"
proof -
interpret K: "functor" B C K using assms(1) by auto
interpret τ: natural_transformation A B F G τ using assms(2) by auto
interpret τ': natural_transformation A B G H τ' using assms(3) by auto
interpret τ'τ: vertical_composite A B F G H τ τ' ..
interpret Koτ: natural_transformation A C ‹K o F› ‹K o G› ‹K o τ›
using τ.natural_transformation_axioms K.as_nat_trans.natural_transformation_axioms
horizontal_composite
by blast
interpret Koτ': natural_transformation A C ‹K o G› ‹K o H› ‹K o τ'›
using τ'.natural_transformation_axioms K.as_nat_trans.natural_transformation_axioms
horizontal_composite
by blast
interpret Koτ'τ: natural_transformation A C ‹K o F› ‹K o H› ‹K o τ'τ.map›
using τ'τ.natural_transformation_axioms K.as_nat_trans.natural_transformation_axioms
horizontal_composite
by blast
interpret Koτ'_Koτ: vertical_composite A C ‹K o F› ‹K o G› ‹K o H› ‹K o τ› ‹K o τ'› ..
show "K o τ'τ.map = Koτ'_Koτ.map"
using Koτ'_Koτ.map_def τ'τ.map_def Koτ'τ.is_extensional Koτ'_Koτ.map_simp_1 τ'τ.map_simp_1
by auto
qed
text‹
The interchange law for horizontal and vertical composition.
›
lemma interchange:
assumes "natural_transformation B C F G τ" and "natural_transformation B C G H ν"
and "natural_transformation C D K L σ" and "natural_transformation C D L M μ"
shows "vertical_composite.map C D σ μ ∘ vertical_composite.map B C τ ν =
vertical_composite.map B D (σ ∘ τ) (μ ∘ ν)"
proof -
interpret τ: natural_transformation B C F G τ
using assms(1) by auto
interpret ν: natural_transformation B C G H ν
using assms(2) by auto
interpret σ: natural_transformation C D K L σ
using assms(3) by auto
interpret μ: natural_transformation C D L M μ
using assms(4) by auto
interpret ντ: vertical_composite B C F G H τ ν ..
interpret μσ: vertical_composite C D K L M σ μ ..
interpret σoτ: natural_transformation B D ‹K o F› ‹L o G› ‹σ o τ›
using σ.natural_transformation_axioms τ.natural_transformation_axioms
horizontal_composite
by blast
interpret μoν: natural_transformation B D ‹L o G› ‹M o H› ‹μ o ν›
using μ.natural_transformation_axioms ν.natural_transformation_axioms
horizontal_composite
by blast
interpret μσoντ: natural_transformation B D ‹K o F› ‹M o H› ‹μσ.map o ντ.map›
using μσ.natural_transformation_axioms ντ.natural_transformation_axioms
horizontal_composite
by blast
interpret μoν_σoτ: vertical_composite B D ‹K o F› ‹L o G› ‹M o H› ‹σ o τ› ‹μ o ν› ..
show "μσ.map o ντ.map = μoν_σoτ.map"
proof (intro eqI)
show "natural_transformation B D (K ∘ F) (M ∘ H) (μσ.map o ντ.map)" ..
show "natural_transformation B D (K ∘ F) (M ∘ H) μoν_σoτ.map" ..
show "⋀a. τ.A.ide a ⟹ (μσ.map o ντ.map) a = μoν_σoτ.map a"
proof -
fix a
assume a: "τ.A.ide a"
have "(μσ.map o ντ.map) a = D (μ (H a)) (σ (C (ν a) (τ a)))"
using a μσ.map_simp_1 ντ.map_simp_2 by simp
also have "... = D (μ (ν a)) (σ (τ a))"
using a
by (metis (full_types) μ.is_natural_1 μσ.map_simp_1 μσ.preserves_comp_1
ντ.map_seq ντ.map_simp_1 ντ.preserves_cod σ.B.comp_assoc τ.A.ide_char τ.B.seqE)
also have "... = μoν_σoτ.map a"
using a μoν_σoτ.map_simp_ide by simp
finally show "(μσ.map o ντ.map) a = μoν_σoτ.map a" by blast
qed
qed
qed
text‹
A special-case of the interchange law in which two of the natural transformations
are functors. It comes up reasonably often, and the reasoning is awkward.
›
lemma interchange_spc:
assumes "natural_transformation B C F G σ"
and "natural_transformation C D H K τ"
shows "τ ∘ σ = vertical_composite.map B D (H o σ) (τ o G)"
and "τ ∘ σ = vertical_composite.map B D (τ o F) (K o σ)"
proof -
show "τ ∘ σ = vertical_composite.map B D (H ∘ σ) (τ ∘ G)"
proof -
have "vertical_composite.map C D H τ ∘ vertical_composite.map B C σ G =
vertical_composite.map B D (H ∘ σ) (τ ∘ G)"
by (meson assms functor_is_transformation interchange natural_transformation.axioms(3-4))
thus ?thesis
using assms by force
qed
show "τ ∘ σ = vertical_composite.map B D (τ ∘ F) (K ∘ σ)"
proof -
have "vertical_composite.map C D τ K ∘ vertical_composite.map B C F σ =
vertical_composite.map B D (τ ∘ F) (K ∘ σ)"
by (meson assms functor_is_transformation interchange natural_transformation.axioms(3-4))
thus ?thesis
using assms by force
qed
qed
end