feat(Topology): First singular homology group of the Hawaiian earring - #485
feat(Topology): First singular homology group of the Hawaiian earring#485vlad902 wants to merge 1 commit into
Conversation
vlad902
changed the title
|
I'm not convinced this is hard enough for inclusion. I want to raise the median difficulty of the problem set: too many are being solved! Only if you're interested, but could you give me an estimate of how hard you think this will be? |
|
So my interest in this is that I have tried to work a bit with homology in Lean and found it fairly difficult and I suspect that AI models are also going to struggle. I think getting the isomorphism is several papers worth of calculations, but I think there is a huge mass of missing theory to get there (that should eventually be in mathlib one day.) Perhaps that's below the current bar, feel free to close! |
|
|
||
| /-- The direct sum `⊕ i : ℕ, ℤ` embedded in the product `∏ i : ℕ, ℤ`. -/ | ||
| noncomputable abbrev directSum : AddSubgroup (ℕ → ℤ) := | ||
| (Finsupp.coeFnAddHom (ι := ℕ) (M := ℤ)).range |
There was a problem hiding this comment.
a small trick
| (Finsupp.coeFnAddHom (ι := ℕ) (M := ℤ)).range | |
| Finsupp.coeFnAddHom (ι := ℕ) (M := ℤ).range |
| @[eval_problem] | ||
| theorem hawaiian_earring_first_singularHomology_isomorphism : | ||
| Nonempty ((singularHomologyFunctor Ab 1 |>.obj (.of ℤ) |>.obj <| .of HawaiianEarring) ≃+ | ||
| (ℕ → ℤ) × ((ℕ → ℤ) ⧸ directSum)) := by |
There was a problem hiding this comment.
If this work you can just remove the abbrev directSum
| (ℕ → ℤ) × ((ℕ → ℤ) ⧸ directSum)) := by | |
| (ℕ → ℤ) × ((ℕ → ℤ) ⧸ Finsupp.coeFnAddHom.range)) := by |
3 participants
The first singular homology group of the Hawaiian earring is isomorphic to
(∏ i : ℕ, ℤ) × (∏ i : ℕ, ℤ / ⊕ i : ℕ, ℤ).First draft by Aristotle, then significantly edited.