# Theory Homology_Groups

section‹Homology, II: Homology Groups›

theory Homology_Groups
imports Simplices "HOL-Algebra.Exact_Sequence"

begin
subsection‹Homology Groups›

text‹Now actually connect to group theory and set up homology groups. Note that we define homomogy
groups for all \emph{integers} @{term p}, since this seems to avoid some special-case reasoning,
though they are trivial for @{term"p < 0"}.›

definition chain_group :: "nat ⇒ 'a topology ⇒ 'a chain monoid"
where "chain_group p X ≡ free_Abelian_group (singular_simplex_set p X)"

lemma carrier_chain_group [simp]: "carrier(chain_group p X) = singular_chain_set p X"
by (auto simp: chain_group_def singular_chain_def free_Abelian_group_def)

lemma one_chain_group [simp]: "one(chain_group p X) = 0"
by (auto simp: chain_group_def free_Abelian_group_def)

lemma mult_chain_group [simp]: "monoid.mult(chain_group p X) = (+)"
by (auto simp: chain_group_def free_Abelian_group_def)

lemma m_inv_chain_group [simp]: "Poly_Mapping.keys a ⊆ singular_simplex_set p X ⟹ inv⇘chain_group p X⇙ a = -a"
unfolding chain_group_def by simp

lemma group_chain_group [simp]: "Group.group (chain_group p X)"

lemma abelian_chain_group: "comm_group(chain_group p X)"
by (simp add: free_Abelian_group_def group.group_comm_groupI [OF group_chain_group])

lemma subgroup_singular_relcycle:
"subgroup (singular_relcycle_set p X S) (chain_group p X)"
proof
show "x ⊗⇘chain_group p X⇙ y ∈ singular_relcycle_set p X S"
if "x ∈ singular_relcycle_set p X S" and "y ∈ singular_relcycle_set p X S" for x y
next
show "inv⇘chain_group p X⇙ x ∈ singular_relcycle_set p X S"
if "x ∈ singular_relcycle_set p X S" for x
using that
by clarsimp (metis m_inv_chain_group singular_chain_def singular_relcycle singular_relcycle_minus)
qed (auto simp: singular_relcycle)

definition relcycle_group :: "nat ⇒ 'a topology ⇒ 'a set ⇒ ('a chain) monoid"
where "relcycle_group p X S ≡
subgroup_generated (chain_group p X) (Collect(singular_relcycle p X S))"

lemma carrier_relcycle_group [simp]:
"carrier (relcycle_group p X S) = singular_relcycle_set p X S"
proof -
have "carrier (chain_group p X) ∩ singular_relcycle_set p X S = singular_relcycle_set p X S"
using subgroup.subset subgroup_singular_relcycle by blast
moreover have "generate (chain_group p X) (singular_relcycle_set p X S) ⊆ singular_relcycle_set p X S"
by (simp add: group.generate_subgroup_incl group_chain_group subgroup_singular_relcycle)
ultimately show ?thesis
by (auto simp: relcycle_group_def subgroup_generated_def generate.incl)
qed

lemma one_relcycle_group [simp]: "one(relcycle_group p X S) = 0"

lemma mult_relcycle_group [simp]: "(⊗⇘relcycle_group p X S⇙) = (+)"

lemma abelian_relcycle_group [simp]:
"comm_group(relcycle_group p X S)"
unfolding relcycle_group_def
by (intro group.abelian_subgroup_generated group_chain_group) (auto simp: abelian_chain_group singular_relcycle)

lemma group_relcycle_group [simp]: "group(relcycle_group p X S)"

lemma relcycle_group_restrict [simp]:
"relcycle_group p X (topspace X ∩ S) = relcycle_group p X S"
by (metis relcycle_group_def singular_relcycle_restrict)

definition relative_homology_group :: "int ⇒ 'a topology ⇒ 'a set ⇒ ('a chain) set monoid"
where
"relative_homology_group p X S ≡
if p < 0 then singleton_group undefined else
(relcycle_group (nat p) X S) Mod (singular_relboundary_set (nat p) X S)"

abbreviation homology_group
where "homology_group p X ≡ relative_homology_group p X {}"

lemma relative_homology_group_restrict [simp]:
"relative_homology_group p X (topspace X ∩ S) = relative_homology_group p X S"

lemma nontrivial_relative_homology_group:
fixes p::nat
shows "relative_homology_group p X S
= relcycle_group p X S Mod singular_relboundary_set p X S"

lemma singular_relboundary_ss:
"singular_relboundary p X S x ⟹ Poly_Mapping.keys x ⊆ singular_simplex_set p X"
using singular_chain_def singular_relboundary_imp_chain by blast

lemma trivial_relative_homology_group [simp]:
"p < 0 ⟹ trivial_group(relative_homology_group p X S)"

lemma subgroup_singular_relboundary:
"subgroup (singular_relboundary_set p X S) (chain_group p X)"
unfolding chain_group_def
proof unfold_locales
show "singular_relboundary_set p X S
⊆ carrier (free_Abelian_group (singular_simplex_set p X))"
using singular_chain_def singular_relboundary_imp_chain by fastforce
next
fix x
assume "x ∈ singular_relboundary_set p X S"
then show "inv⇘free_Abelian_group (singular_simplex_set p X)⇙ x
∈ singular_relboundary_set p X S"

lemma subgroup_singular_relboundary_relcycle:
"subgroup (singular_relboundary_set p X S) (relcycle_group p X S)"
unfolding relcycle_group_def
by (simp add: Collect_mono group.subgroup_of_subgroup_generated singular_relboundary_imp_relcycle subgroup_singular_relboundary)

lemma normal_subgroup_singular_relboundary_relcycle:
"(singular_relboundary_set p X S) ⊲ (relcycle_group p X S)"

lemma group_relative_homology_group [simp]:
"group (relative_homology_group p X S)"
normal_subgroup_singular_relboundary_relcycle)

lemma right_coset_singular_relboundary:
"r_coset (relcycle_group p X S) (singular_relboundary_set p X S)
= (λa. {b. homologous_rel p X S a b})"
using singular_relboundary_minus
by (force simp: r_coset_def homologous_rel_def relcycle_group_def subgroup_generated_def)

lemma carrier_relative_homology_group:
"carrier(relative_homology_group (int p) X S)
= (homologous_rel_set p X S)  singular_relcycle_set p X S"
by (auto simp: set_eq_iff image_iff relative_homology_group_def FactGroup_def RCOSETS_def right_coset_singular_relboundary)

lemma carrier_relative_homology_group_0:
"carrier(relative_homology_group 0 X S)
= (homologous_rel_set 0 X S)  singular_relcycle_set 0 X S"
using carrier_relative_homology_group [of 0 X S] by simp

lemma one_relative_homology_group [simp]:
"one(relative_homology_group (int p) X S) = singular_relboundary_set p X S"

lemma mult_relative_homology_group:
"(⊗⇘relative_homology_group (int p) X S⇙) = (λR S. (⋃r∈R. ⋃s∈S. {r + s}))"
unfolding relcycle_group_def subgroup_generated_def chain_group_def free_Abelian_group_def set_mult_def relative_homology_group_def FactGroup_def
by force

lemma inv_relative_homology_group:
assumes "R ∈ carrier (relative_homology_group (int p) X S)"
shows "m_inv(relative_homology_group (int p) X S) R = uminus  R"
proof (rule group.inv_equality [OF group_relative_homology_group _ assms])
obtain c where c: "R = homologous_rel_set p X S c" "singular_relcycle p X S c"
using assms by (auto simp: carrier_relative_homology_group)
have "singular_relboundary p X S (b - a)"
if "a ∈ R" and "b ∈ R" for a b
using c that
by clarify (metis homologous_rel_def homologous_rel_eq)
moreover
have "x ∈ (⋃x∈R. ⋃y∈R. {y - x})"
if "singular_relboundary p X S x" for x
using c
by simp (metis diff_eq_eq homologous_rel_def homologous_rel_refl homologous_rel_sym that)
ultimately
have "(⋃x∈R. ⋃xa∈R. {xa - x}) = singular_relboundary_set p X S"
by auto
then show "uminus  R ⊗⇘relative_homology_group (int p) X S⇙ R =
𝟭⇘relative_homology_group (int p) X S⇙"
by (auto simp: carrier_relative_homology_group mult_relative_homology_group)
have "singular_relcycle p X S (-c)"
using c by (simp add: singular_relcycle_minus)
moreover have "homologous_rel p X S c x ⟹ homologous_rel p X S (-c) (- x)" for x
by (metis homologous_rel_def homologous_rel_sym minus_diff_eq minus_diff_minus)
moreover have "homologous_rel p X S (-c) x ⟹ x ∈ uminus  homologous_rel_set p X S c" for x
by (clarsimp simp: image_iff) (metis add.inverse_inverse diff_0 homologous_rel_diff homologous_rel_refl)
ultimately show "uminus  R ∈ carrier (relative_homology_group (int p) X S)"
using c by (auto simp: carrier_relative_homology_group)
qed

