VanishingFilter.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

11 declarations, 0 contain sorry, 0 declared as axioms

Vanishing filters of ideals in product rings

For an ideal p of Πᵢ R i, we define the vanishing filter vanishingFilter p of p: the filter of subsets s such that the characteristic idempotent of s lies in p. Prime ideals give rise to ultrafilters via this construction.

Imports (2)

Imported by 1 file

FLT.lean

def vanishingFilter Documented declaration: vanishingFilter line 34 source
Source documentation
The vanishing filter of an ideal p of the product ring Πᵢ Rᵢ over an index set ι: a set s ⊆ ι is in the vanishing filter if the element of Πᵢ Rᵢ which is 0 on s and 1 outside s lies in p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Filter
Proof uses: Filter.mk, Set.ofPred, Set, Membership.mem, ite, Classical.propDecidable, OfNat.ofNat, LE.le
23 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def vanishingFilter (p : Ideal (Π i, R i)) : Filter ι where
…
```
lemma mem_vanishingFilter line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Set, Iff, Membership.mem, Filter, vanishingFilter, ite, Classical.propDecidable, OfNat.ofNat
Proof uses: Iff.rfl
21 instances, coercions and auxiliary constants left out.
def vanishingUltrafilter The vanishing ultrafilter of a prime ideal p of the product ring line 57 source
Source documentation
The vanishing ultrafilter of a prime ideal p of the product ring. See vanishingFilter for definition of a vanishing filter of an ideal of Πᵢ Rᵢ; if p is prime then this is an ultrafilter.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Ideal.IsPrime, Ultrafilter
Proof uses: Ultrafilter.ofComplNotMemIff, vanishingFilter
7 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
def vanishingUltrafilter (p : Ideal (Π i, R i)) [p.IsPrime] : Ultrafilter ι :=
…
```
lemma mem_vanishingUltrafilter line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Ideal.IsPrime, Set, Iff, Membership.mem, Ultrafilter, vanishingUltrafilter, ite, Classical.propDecidable, OfNat.ofNat
Proof uses: Iff.rfl
21 instances, coercions and auxiliary constants left out.
lemma eventually_vanishingFilter_not_isUnit line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Membership.mem, Filter.Eventually, Not, IsUnit, vanishingFilter
Proof uses: ite, Classical.propDecidable, Exists, Units, Eq, OfNat.ofNat, Eq.mpr, HMul.hMul, dite, Inv.inv, IsUnit.unit, eq_of_heq, outParam, Membership, HEq, Eq.refl, HEq.refl, Eq.symm, funext, of_eq_true and 17 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma vanishingFilter_le line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Filter, Iff, LE.le, vanishingFilter, Submodule, eventuallyProd, Bot.bot
Proof uses: Iff.intro, Membership.mem, Eq.mpr, HMul.hMul, ite, Set, Set.ofPred, Classical.propDecidable, OfNat.ofNat, eq_of_heq, outParam, Membership, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, id, funext, of_eq_true and 16 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma vanishingFilter_eventuallyProd line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Filter, Ne, Top.top, Eq, vanishingFilter, eventuallyProd
Proof uses: Filter.ext, Set, of_eq_true, Iff, Membership.mem, Eq.trans, True, congrFun', congrArg, ite, Classical.propDecidable, OfNat.ofNat, Submodule, Filter.Eventually, funext, apply_ite, And, False, ite.congr_simp, Eq.refl and 3 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma vanishingFilter_gc line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, GaloisConnection, OrderDual, Ideal, Filter, Function.comp, vanishingFilter, Equiv, OrderDual.ofDual, OrderDual.toDual, eventuallyProd, Bot.bot
Proof uses: vanishingFilter_le
22 instances, coercions and auxiliary constants left out.
def vanishingFilterGI The Galois insertion between filters on ι and ideals of Π i, R i (for nontrivial R i) formed by vanishingFilter and eventuallyProd ⊥ line 116 source
Source documentation
The Galois insertion between filters on ι and ideals of Π i, R i (for nontrivial R i) formed by vanishingFilter and eventuallyProd ⊥.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Nontrivial, GaloisInsertion, OrderDual, Ideal, Filter, Function.comp, vanishingFilter, Equiv, OrderDual.ofDual, OrderDual.toDual, eventuallyProd, Bot.bot
Proof uses: GaloisInsertion.mk, LE.le, vanishingFilter_gc
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def vanishingFilterGI [∀ i, Nontrivial (R i)] :
    GaloisInsertion (vanishingFilter ∘ ofDual)
      (toDual ∘ eventuallyProd (⊥ : ∀ i, Ideal (R i))) where
…
```
Mentions: vanishingFilter, eventuallyProd
lemma vanishingFilter_antimono line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, LE.le, Filter, vanishingFilter
Proof uses: GaloisConnection.monotone_l, OrderDual, Function.comp, Equiv, OrderDual.toDual, eventuallyProd, Bot.bot, OrderDual.ofDual, vanishingFilter_gc
26 instances, coercions and auxiliary constants left out.
lemma eventuallyProd_vanishingFilter_le line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, LE.le, Submodule, eventuallyProd, Bot.bot, vanishingFilter
Proof uses: GaloisConnection.le_u_l, OrderDual, Filter, Function.comp, Equiv, OrderDual.ofDual, OrderDual.toDual, vanishingFilter_gc
30 instances, coercions and auxiliary constants left out.