Reduced Scheme Structure on closed subsets

Stream: Is there code for X?

[Alessandro D'Angelo]

Hi all! I wonder if there's already in mathlib4 code for the fact that we have a unique reduced scheme structure on closed subset of a scheme. I've formalised it (@ https://github.com/ADA-Projects/Lean-AG/blob/main/GWchap5/IrredClosedSubscheme.lean), but maybe there are already existing pieces of this.

Also since I'm quite new to Lean, if you spot missed refactoring opportunities, please do tell! It's also the first time I deal with formalising results "up to iso", so if there are conceptual mistakes let me know.

[Andrew Yang]

Hello! Great to see another algebraic geometry contributor. Given a (X : Scheme) (Z : Closeds X), the reduced scheme structure should be (vanishingIdeal Z).subscheme (you don't need to take the radical) and we are indeed missing the fact that this is reduced.

[Andrew Yang]

In general you should use [IsClosedImmersion f] instead of (hf_closed : IsClosedImmersion f) so that the type class machinery can work in your favour.

[Alessandro D'Angelo]

yeah, sorry I didn't carefully check what the LLM generated. I'll fix the definition removing the nonsense radical. Also great advice about the square brackets! Thanks!