lemma homologous_rel_eq_relboundary:
"homologous_rel p X S c = singular_relboundary p X S
⟷ singular_relboundary p X S c" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding homologous_rel_def
by (metis diff_zero singular_relboundary_0)
next
assume R: ?rhs
show ?lhs
unfolding homologous_rel_def
using singular_relboundary_diff R by fastforce
qed

lemma homologous_rel_set_eq_relboundary:
"homologous_rel_set p X S c = singular_relboundary_set p X S ⟷ singular_relboundary p X S c"
by (auto simp flip: homologous_rel_eq_relboundary)

text‹Lift the boundary and induced maps to homology groups. We totalize both
quite aggressively to the appropriate group identity in all "undefined"
situations, which makes several of the properties cleaner and simpler.›

lemma homomorphism_chain_boundary:
"chain_boundary p ∈ hom (relcycle_group p X S) (relcycle_group(p - Suc 0) (subtopology X S) {})"
(is "?h ∈ hom ?G ?H")
proof (rule homI)
show "⋀x. x ∈ carrier ?G ⟹ ?h x  ∈ carrier ?H"
by (auto simp: singular_relcycle_def mod_subset_def chain_boundary_boundary)

lemma hom_boundary1:
"∃d. ∀p X S.
d p X S ∈ hom (relative_homology_group (int p) X S)
(homology_group (int (p - Suc 0)) (subtopology X S))
∧ (∀c. singular_relcycle p X S c
⟶ d p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c))"
(is "∃d. ∀p X S. ?Φ (d p X S) p X S")
proof ((subst choice_iff [symmetric])+, clarify)
fix p X and S :: "'a set"
define θ where "θ ≡ r_coset (relcycle_group(p - Suc 0) (subtopology X S) {})
(singular_relboundary_set (p - Suc 0) (subtopology X S) {}) ∘ chain_boundary p"
define H where "H ≡ relative_homology_group (int (p - Suc 0)) (subtopology X S) {}"
define J where "J ≡ relcycle_group (p - Suc 0) (subtopology X S) {}"

have θ: "θ ∈ hom (relcycle_group p X S) H"
unfolding θ_def
proof (rule hom_compose)
show "chain_boundary p ∈ hom (relcycle_group p X S) J"
show "(#>⇘relcycle_group (p - Suc 0) (subtopology X S) {}⇙)
(singular_relboundary_set (p - Suc 0) (subtopology X S) {}) ∈ hom J H"
by (simp add: H_def J_def nontrivial_relative_homology_group
normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle)
qed
have *: "singular_relboundary (p - Suc 0) (subtopology X S) {} (chain_boundary p c)"
if "singular_relboundary p X S c" for c
proof (cases "p=0")
case True
then show ?thesis
by (metis chain_boundary_def singular_relboundary_0)
next
case False
with that have "∃d. singular_chain p (subtopology X S) d ∧ chain_boundary p d = chain_boundary p c"
with that False show ?thesis
by (auto simp: singular_boundary)
qed
have θ_eq: "θ x = θ y"
if x: "x ∈ singular_relcycle_set p X S" and y: "y ∈ singular_relcycle_set p X S"
and eq: "singular_relboundary_set p X S #>⇘relcycle_group p X S⇙ x
= singular_relboundary_set p X S #>⇘relcycle_group p X S⇙ y" for x y
proof -
have "singular_relboundary p X S (x-y)"
by (metis eq homologous_rel_def homologous_rel_eq mem_Collect_eq right_coset_singular_relboundary)
with * have "(singular_relboundary (p - Suc 0) (subtopology X S) {}) (chain_boundary p (x-y))"
by blast
then show ?thesis
unfolding θ_def comp_def
by (metis chain_boundary_diff homologous_rel_def homologous_rel_eq right_coset_singular_relboundary)
qed
obtain d
where "d ∈ hom ((relcycle_group p X S) Mod (singular_relboundary_set p X S)) H"
and d: "⋀u. u ∈ singular_relcycle_set p X S ⟹ d (homologous_rel_set p X S u) = θ u"
by (metis FactGroup_universal [OF θ normal_subgroup_singular_relboundary_relcycle θ_eq] right_coset_singular_relboundary carrier_relcycle_group)
then have "d ∈ hom (relative_homology_group p X S) H"
then show  "∃d. ?Φ d p X S"
by (force simp: H_def right_coset_singular_relboundary d θ_def)
qed

lemma hom_boundary2:
"∃d. (∀p X S.
(d p X S) ∈ hom (relative_homology_group p X S)
(homology_group (p-1) (subtopology X S)))
∧ (∀p X S c. singular_relcycle p X S c ∧ Suc 0 ≤ p
⟶ d p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c))"
(is "∃d. ?Φ d")
proof -
have *: "∃f. Φ(λp. if p ≤ 0 then λq r t. undefined else f(nat p)) ⟹ ∃f. Φ f"  for Φ
by blast
show ?thesis
apply (rule * [OF ex_forward [OF hom_boundary1]])
apply (simp add: not_le relative_homology_group_def nat_diff_distrib' int_eq_iff nat_diff_distrib flip: nat_1)
qed

lemma hom_boundary3:
"∃d. ((∀p X S c. c ∉ carrier(relative_homology_group p X S)
⟶ d p X S c = one(homology_group (p-1) (subtopology X S))) ∧
(∀p X S.
d p X S ∈ hom (relative_homology_group p X S)
(homology_group (p-1) (subtopology X S))) ∧
(∀p X S c.
singular_relcycle p X S c ∧ 1 ≤ p
⟶ d p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)) ∧
(∀p X S. d p X S = d p X (topspace X ∩ S))) ∧
(∀p X S c. d p X S c ∈ carrier(homology_group (p-1) (subtopology X S))) ∧
(∀p. p ≤ 0 ⟶ d p = (λq r t. undefined))"
(is "∃x. ?P x ∧ ?Q x ∧ ?R x")
proof -
have "⋀x. ?Q x ⟹ ?R x"
by (erule all_forward) (force simp: relative_homology_group_def)
moreover have "∃x. ?P x ∧ ?Q x"
proof -
obtain d:: "[int, 'a topology, 'a set, ('a chain) set] ⇒ ('a chain) set"
where 1: "⋀p X S. d p X S ∈ hom (relative_homology_group p X S)
(homology_group (p-1) (subtopology X S))"
and 2: "⋀n X S c. singular_relcycle n X S c ∧ Suc 0 ≤ n
⟹ d n X S (homologous_rel_set n X S c)
= homologous_rel_set (n - Suc 0) (subtopology X S) {} (chain_boundary n c)"
using hom_boundary2 by blast
have 4: "c ∈ carrier (relative_homology_group p X S) ⟹
d p X (topspace X ∩ S) c ∈ carrier (relative_homology_group (p-1) (subtopology X S) {})"
for p X S c
using hom_carrier [OF 1 [of p X "topspace X ∩ S"]]
show ?thesis
apply (rule_tac x="λp X S c.
if c ∈ carrier(relative_homology_group p X S)
then d p X (topspace X ∩ S) c
else one(homology_group (p-1) (subtopology X S))" in exI)
apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
group.is_monoid group.restrict_hom_iff 4 cong: if_cong)
by (metis "1" "2" homologous_rel_restrict relative_homology_group_restrict singular_relcycle_def subtopology_restrict)
qed
ultimately show ?thesis
by auto
qed

