feat(Algebra/Bijective): a weakly étale bijective-on-residue-fields local hom is an isomorphism#170
Open
chrisflav wants to merge 2 commits into
Conversation
…ocal hom is an isomorphism Fill three sorries in `Proetale/Algebra/Bijective.lean`: * `Algebra.bijective_comap_lmul'_of_bijective_of_bijective` * `Algebra.bijective_of_bijective_of_flat` * `Algebra.WeaklyEtale.bijective_algebraMap_of_bijective_residueFieldMap` These prove that for a weakly étale local homomorphism of local rings that is bijective on prime spectra with trivial residue field extensions, the multiplication map `S ⊗[R] S → S` is bijective on spectra, a flat surjective spectrum-bijective map is an isomorphism, and consequently such a local map is itself an isomorphism. Adds the corresponding proof-level `\leanok`s in the blueprint. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
added
awaiting-auto-review
Reconcile blueprint with the formalised proofs and extract reusable facts:
- Remove the dead scaffolding sorry-lemmas
`isLocalRing_tensorProduct_of_krullDimLE_zero` and
`krullDimLE_zero_tensorProduct_of_krullDimLE_zero` (and the orphaned
`lem:local-dim-zero-tensor` blueprint lemma), as the direct
section/residue-field proof does not use the field-reduction strategy.
- Rewrite the blueprint proof of
`lem:bij-on-spectrum-of-unique-lying-over-and-residue-field-eq` to the direct
argument actually formalised and drop `\uses{lem:local-dim-zero-tensor}`.
- Rewrite the blueprint proof of
`lem:isom-of-unique-lying-over-and-residue-field-eq` to the descent argument
actually formalised and drop `\uses{lem:isom-of-ff-and-mul-isom}`.
- Extract `PrimeSpectrum.comap_injective_of_comp_eq_id` (comap of a hom with a
section is injective) and `Function.bijective_of_leftInverse_of_bijective`
(a left inverse of a bijection is bijective), used in place of the inlined
arguments.
- Style: `haveI` -> `have`, split semicolon-chained tactics, distinct names for
the two `Pure` hypotheses, terminal `simp`, and `RingHom.ext hcommfun`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
chrisflav
removed
the
awaiting-auto-review
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fill three sorries in
Proetale/Algebra/Bijective.lean:Algebra.bijective_comap_lmul'_of_bijective_of_bijective: if a ring mapR → Sis bijective on prime spectra with trivial residue field extensions, thenSpec S → Spec (S ⊗[R] S)(vialmul') is bijective.Algebra.bijective_of_bijective_of_flat: a flat, surjective ring map that is bijective on prime spectra is an isomorphism (its kernel is a pure ideal with empty vanishing locus, hence zero).Algebra.WeaklyEtale.bijective_algebraMap_of_bijective_residueFieldMap: a weakly étale local homomorphism of local rings that is bijective on spectra with trivial residue field extensions is an isomorphism.These correspond to the blueprint lemmas
lem:bij-on-spectrum-of-unique-lying-over-and-residue-field-eq,lem:iso-of-bij-on-spectrum-and-surj-and-flat, andlem:isom-of-unique-lying-over-and-residue-field-eq; the matching proof-level\leanoks are added.🤖 Generated with Claude Code