Implementation of base change

Stream: lean4

[Tammo Brinner]

Hello!
I am a master student in mathematics and plan to write my master thesis about the implementation of a topic of my choice in lean4. I was wondering whether it would be feasible to implement a theorem like base change in lean4 (the sheaves in topology version). I have been reading up on sheaves in lean4 and i feel like it would be managable but i am also not an expert in lean4 so i was wondering if someone has an idea whether this is doable or not. Thank you in advance!

[Henrik Böving]

I think you might find more relevant eyes in #mathlib4 as this sounds like it would require quite a bit of mathlib theory upfront

[Tammo Brinner]

Henrik Böving schrieb:

I think you might find more relevant eyes in #mathlib4 as this sounds like it would require quite a bit of mathlib theory upfront

Ahh maybe you are right, i will post it there again, thanks!