consts hom_boundary :: "[int,'a topology,'a set,'a chain set] ⇒ 'a chain set"
specification (hom_boundary)
hom_boundary:
"((∀p X S c. c ∉ carrier(relative_homology_group p X S)
⟶ hom_boundary p X S c = one(homology_group (p-1) (subtopology X (S::'a set)))) ∧
(∀p X S.
hom_boundary p X S ∈ hom (relative_homology_group p X S)
(homology_group (p-1) (subtopology X (S::'a set)))) ∧
(∀p X S c.
singular_relcycle p X S c ∧ 1 ≤ p
⟶ hom_boundary p X S (homologous_rel_set p X S c)
= homologous_rel_set (p - Suc 0) (subtopology X (S::'a set)) {} (chain_boundary p c)) ∧
(∀p X S. hom_boundary p X S = hom_boundary p X (topspace X ∩ (S::'a set)))) ∧
(∀p X S c. hom_boundary p X S c ∈ carrier(homology_group (p-1) (subtopology X (S::'a set)))) ∧
(∀p. p ≤ 0 ⟶ hom_boundary p = (λq r. λt::'a chain set. undefined))"
by (fact hom_boundary3)

lemma hom_boundary_default:
"c ∉ carrier(relative_homology_group p X S)
⟹ hom_boundary p X S c = one(homology_group (p-1) (subtopology X S))"
and hom_boundary_hom: "hom_boundary p X S ∈ hom (relative_homology_group p X S) (homology_group (p-1) (subtopology X S))"
and hom_boundary_restrict [simp]: "hom_boundary p X (topspace X ∩ S) = hom_boundary p X S"
and hom_boundary_carrier: "hom_boundary p X S c ∈ carrier(homology_group (p-1) (subtopology X S))"
and hom_boundary_trivial: "p ≤ 0 ⟹ hom_boundary p = (λq r t. undefined)"
by (metis hom_boundary)+

lemma hom_boundary_chain_boundary:
"⟦singular_relcycle p X S c; 1 ≤ p⟧
⟹ hom_boundary (int p) X S (homologous_rel_set p X S c) =
homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)"
by (metis hom_boundary)+

lemma hom_chain_map:
"⟦continuous_map X Y f; f  S ⊆ T⟧
⟹ (chain_map p f) ∈ hom (relcycle_group p X S) (relcycle_group p Y T)"
by (force simp: chain_map_add singular_relcycle_chain_map hom_def)

lemma hom_induced1:
"∃hom_relmap.
(∀p X S Y T f.
continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T
⟶ (hom_relmap p X S Y T f) ∈ hom (relative_homology_group (int p) X S)
(relative_homology_group (int p) Y T)) ∧
(∀p X S Y T f c.
continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧
singular_relcycle p X S c
⟶ hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c))"
proof -
have "∃y. (y ∈ hom (relative_homology_group (int p) X S) (relative_homology_group (int p) Y T)) ∧
(∀c. singular_relcycle p X S c ⟶
y (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c))"
if contf: "continuous_map X Y f" and fim: "f  (topspace X ∩ S) ⊆ T"
for p X S Y T and f :: "'a ⇒ 'b"
proof -
let ?f = "(#>⇘relcycle_group p Y T⇙) (singular_relboundary_set p Y T) ∘ chain_map p f"
let ?F = "λx. singular_relboundary_set p X S #>⇘relcycle_group p X S⇙ x"
have "chain_map p f ∈ hom (relcycle_group p X S) (relcycle_group p Y T)"
by (metis contf fim hom_chain_map relcycle_group_restrict)
then have 1: "?f ∈ hom (relcycle_group p X S) (relative_homology_group (int p) Y T)"
by (simp add: hom_compose normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle relative_homology_group_def)
have 2: "singular_relboundary_set p X S ⊲ relcycle_group p X S"
using normal_subgroup_singular_relboundary_relcycle by blast
have 3: "?f x = ?f y"
if "singular_relcycle p X S x" "singular_relcycle p X S y" "?F x = ?F y" for x y
proof -
have "homologous_rel p X S x y"
by (metis (no_types) homologous_rel_set_eq right_coset_singular_relboundary that(3))
then have "singular_relboundary p Y T (chain_map p f (x - y))"
using  singular_relboundary_chain_map [OF _ contf fim] by (simp add: homologous_rel_def)
then have "singular_relboundary p Y T (chain_map p f x - chain_map p f y)"
with that
show ?thesis
by (metis comp_apply homologous_rel_def homologous_rel_set_eq right_coset_singular_relboundary)
qed
obtain g where "g ∈ hom (relcycle_group p X S Mod singular_relboundary_set p X S)
(relative_homology_group (int p) Y T)"
"⋀x. x ∈ singular_relcycle_set p X S ⟹ g (?F x) = ?f x"
using FactGroup_universal [OF 1 2 3, unfolded carrier_relcycle_group] by blast
then show ?thesis
by (force simp: right_coset_singular_relboundary nontrivial_relative_homology_group)
qed
then show ?thesis
apply (simp flip: all_conj_distrib)
apply ((subst choice_iff [symmetric])+)
apply metis
done
qed

lemma hom_induced2:
"∃hom_relmap.
(∀p X S Y T f.
continuous_map X Y f ∧
f  (topspace X ∩ S) ⊆ T
⟶ (hom_relmap p X S Y T f) ∈ hom (relative_homology_group p X S)
(relative_homology_group p Y T)) ∧
(∀p X S Y T f c.
continuous_map X Y f ∧
f  (topspace X ∩ S) ⊆ T ∧
singular_relcycle p X S c
⟶ hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) ∧
(∀p. p < 0 ⟶ hom_relmap p = (λX S Y T f c. undefined))"
(is "∃d. ?Φ d")
proof -
have *: "∃f. Φ(λp. if p < 0 then λX S Y T f c. undefined else f(nat p)) ⟹ ∃f. Φ f"  for Φ
by blast
show ?thesis
apply (rule * [OF ex_forward [OF hom_induced1]])
apply (simp add: not_le relative_homology_group_def nat_diff_distrib' int_eq_iff nat_diff_distrib flip: nat_1)
done
qed

lemma hom_induced3:
"∃hom_relmap.
((∀p X S Y T f c.
~(continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧
c ∈ carrier(relative_homology_group p X S))
⟶ hom_relmap p X S Y T f c = one(relative_homology_group p Y T)) ∧
(∀p X S Y T f.
hom_relmap p X S Y T f ∈ hom (relative_homology_group p X S) (relative_homology_group p Y T)) ∧
(∀p X S Y T f c.
continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧ singular_relcycle p X S c
⟶ hom_relmap p X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) ∧
(∀p X S Y T.
hom_relmap p X S Y T =
hom_relmap p X (topspace X ∩ S) Y (topspace Y ∩ T))) ∧
(∀p X S Y f T c.
hom_relmap p X S Y T f c ∈ carrier(relative_homology_group p Y T)) ∧
(∀p. p < 0 ⟶ hom_relmap p = (λX S Y T f c. undefined))"
(is "∃x. ?P x ∧ ?Q x ∧ ?R x")
proof -
have "⋀x. ?Q x ⟹ ?R x"
by (erule all_forward) (fastforce simp: relative_homology_group_def)
moreover have "∃x. ?P x ∧ ?Q x"
proof -
obtain hom_relmap:: "[int,'a topology,'a set,'b topology,'b set,'a ⇒ 'b,('a chain) set] ⇒ ('b chain) set"
where 1: "⋀p X S Y T f. ⟦continuous_map X Y f; f  (topspace X ∩ S) ⊆ T⟧ ⟹
hom_relmap p X S Y T f
∈ hom (relative_homology_group p X S) (relative_homology_group p Y T)"
and 2: "⋀p X S Y T f c.
⟦continuous_map X Y f; f  (topspace X ∩ S) ⊆ T; singular_relcycle p X S c⟧
⟹
hom_relmap (int p) X S Y T f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)"
and 3: "(∀p. p < 0 ⟶ hom_relmap p = (λX S Y T f c. undefined))"
using hom_induced2 [where ?'a='a and ?'b='b]
by (metis (mono_tags, lifting))
have 4: "⟦continuous_map X Y f; f  (topspace X ∩ S) ⊆ T; c ∈ carrier (relative_homology_group p X S)⟧ ⟹
hom_relmap p X (topspace X ∩ S) Y (topspace Y ∩ T) f c
∈ carrier (relative_homology_group p Y T)"
for p X S Y f T c
using hom_carrier [OF 1 [of X Y f "topspace X ∩ S" "topspace Y ∩ T" p]]
continuous_map_image_subset_topspace by fastforce
have inhom: "(λc. if continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧
c ∈ carrier (relative_homology_group p X S)
then hom_relmap p X (topspace X ∩ S) Y (topspace Y ∩ T) f c
else 𝟭⇘relative_homology_group p Y T⇙)
∈ hom (relative_homology_group p X S) (relative_homology_group p Y T)" (is "?h ∈ hom ?GX ?GY")
for p X S Y T f
proof (rule homI)
show "⋀x. x ∈ carrier ?GX ⟹ ?h x ∈ carrier ?GY"
by (auto simp: 4 group.is_monoid)
show "?h (x ⊗⇘?GX⇙ y) = ?h x ⊗⇘?GY⇙?h y" if "x ∈ carrier ?GX" "y ∈ carrier ?GX" for x y
proof (cases "p < 0")
case True
with that show ?thesis
by (simp add: relative_homology_group_def singleton_group_def 3)
next
case False
show ?thesis
proof (cases "continuous_map X Y f")
case True
then have "f  (topspace X ∩ S) ⊆ topspace Y"
using continuous_map_image_subset_topspace by blast
then show ?thesis
using True False that
using 1 [of X Y f "topspace X ∩ S" "topspace Y ∩ T" p]
by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
qed
qed
have hrel: "⟦continuous_map X Y f; f  (topspace X ∩ S) ⊆ T; singular_relcycle p X S c⟧
⟹ hom_relmap (int p) X (topspace X ∩ S) Y (topspace Y ∩ T)
f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
for p X S Y T f c
using 2 [of X Y f "topspace X ∩ S" "topspace Y ∩ T" p c]
continuous_map_image_subset_topspace by fastforce
show ?thesis
apply (rule_tac x="λp X S Y T f c.
if continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧
c ∈ carrier(relative_homology_group p X S)
then hom_relmap p X (topspace X ∩ S) Y (topspace Y ∩ T) f c
else one(relative_homology_group p Y T)" in exI)
apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
group.is_monoid group.restrict_hom_iff 4 inhom hrel cong: if_cong)
apply (force simp: continuous_map_def intro!: ext)
done
qed
ultimately show ?thesis
by auto
qed

consts hom_induced:: "[int,'a topology,'a set,'b topology,'b set,'a ⇒ 'b,('a chain) set] ⇒ ('b chain) set"
specification (hom_induced)
hom_induced:
"((∀p X S Y T f c.
~(continuous_map X Y f ∧
f  (topspace X ∩ S) ⊆ T ∧
c ∈ carrier(relative_homology_group p X S))
⟶ hom_induced p X (S::'a set) Y (T::'b set) f c =
one(relative_homology_group p Y T)) ∧
(∀p X S Y T f.
(hom_induced p X (S::'a set) Y (T::'b set) f) ∈ hom (relative_homology_group p X S)
(relative_homology_group p Y T)) ∧
(∀p X S Y T f c.
continuous_map X Y f ∧
f  (topspace X ∩ S) ⊆ T ∧
singular_relcycle p X S c
⟶ hom_induced p X (S::'a set) Y (T::'b set) f (homologous_rel_set p X S c) =
homologous_rel_set p Y T (chain_map p f c)) ∧
(∀p X S Y T.
hom_induced p X (S::'a set) Y (T::'b set) =
hom_induced p X (topspace X ∩ S) Y (topspace Y ∩ T))) ∧
(∀p X S Y f T c.
hom_induced p X (S::'a set) Y (T::'b set) f c ∈
carrier(relative_homology_group p Y T)) ∧
(∀p. p < 0 ⟶ hom_induced p = (λX S Y T. λf::'a⇒'b. λc. undefined))"
by (fact hom_induced3)

lemma hom_induced_default:
"~(continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧ c ∈ carrier(relative_homology_group p X S))
⟹ hom_induced p X S Y T f c = one(relative_homology_group p Y T)"
and hom_induced_hom:
"hom_induced p X S Y T f ∈ hom (relative_homology_group p X S) (relative_homology_group p Y T)"
and hom_induced_restrict [simp]:
"hom_induced p X (topspace X ∩ S) Y (topspace Y ∩ T) = hom_induced p X S Y T"
and hom_induced_carrier:
"hom_induced p X S Y T f c ∈ carrier(relative_homology_group p Y T)"
and hom_induced_trivial: "p < 0 ⟹ hom_induced p = (λX S Y T f c. undefined)"
by (metis hom_induced)+

lemma hom_induced_chain_map_gen:
"⟦continuous_map X Y f; f  (topspace X ∩ S) ⊆ T; singular_relcycle p X S c⟧
⟹ hom_induced p X S Y T f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
by (metis hom_induced)

lemma hom_induced_chain_map:
"⟦continuous_map X Y f; f  S ⊆ T; singular_relcycle p X S c⟧
⟹ hom_induced p X S Y T f (homologous_rel_set p X S c)
= homologous_rel_set p Y T (chain_map p f c)"
by (meson Int_lower2 hom_induced image_subsetI image_subset_iff subset_iff)

lemma hom_induced_eq:
assumes "⋀x. x ∈ topspace X ⟹ f x = g x"
shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof -
consider "p < 0" | n where "p = int n"
by (metis int_nat_eq not_less)
then show ?thesis
proof cases
case 1
then show ?thesis
next
case 2
have "hom_induced n X S Y T f C = hom_induced n X S Y T g C" for C
proof -
have "continuous_map X Y f ∧ f  (topspace X ∩ S) ⊆ T ∧ C ∈ carrier (relative_homology_group n X S)
⟷ continuous_map X Y g ∧ g  (topspace X ∩ S) ⊆ T ∧ C ∈ carrier (relative_homology_group n X S)"
(is "?P = ?Q")
by (metis IntD1 assms continuous_map_eq image_cong)
then consider "¬ ?P ∧ ¬ ?Q" | "?P ∧ ?Q"
by blast
then show ?thesis
proof cases
case 1
then show ?thesis
next
case 2
have "homologous_rel_set n Y T (chain_map n f c) = homologous_rel_set n Y T (chain_map n g c)"
if "continuous_map X Y f" "f  (topspace X ∩ S) ⊆ T"
"continuous_map X Y g" "g  (topspace X ∩ S) ⊆ T"
"C = homologous_rel_set n X S c" "singular_relcycle n X S c"
for c
proof -
have "chain_map n f c = chain_map n g c"
using assms chain_map_eq singular_relcycle that by blast
then show ?thesis
by simp
qed
with 2 show ?thesis
by (auto simp: relative_homology_group_def carrier_FactGroup
right_coset_singular_relboundary hom_induced_chain_map_gen)
qed
qed
with 2 show ?thesis
by auto
qed
qed

subsection‹Towards the Eilenberg-Steenrod axioms›

text‹First prove we get functors into abelian groups with the boundary map
being a natural transformation between them, and prove Eilenberg-Steenrod
axioms (we also prove additivity a bit later on if one counts that). ›
(*1. Exact sequence from the inclusions and boundary map
H_{p+1} X --(j')⤏ H_{p+1}X (A) --(d')⤏ H_p A --(i')⤏ H_p X
2. Dimension axiom: H_p X is trivial for one-point X and p =/= 0
3. Homotopy invariance of the induced map
4. Excision: inclusion (X - U,A - U) --(i')⤏ X (A) induces an isomorphism
when cl U ⊆ int A*)

lemma abelian_relative_homology_group [simp]:
"comm_group(relative_homology_group p X S)"
by (simp add: comm_group.abelian_FactGroup relative_homology_group_def subgroup_singular_relboundary_relcycle)

lemma abelian_homology_group: "comm_group(homology_group p X)"
by simp

lemma hom_induced_id_gen:
assumes contf: "continuous_map X X f" and feq: "⋀x. x ∈ topspace X ⟹ f x = x"
and c: "c ∈ carrier (relative_homology_group p X S)"
shows "hom_induced p X S X S f c = c"
proof -
consider "p < 0" | n where "p = int n"
by (metis int_nat_eq not_less)
then show ?thesis
proof cases
case 1
with c show ?thesis
next
case 2
have cm: "chain_map n f d = d" if "singular_relcycle n X S d" for d
using that assms by (auto simp: chain_map_id_gen singular_relcycle)
have "f  (topspace X ∩ S) ⊆ S"
using feq by auto
with 2 c show ?thesis
by (auto simp: nontrivial_relative_homology_group carrier_FactGroup
cm right_coset_singular_relboundary hom_induced_chain_map_gen assms)
qed
qed

lemma hom_induced_id:
"c ∈ carrier (relative_homology_group p X S) ⟹ hom_induced p X S X S id c = c"
by (rule hom_induced_id_gen) auto

lemma hom_induced_compose:
assumes "continuous_map X Y f" "f  S ⊆ T" "continuous_map Y Z g" "g  T ⊆ U"
shows "hom_induced p X S Z U (g ∘ f) = hom_induced p Y T Z U g ∘ hom_induced p X S Y T f"
proof -
consider (neg) "p < 0" | (int) n where "p = int n"
by (metis int_nat_eq not_less)
then show ?thesis
proof cases
case int
have gf: "continuous_map X Z (g ∘ f)"
using assms continuous_map_compose by fastforce
have gfim: "(g ∘ f)  S ⊆ U"
unfolding o_def using assms by blast
have sr: "⋀a. singular_relcycle n X S a ⟹ singular_relcycle n Y T (chain_map n f a)"
show ?thesis
proof
fix c
show "hom_induced p X S Z U (g ∘ f) c = (hom_induced p Y T Z U g ∘ hom_induced p X S Y T f) c"
proof (cases "c ∈ carrier(relative_homology_group p X S)")
case True
with gfim show ?thesis
unfolding int
by (auto simp: carrier_relative_homology_group gf gfim assms sr chain_map_compose  hom_induced_chain_map)
next
case False
then show ?thesis
by (simp add: hom_induced_default hom_one [OF hom_induced_hom])
qed
qed
qed (force simp: hom_induced_trivial)
qed

lemma hom_induced_compose':
assumes "continuous_map X Y f" "f  S ⊆ T" "continuous_map Y Z g" "g  T ⊆ U"
shows "hom_induced p Y T Z U g (hom_induced p X S Y T f x) = hom_induced p X S Z U (g ∘ f) x"
using hom_induced_compose [OF assms] by simp

lemma naturality_hom_induced:
assumes "continuous_map X Y f" "f  S ⊆ T"
shows "hom_boundary q Y T ∘ hom_induced q X S Y T f
= hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f ∘ hom_boundary q X S"
proof (cases "q ≤ 0")
case False
then obtain p where p1: "p ≥ Suc 0" and q: "q = int p"
using zero_le_imp_eq_int by force
show ?thesis
proof
fix c
show "(hom_boundary q Y T ∘ hom_induced q X S Y T f) c =
(hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f ∘ hom_boundary q X S) c"
proof (cases "c ∈ carrier(relative_homology_group p X S)")
case True
then obtain a where ceq: "c = homologous_rel_set p X S a" and a: "singular_relcycle p X S a"
by (force simp: carrier_relative_homology_group)
then have sr: "singular_relcycle p Y T (chain_map p f a)"
using assms singular_relcycle_chain_map by fastforce
then have sb: "singular_relcycle (p - Suc 0) (subtopology X S) {} (chain_boundary p a)"
by (metis One_nat_def a chain_boundary_boundary singular_chain_0 singular_relcycle)
have p1_eq: "int p - 1 = int (p - Suc 0)"
using p1 by auto
have cbm: "(chain_boundary p (chain_map p f a))
= (chain_map (p - Suc 0) f (chain_boundary p a))"
using a chain_boundary_chain_map singular_relcycle by blast
have contf: "continuous_map (subtopology X S) (subtopology Y T) f"
using assms
by (auto simp: continuous_map_in_subtopology topspace_subtopology
continuous_map_from_subtopology)
show ?thesis
unfolding q using assms p1 a
by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr)
next
case False
with assms show ?thesis
unfolding q o_def using assms
by (metis group_relative_homology_group hom_boundary hom_induced hom_one one_relative_homology_group)
qed
qed
qed (force simp: hom_induced_trivial hom_boundary_trivial)

lemma homology_exactness_axiom_1:
"exact_seq ([homology_group (p-1) (subtopology X S), relative_homology_group p X S, homology_group p X],
[hom_boundary p X S,hom_induced p X {} X S id])"
proof -
consider (neg) "p < 0" | (int) n where "p = int n"
by (metis int_nat_eq not_less)
then have "(hom_induced p X {} X S id)  carrier (homology_group p X)
= kernel (relative_homology_group p X S) (homology_group (p-1) (subtopology X S))
(hom_boundary p X S)"
proof cases
case neg
then show ?thesis
unfolding kernel_def singleton_group_def relative_homology_group_def
by (auto simp: hom_induced_trivial hom_boundary_trivial)
next
case int
have "hom_induced (int m) X {} X S id  carrier (relative_homology_group (int m) X {})
= carrier (relative_homology_group (int m) X S) ∩
{c. hom_boundary (int m) X S c = 𝟭⇘relative_homology_group (int m - 1) (subtopology X S) {}⇙}" for m
proof (cases m)
case 0
have "hom_induced 0 X {} X S id  carrier (relative_homology_group 0 X {})
= carrier (relative_homology_group 0 X S)"   (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
using hom_induced_hom [of 0 X "{}" X S id]
show "?rhs ⊆ ?lhs"
apply (clarsimp simp add: image_iff carrier_relative_homology_group [of 0, simplified] singular_relcycle)
apply (force simp: chain_map_id_gen chain_boundary_def singular_relcycle
hom_induced_chain_map [of concl: 0, simplified])
done
qed
with 0 show ?thesis
by (simp add: hom_boundary_trivial relative_homology_group_def [of "-1"] singleton_group_def)
next
case (Suc n)
have "(hom_induced (int (Suc n)) X {} X S id ∘
homologous_rel_set (Suc n) X {})  singular_relcycle_set (Suc n) X {}
= homologous_rel_set (Suc n) X S 
(singular_relcycle_set (Suc n) X S ∩
{c. hom_boundary (int (Suc n)) X S (homologous_rel_set (Suc n) X S c)
= singular_relboundary_set n (subtopology X S) {}})"
(is "?lhs = ?rhs")
proof -
have 1: "(⋀x. x ∈ A ⟹ x ∈ B ⟷ x ∈ C) ⟹ f  (A ∩ B) = f  (A ∩ C)" for f A B C
by blast
have 2: "⟦⋀x. x ∈ A ⟹ ∃y. y ∈ B ∧ f x = f y; ⋀x. x ∈ B ⟹ ∃y. y ∈ A ∧ f x = f y⟧
⟹ f  A = f  B" for f A B
by blast
have "?lhs = homologous_rel_set (Suc n) X S  singular_relcycle_set (Suc n) X {}"
using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle
by (smt (verit) bot.extremum comp_apply continuous_map_id image_cong image_empty mem_Collect_eq)
also have "… = homologous_rel_set (Suc n) X S 
(singular_relcycle_set (Suc n) X S ∩
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)})"
proof (rule 2)
fix c
assume "c ∈ singular_relcycle_set (Suc n) X {}"
then show "∃y. y ∈ singular_relcycle_set (Suc n) X S ∩
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)} ∧
homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
using singular_cycle singular_relcycle by (fastforce simp: singular_boundary)
next
fix c
assume c: "c ∈ singular_relcycle_set (Suc n) X S ∩
{c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)}"
then obtain d where d: "singular_chain (Suc n) (subtopology X S) d"
"chain_boundary (Suc n) d = chain_boundary (Suc n) c"
by (auto simp: singular_boundary)
with c have "c - d ∈ singular_relcycle_set (Suc n) X {}"
by (auto simp: singular_cycle chain_boundary_diff singular_chain_subtopology singular_relcycle singular_chain_diff)
moreover have "homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S (c - d)"
show "homologous_rel (Suc n) X S c (c - d)"
using d by (simp add: homologous_rel_def singular_chain_imp_relboundary)
qed
ultimately show "∃y. y ∈ singular_relcycle_set (Suc n) X {} ∧
homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
by blast
qed
also have "… = ?rhs"
by (rule 1) (simp add: hom_boundary_chain_boundary homologous_rel_set_eq_relboundary del: of_nat_Suc)
finally show "?lhs = ?rhs" .
qed
with Suc show ?thesis
unfolding carrier_relative_homology_group image_comp id_def by auto
qed
then show ?thesis
by (auto simp: kernel_def int)
qed
then show ?thesis
using hom_boundary_hom hom_induced_hom
by (force simp: group_hom_def group_hom_axioms_def)
qed

lemma homology_exactness_axiom_2:
"exact_seq ([homology_group (p-1) X, homology_group (p-1) (subtopology X S), relative_homology_group p X S],
[hom_induced (p-1) (subtopology X S) {} X {} id, hom_boundary p X S])"
proof -
consider (neg) "p ≤ 0" | (int) n where "p = int (Suc n)"
by (metis linear not0_implies_Suc of_nat_0 zero_le_imp_eq_int)
then have "kernel (relative_homology_group (p-1) (subtopology X S) {})
(relative_homology_group (p-1) X {})
(hom_induced (p-1) (subtopology X S) {} X {} id)
= hom_boundary p X S  carrier (relative_homology_group p X S)"
proof cases
case neg
obtain x where "x ∈ carrier (relative_homology_group p X S)"
using group_relative_homology_group group.is_monoid by blast
with neg show ?thesis
unfolding kernel_def singleton_group_def relative_homology_group_def
by (force simp: hom_induced_trivial hom_boundary_trivial)
next
case int
have "hom_boundary (int (Suc n)) X S  carrier (relative_homology_group (int (Suc n)) X S)
= carrier (relative_homology_group n (subtopology X S) {}) ∩
{c. hom_induced n (subtopology X S) {} X {} id c =
𝟭⇘relative_homology_group n X {}⇙}"
(is "?lhs = ?rhs")
proof -
have 1: "(⋀x. x ∈ A ⟹ x ∈ B ⟷ x ∈ C) ⟹ f  (A ∩ B) = f  (A ∩ C)" for f A B C
by blast
have 2: "(⋀x. x ∈ A ⟹ x ∈ B ⟷ x ∈ f - C) ⟹ f  (A ∩ B) = f  A ∩ C" for f A B C
by blast
have "?lhs = homologous_rel_set n (subtopology X S) {}
 (chain_boundary (Suc n)  singular_relcycle_set (Suc n) X S)"
unfolding carrier_relative_homology_group image_comp
by (rule image_cong [OF refl]) (simp add: o_def hom_boundary_chain_boundary del: of_nat_Suc)
also have "… = homologous_rel_set n (subtopology X S) {} 
(singular_relcycle_set n (subtopology X S) {} ∩ singular_relboundary_set n X {})"
by (force simp: singular_relcycle singular_boundary chain_boundary_boundary_alt)
also have "… = ?rhs"
unfolding carrier_relative_homology_group vimage_def
by (intro 2) (auto simp: hom_induced_chain_map chain_map_ident homologous_rel_set_eq_relboundary singular_relcycle)
finally show ?thesis .
qed
then show ?thesis
by (auto simp: kernel_def int)
qed
then show ?thesis
using hom_boundary_hom hom_induced_hom
by (force simp: group_hom_def group_hom_axioms_def)
qed

lemma homology_exactness_axiom_3:
"exact_seq ([relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)],
[hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])"
proof (cases "p < 0")
case True
then show ?thesis
unfolding relative_homology_group_def
by (simp add: group_hom.kernel_to_trivial_group group_hom_axioms_def group_hom_def hom_induced_trivial)
next
case False
then obtain n where peq: "p = int n"
by (metis int_ops(1) linorder_neqE_linordered_idom pos_int_cases)
have "hom_induced n (subtopology X S) {} X {} id
(homologous_rel_set n (subtopology X S) {} 
singular_relcycle_set n (subtopology X S) {})
= {c ∈ homologous_rel_set n X {}  singular_relcycle_set n X {}.
hom_induced n X {} X S id c = singular_relboundary_set n X S}"
(is "?lhs = ?rhs")
proof -
have 2: "⟦⋀x. x ∈ A ⟹ ∃y. y ∈ B ∧ f x = f y; ⋀x. x ∈ B ⟹ ∃y. y ∈ A ∧ f x = f y⟧
⟹ f  A = f  B" for f A B
by blast
have "?lhs = homologous_rel_set n X {}  (singular_relcycle_set n (subtopology X S) {})"
by (smt (verit) chain_map_ident continuous_map_id_subt empty_subsetI hom_induced_chain_map image_cong image_empty image_image mem_Collect_eq singular_relcycle)
also have "… = homologous_rel_set n X {}  (singular_relcycle_set n X {} ∩ singular_relboundary_set n X S)"
proof (rule 2)
fix c
assume "c ∈ singular_relcycle_set n (subtopology X S) {}"
then show "∃y. y ∈ singular_relcycle_set n X {} ∩ singular_relboundary_set n X S ∧
homologous_rel_set n X {} c = homologous_rel_set n X {} y"
using singular_chain_imp_relboundary singular_cycle singular_relboundary_imp_chain singular_relcycle by fastforce
next
fix c
assume "c ∈ singular_relcycle_set n X {} ∩ singular_relboundary_set n X S"
then obtain d e where c: "singular_relcycle n X {} c" "singular_relboundary n X S c"
and d:  "singular_chain n (subtopology X S) d"
and e: "singular_chain (Suc n) X e" "chain_boundary (Suc n) e = c + d"
using singular_relboundary_alt by blast
then have "chain_boundary n (c + d) = 0"
using chain_boundary_boundary_alt by fastforce
then have "chain_boundary n c + chain_boundary n d = 0"
with c have "singular_relcycle n (subtopology X S) {} (- d)"
by (metis (no_types) d eq_add_iff singular_cycle singular_relcycle_minus)
moreover have "homologous_rel n X {} c (- d)"
using c
by (metis diff_minus_eq_add e homologous_rel_def singular_boundary)
ultimately
show "∃y. y ∈ singular_relcycle_set n (subtopology X S) {} ∧
homologous_rel_set n X {} c = homologous_rel_set n X {} y"
by (force simp: homologous_rel_set_eq)
qed
also have "… = homologous_rel_set n X {} 
(singular_relcycle_set n X {} ∩ homologous_rel_set n X {} - {x. hom_induced n X {} X S id x = singular_relboundary_set n X S})"
by (rule 2) (auto simp: hom_induced_chain_map homologous_rel_set_eq_relboundary chain_map_ident [of _ X] singular_cycle cong: conj_cong)
also have "… = ?rhs"
by blast
finally show ?thesis .
qed
then have "kernel (relative_homology_group p X {}) (relative_homology_group p X S) (hom_induced p X {} X S id)
= hom_induced p (subtopology X S) {} X {} id  carrier (relative_homology_group p (subtopology X S) {})"
by (simp add: kernel_def carrier_relative_homology_group peq)
then show ?thesis
by (simp add: not_less group_hom_def group_hom_axioms_def hom_induced_hom)
qed

lemma homology_dimension_axiom:
assumes X: "topspace X = {a}" and "p ≠ 0"
shows "trivial_group(homology_group p X)"
proof (cases "p < 0")
case True
then show ?thesis
by simp
next
case False
then obtain n where peq: "p = int n" "n > 0"
by (metis assms(2) neq0_conv nonneg_int_cases not_less of_nat_0)
have "homologous_rel_set n X {}  singular_relcycle_set n X {} = {singular_relcycle_set n X {}}"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
using peq assms
by (auto simp: image_subset_iff homologous_rel_set_eq_relboundary simp flip: singular_boundary_set_eq_cycle_singleton)
have "singular_relboundary n X {} 0"
by simp
with peq assms
show "?rhs ⊆ ?lhs"
by (auto simp: image_iff simp flip: homologous_rel_eq_relboundary singular_boundary_set_eq_cycle_singleton)
qed
with peq assms show ?thesis
unfolding trivial_group_def
by (simp add:  carrier_relative_homology_group singular_boundary_set_eq_cycle_singleton [OF X])
qed

proposition homology_homotopy_axiom:
assumes "homotopic_with (λh. h  S ⊆ T) X Y f g"
shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof (cases "p < 0")
case True
then show ?thesis
next
case False
then obtain n where peq: "p = int n"
by (metis int_nat_eq not_le)
have cont: "continuous_map X Y f" "continuous_map X Y g"
using assms homotopic_with_imp_continuous_maps by blast+
have im: "f  (topspace X ∩ S) ⊆ T" "g  (topspace X ∩ S) ⊆ T"
using homotopic_with_imp_property assms by blast+
show ?thesis
proof
fix c show "hom_induced p X S Y T f c = hom_induced p X S Y T g c"
proof (cases "c ∈ carrier(relative_homology_group p X S)")
case True
then obtain a where a: "c = homologous_rel_set n X S a" "singular_relcycle n X S a"
unfolding carrier_relative_homology_group peq by auto
with assms homotopic_imp_homologous_rel_chain_maps show ?thesis
by (force simp add: peq hom_induced_chain_map_gen cont im homologous_rel_set_eq)
qed
qed

proposition homology_excision_axiom:
assumes "X closure_of U ⊆ X interior_of T" "T ⊆ S"
shows
"hom_induced p (subtopology X (S - U)) (T - U) (subtopology X S) T id
∈ iso (relative_homology_group p (subtopology X (S - U)) (T - U))
(relative_homology_group p (subtopology X S) T)"
proof (cases "p < 0")
case True
then show ?thesis
unfolding iso_def bij_betw_def relative_homology_group_def by (simp add: hom_induced_trivial)
next
case False
then obtain n where peq: "p = int n"
by (metis int_nat_eq not_le)
have cont: "continuous_map (subtopology X (S - U)) (subtopology X S) id"
have TU: "topspace X ∩ (S - U) ∩ (T - U) ⊆ T"
by auto
show ?thesis
proof (simp add: iso_def peq carrier_relative_homology_group bij_betw_def hom_induced_hom, intro conjI)
show "inj_on (hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id)
(homologous_rel_set n (subtopology X (S - U)) (T - U)
singular_relcycle_set n (subtopology X (S - U)) (T - U))"
unfolding inj_on_def
fix c d
assume c: "singular_relcycle n (subtopology X (S - U)) (T - U) c"
and d: "singular_relcycle n (subtopology X (S - U)) (T - U) d"
and hh: "hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
(homologous_rel_set n (subtopology X (S - U)) (T - U) c)
= hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
(homologous_rel_set n (subtopology X (S - U)) (T - U) d)"
then have scc: "singular_chain n (subtopology X (S - U)) c"
and  scd: "singular_chain n (subtopology X (S - U)) d"
using singular_relcycle by blast+
have "singular_relboundary n (subtopology X (S - U)) (T - U) c"
if srb: "singular_relboundary n (subtopology X S) T c"
and src: "singular_relcycle n (subtopology X (S - U)) (T - U) c" for c
proof -
have [simp]: "(S - U) ∩ (T - U) = T - U" "S ∩ T = T"
using ‹T ⊆ S› by blast+
have c: "singular_chain n (subtopology X (S - U)) c"
"singular_chain (n - Suc 0) (subtopology X (T - U)) (chain_boundary n c)"
using that by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology)
obtain d e where d: "singular_chain (Suc n) (subtopology X S) d"
and e: "singular_chain n (subtopology X T) e"
and dce: "chain_boundary (Suc n) d = c + e"
using srb by (auto simp: singular_relboundary_alt subtopology_subtopology)
obtain m f g where f: "singular_chain (Suc n) (subtopology X (S - U)) f"
and g: "singular_chain (Suc n) (subtopology X T) g"
and dfg: "(singular_subdivision (Suc n) ^^ m) d = f + g"
using excised_chain_exists [OF assms d] .
obtain h where
h0:  "⋀p. h p 0 = (0 :: 'a chain)"
and hdiff: "⋀p c1 c2. h p (c1-c2) = h p c1 - h p c2"
and hSuc: "⋀p X c. singular_chain p X c ⟹ singular_chain (Suc p) X (h p c)"
and hchain: "⋀p X c. singular_chain p X c
⟹ chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
= (singular_subdivision p ^^ m) c - c"
using chain_homotopic_iterated_singular_subdivision by blast
have hadd: "⋀p c1 c2. h p (c1 + c2) = h p c1 + h p c2"
define c1 where "c1 ≡ f - h n c"
define c2 where "c2 ≡ chain_boundary (Suc n) (h n e) - (chain_boundary (Suc n) g - e)"
show ?thesis
unfolding singular_relboundary_alt
proof (intro exI conjI)
show c1: "singular_chain (Suc n) (subtopology X (S - U)) c1"
by (simp add: ‹singular_chain n (subtopology X (S - U)) c› c1_def f hSuc singular_chain_diff)
have "chain_boundary (Suc n) (chain_boundary (Suc (Suc n)) (h (Suc n) d) + h n (c+e))
= chain_boundary (Suc n) (f + g - d)"
using hchain [OF d] by (simp add: dce dfg)
then have "chain_boundary (Suc n) (h n (c + e))
= chain_boundary (Suc n) f + chain_boundary (Suc n) g - (c + e)"
using chain_boundary_boundary_alt [of "Suc n" "subtopology X S"]
then have "chain_boundary (Suc n) (h n c) + chain_boundary (Suc n) (h n e)
= chain_boundary (Suc n) f + chain_boundary (Suc n) g - (c + e)"
then have *: "chain_boundary (Suc n) (f - h n c) = c + (chain_boundary (Suc n) (h n e) - (chain_boundary (Suc n) g - e))"
then show "chain_boundary (Suc n) c1 = c + c2"
unfolding c1_def c2_def
obtain "singular_chain n (subtopology X (S - U)) c2" "singular_chain n (subtopology X T) c2"
using singular_chain_diff c c1 *
unfolding c1_def c2_def
by (metis add_diff_cancel_left' e g hSuc singular_chain_boundary_alt)
then show "singular_chain n (subtopology (subtopology X (S - U)) (T - U)) c2"
qed
qed
then have "singular_relboundary n (subtopology X S) T (c - d) ⟹
singular_relboundary n (subtopology X (S - U)) (T - U) (c - d)"
using c d singular_relcycle_diff by metis
with hh show "homologous_rel n (subtopology X (S - U)) (T - U) c d"
apply (simp add: hom_induced_chain_map cont c d chain_map_ident [OF scc] chain_map_ident [OF scd])
using homologous_rel_set_eq homologous_rel_def by metis
qed
next
have h: "homologous_rel_set n (subtopology X S) T a
∈ (λx. homologous_rel_set n (subtopology X S) T (chain_map n id x)) 
singular_relcycle_set n (subtopology X (S - U)) (T - U)"
if a: "singular_relcycle n (subtopology X S) T a" for a
proof -
obtain c' where c': "singular_relcycle n (subtopology X (S - U)) (T - U) c'"
"homologous_rel n (subtopology X S) T a c'"
using a by (blast intro: excised_relcycle_exists [OF assms])
then have scc': "singular_chain n (subtopology X S) c'"
using homologous_rel_singular_chain singular_relcycle that by blast
then show ?thesis
using scc' chain_map_ident [of _ "subtopology X S"] c' homologous_rel_set_eq
by fastforce
qed
have "(λx. homologous_rel_set n (subtopology X S) T (chain_map n id x))
singular_relcycle_set n (subtopology X (S - U)) (T - U) =
homologous_rel_set n (subtopology X S) T 
singular_relcycle_set n (subtopology X S) T"
by (force simp: cont h singular_relcycle_chain_map)
then
show "hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
homologous_rel_set n (subtopology X (S - U)) (T - U) 
singular_relcycle_set n (subtopology X (S - U)) (T - U)
= homologous_rel_set n (subtopology X S) T  singular_relcycle_set n (subtopology X S) T"
by (simp add: image_comp o_def hom_induced_chain_map_gen cont TU topspace_subtopology
cong: image_cong_simp)
qed
qed

text‹Not in the original Eilenberg-Steenrod list but usually included nowadays,
following Milnor's "On Axiomatic Homology Theory".›

lemma iso_chain_group_sum:
assumes disj: "pairwise disjnt 𝒰" and UU: "⋃𝒰 = topspace X"
and subs: "⋀C T. ⟦compactin X C; path_connectedin X C; T ∈ 𝒰; ~ disjnt C T⟧ ⟹ C ⊆ T"
shows "(λf. sum' f 𝒰) ∈ iso (sum_group 𝒰 (λS. chain_group p (subtopology X S))) (chain_group p X)"
proof -
have pw: "pairwise (λi j. disjnt (singular_simplex_set p (subtopology X i))
(singular_simplex_set p (subtopology X j))) 𝒰"
proof
fix S T
assume "S ∈ 𝒰" "T ∈ 𝒰" "S ≠ T"
then show "disjnt (singular_simplex_set p (subtopology X S))
(singular_simplex_set p (subtopology X T))"
using nonempty_standard_simplex [of p] disj
by (fastforce simp: pairwise_def disjnt_def singular_simplex_subtopology image_subset_iff)
qed
have "∃S∈𝒰. singular_simplex p (subtopology X S) f"
if f: "singular_simplex p X f" for f
proof -
obtain x where x: "x ∈ topspace X" "x ∈ f  standard_simplex p"
using f nonempty_standard_simplex [of p] continuous_map_image_subset_topspace
unfolding singular_simplex_def by fastforce
then obtain S where "S ∈ 𝒰" "x ∈ S"
using UU by auto
have "f  standard_simplex p ⊆ S"
proof (rule subs)
have cont: "continuous_map (subtopology (powertop_real UNIV)
(standard_simplex p)) X f"
using f singular_simplex_def by auto
show "compactin X (f  standard_simplex p)"
by (simp add: compactin_subtopology compactin_standard_simplex image_compactin [OF _ cont])
show "path_connectedin X (f  standard_simplex p)"
by (simp add: path_connectedin_subtopology path_connectedin_standard_simplex path_connectedin_continuous_map_image [OF cont])
have "standard_simplex p ≠ {}"
then
show "¬ disjnt (f  standard_simplex p) S"
using x ‹x ∈ S› by (auto simp: disjnt_def)
qed (auto simp: ‹S ∈ 𝒰›)
then show ?thesis
by (meson ‹S ∈ 𝒰› singular_simplex_subtopology that)
qed
then have "(⋃i∈𝒰. singular_simplex_set p (subtopology X i)) = singular_simplex_set p X"
by (auto simp: singular_simplex_subtopology)
then show ?thesis
using iso_free_Abelian_group_sum [OF pw] by (simp add: chain_group_def)
qed

lemma relcycle_group_0_eq_chain_group: "relcycle_group 0 X {} = chain_group 0 X"
proof (rule monoid.equality)
show "carrier (relcycle_group 0 X {}) = carrier (chain_group 0 X)"
by (simp add: Collect_mono chain_boundary_def singular_cycle subset_antisym)

proposition iso_cycle_group_sum:
assumes disj: "pairwise disjnt 𝒰" and UU: "⋃𝒰 = topspace X"
and subs: "⋀C T. ⟦compactin X C; path_connectedin X C; T ∈ 𝒰; ¬ disjnt C T⟧ ⟹ C ⊆ T"
shows "(λf. sum' f 𝒰) ∈ iso (sum_group 𝒰 (λT. relcycle_group p (subtopology X T) {}))
(relcycle_group p X {})"
proof (cases "p = 0")
case True
then show ?thesis
by (simp add: relcycle_group_0_eq_chain_group iso_chain_group_sum [OF assms])
next
case False
let ?SG = "(sum_group 𝒰 (λT. chain_group p (subtopology X T)))"
let ?PI = "(Π⇩E T∈𝒰. singular_relcycle_set p (subtopology X T) {})"
have "(λf. sum' f 𝒰) ∈ Group.iso (subgroup_generated ?SG (carrier ?SG ∩ ?PI))
(subgroup_generated (chain_group p X) (singular_relcycle_set p X {}))"
proof (rule group_hom.iso_between_subgroups)
have iso: "(λf. sum' f 𝒰) ∈ Group.iso ?SG (chain_group p X)"
by (auto simp: assms iso_chain_group_sum)
then show "group_hom ?SG (chain_group p X) (λf. sum' f 𝒰)"
by (auto simp: iso_imp_homomorphism group_hom_def group_hom_axioms_def)
have B: "sum' f 𝒰 ∈ singular_relcycle_set p X {} ⟷ f ∈ (carrier ?SG ∩ ?PI)"
if "f ∈ (carrier ?SG)" for f
proof -
have f: "⋀S. S ∈ 𝒰 ⟶ singular_chain p (subtopology X S) (f S)"
"f ∈ extensional 𝒰" "finite {i ∈ 𝒰. f i ≠ 0}"
using that by (auto simp: carrier_sum_group PiE_def Pi_def)
then have rfin: "finite {S ∈ 𝒰. restrict (chain_boundary p ∘ f) 𝒰 S ≠ 0}"
by (auto elim: rev_finite_subset)
have "chain_boundary p ((∑x | x ∈ 𝒰 ∧ f x ≠ 0. f x)) = 0
⟷ (∀S ∈ 𝒰. chain_boundary p (f S) = 0)" (is "?cb = 0 ⟷ ?rhs")
proof
assume "?cb = 0"
moreover have "?cb = sum' (λS. chain_boundary p (f S)) 𝒰"
unfolding sum.G_def using rfin f
by (force simp: chain_boundary_sum intro: sum.mono_neutral_right cong: conj_cong)
ultimately have eq0: "sum' (λS. chain_boundary p (f S)) 𝒰 = 0"
by simp
have "(λf. sum' f 𝒰) ∈ hom (sum_group 𝒰 (λS. chain_group (p - Suc 0) (subtopology X S)))
(chain_group (p - Suc 0) X)"
and inj: "inj_on (λf. sum' f 𝒰) (carrier (sum_group 𝒰 (λS. chain_group (p - Suc 0) (subtopology X S))))"
using iso_chain_group_sum [OF assms, of "p-1"] by (auto simp: iso_def bij_betw_def)
then have eq: "⟦f ∈ (Π⇩E i∈𝒰. singular_chain_set (p - Suc 0) (subtopology X i));
finite {S ∈ 𝒰. f S ≠ 0}; sum' f 𝒰 = 0; S ∈ 𝒰⟧ ⟹ f S = 0" for f S
apply (simp add: group_hom_def group_hom_axioms_def group_hom.inj_on_one_iff [of _ "chain_group (p-1) X"])
apply (auto simp: carrier_sum_group fun_eq_iff that)
done
show ?rhs
proof clarify
fix S assume "S ∈ 𝒰"
then show "chain_boundary p (f S) = 0"
using eq [of "restrict (chain_boundary p ∘ f) 𝒰" S] rfin f eq0
by (simp add: singular_chain_boundary cong: conj_cong)
qed
next
assume ?rhs
then show "?cb = 0"
by (force simp: chain_boundary_sum intro: sum.mono_neutral_right)
qed
moreover
have "(⋀S. S ∈ 𝒰 ⟶ singular_chain p (subtopology X S) (f S))
⟹ singular_chain p X (∑x | x ∈ 𝒰 ∧ f x ≠ 0. f x)"
by (metis (no_types, lifting) mem_Collect_eq singular_chain_subtopology singular_chain_sum)
ultimately show ?thesis
using f by (auto simp: carrier_sum_group sum.G_def singular_cycle PiE_iff)
qed
have "singular_relcycle_set p X {} ⊆ carrier (chain_group p X)"
using subgroup.subset subgroup_singular_relcycle by blast
then show "(λf. sum' f 𝒰)  (carrier ?SG ∩ ?PI) = singular_relcycle_set p X {}"
using iso B unfolding Group.iso_def
by (smt (verit, del_insts) Int_iff bij_betw_def image_iff mem_Collect_eq subset_antisym subset_iff)
qed (auto simp: assms iso_chain_group_sum)
then show ?thesis
by (simp add: relcycle_group_def sum_group_subgroup_generated subgroup_singular_relcycle)
qed

assumes disj: "pairwise disjnt 𝒰" and UU: "⋃𝒰 = topspace X"
and subs: "⋀C T. ⟦compactin X C; path_connectedin X C; T ∈ 𝒰; ¬ disjnt C T⟧ ⟹ C ⊆ T"
shows "(λx. gfinprod (homology_group p X)
(λV. hom_induced p (subtopology X V) {} X {} id (x V)) 𝒰)
∈ iso (sum_group 𝒰 (λS. homology_group p (subtopology X S))) (homology_group p X)"
(is  "?h ∈ iso ?SG ?HG")
proof (cases "p < 0")
case True
then have [simp]: "gfinprod (singleton_group undefined) (λv. undefined) 𝒰 = undefined"
by (metis Pi_I carrier_singleton_group comm_group_def comm_monoid.gfinprod_closed singletonD singleton_abelian_group)
show ?thesis
using True
apply (simp add: iso_def relative_homology_group_def hom_induced_trivial carrier_sum_group)
apply (auto simp: singleton_group_def bij_betw_def inj_on_def fun_eq_iff)
done
next
case False
then obtain n where peq: "p = int n"
by (metis int_ops(1) linorder_neqE_linordered_idom pos_int_cases)
interpret comm_group "homology_group p X"
by (rule abelian_homology_group)
show ?thesis
proof (simp add: iso_def bij_betw_def, intro conjI)
show "?h ∈ hom ?SG ?HG"
by (rule hom_group_sum) (simp_all add: hom_induced_hom)
then interpret group_hom ?SG ?HG ?h
have carrSG: "carrier ?SG
= (λx. λS∈𝒰. homologous_rel_set n (subtopology X S) {} (x S))
 (carrier (sum_group 𝒰 (λS. relcycle_group n (subtopology X S) {})))" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
proof (clarsimp simp: carrier_sum_group carrier_relative_homology_group peq)
fix z
assume z: "z ∈ (Π⇩E S∈𝒰. homologous_rel_set n (subtopology X S) {}  singular_relcycle_set n (subtopology X S) {})"
and fin: "finite {S ∈ 𝒰. z S ≠ singular_relboundary_set n (subtopology X S) {}}"
then obtain c where c: "∀S∈𝒰. singular_relcycle n (subtopology X S) {} (c S)
∧ z S = homologous_rel_set n (subtopology X S) {} (c S)"
by (simp add: PiE_def Pi_def image_def) metis
let ?f = "λS∈𝒰. if singular_relboundary n (subtopology X S) {} (c S) then 0 else c S"
have "z = (λS∈𝒰. homologous_rel_set n (subtopology X S) {} (?f S))"
by (smt (verit) PiE_restrict c homologous_rel_eq_relboundary restrict_apply restrict_ext singular_relboundary_0 z)
moreover have "?f ∈ (Π⇩E i∈𝒰. singular_relcycle_set n (subtopology X i) {})"
by (simp add: c fun_eq_iff PiE_arb [OF z])
moreover have "finite {i ∈ 𝒰. ?f i ≠ 0}"
using z c  by (intro finite_subset [OF _ fin]) auto
ultimately
show "z ∈ (λx. λS∈𝒰. homologous_rel_set n (subtopology X S) {} (x S)) 
{x ∈ Π⇩E i∈𝒰. singular_relcycle_set n (subtopology X i) {}. finite {i ∈ 𝒰. x i ≠ 0}}"
by blast
qed
show "?rhs ⊆ ?lhs"
by (force simp: peq carrier_sum_group carrier_relative_homology_group homologous_rel_set_eq_relboundary
elim: rev_finite_subset)
qed
have gf: "gfinprod (homology_group p X)
(λV. hom_induced n (subtopology X V) {} X {} id
((λS∈𝒰. homologous_rel_set n