Proved B is finite #211
Proved B is finite #211
Conversation
|
Thanks a lot! This is great. I gave you a code review (edit: oops, but forgot to submit it -- I did this now) because I'm not sure I've seen you around before, but the code is fine; I was just showing you some tricks. You might want to consider upstreaming this result to mathlib -- I couldn't find it but I'm pretty sure that the experts there will know if it's there, and if it's not then I'm pretty sure they'll want it. |
| example : Module.Finite A B := by sorry -- I assume this is correct | ||
| example: Module.Finite A B := by | ||
| obtain ⟨ι, u, hi⟩ := FiniteDimensional.exists_is_basis_integral A K L | ||
| have: DecidableEq { x // x ∈ ι } := by exact Classical.typeDecidableEq { x // x ∈ ι } |
There was a problem hiding this comment.
| have: DecidableEq { x // x ∈ ι } := by exact Classical.typeDecidableEq { x // x ∈ ι } | |
| classical |
| obtain ⟨ι, u, hi⟩ := FiniteDimensional.exists_is_basis_integral A K L | ||
| have: DecidableEq { x // x ∈ ι } := by exact Classical.typeDecidableEq { x // x ∈ ι } | ||
| have h := integralClosure_le_span_dualBasis u hi | ||
| let V := (Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u))) |
There was a problem hiding this comment.
| let V := (Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u))) | |
| let V := (Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis | |
| (traceForm_nondegenerate K L) u))) |
I am surprised that we don't have a linter telling you that we would like to have all lines <= 100 chars (mathlib has one and I think it's a good idea)
| exact Set.finite_range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u) | ||
| have h3: Module.Finite A (integralClosure A L) := by | ||
| refine (@Module.Finite.iff_fg A L _ _ _ (Subalgebra.toSubmodule (integralClosure A L))).mpr ?_ | ||
| exact (@isNoetherian_submodule A L _ _ _ V).mp h2 (Subalgebra.toSubmodule (integralClosure A L)) h |
There was a problem hiding this comment.
| exact (@isNoetherian_submodule A L _ _ _ V).mp h2 (Subalgebra.toSubmodule (integralClosure A L)) h | |
| exact isNoetherian_submodule.mp h2 (Subalgebra.toSubmodule (integralClosure A L)) h |
You might have needed the @ when writing the code, but because it's an exact Lean can figure everything out.
| apply @Module.Finite.equiv A (integralClosure A L) B | ||
| exact AlgEquiv.toLinearEquiv (AlgEquiv.symm hb) |
There was a problem hiding this comment.
| apply @Module.Finite.equiv A (integralClosure A L) B | |
| exact AlgEquiv.toLinearEquiv (AlgEquiv.symm hb) | |
| exact Module.Finite.equiv <| AlgEquiv.toLinearEquiv (AlgEquiv.symm hb) |
Similarly here you don't need the @s as long as you tell Lean exactly what you're proving; unification can do the rest.
|
Thanks for the review! I looked through mathlib again, and I found that B is noetherian is already there, so the proof becomes trivial 😅 |
|
I submitted leanprover-community/mathlib4#18842 |
|
Thanks! Probably we should wait for that to get merged and bump mathlib and modify this PR to use it. |
|
Actually I just copied your mathlib PR into this repo :-) Many thanks for sorting this out! |
Proved
Module.Finite A BinBaseChange.leanCloses #202
Closes #202