feat(topology/sheaves/*): sheaves have enough injectives under some condition

[jjaassoonn]

• [x] define skyscraper sheaves
• [x] skyscraper sheaves are isomorphic to pullback of a sheaf on the single point space (not actually needed for enough invectiveness, just for completeness)
• [x] calculate their stalks
• [x] skyscraper sheaves are injective if targets are injective
• [x] godement resolution
• [x] show enough injective

---

• [x] depends on:#15932
• [x] depends on:#15496
• [x] depends on:#15934
• [x] depends on:#15935
• [x] depends on:#16180

[jjaassoonn]

This PR originally started as defining skyscraper sheaf, but now too many things has been added, so I will move the definition of skyscraper sheaf into another branch (#15934).

[alreadydone]

Are there plans to merge master and port this PR to Lean 4? It's listed as the first item in @joelriou 's AIM workshop statement.