Over.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

12 declarations, 0 contain sorry, 0 declared as axioms

The patching module over a coefficient ring

Lifting linear (iso)morphisms modulo a power of an ideal to the level of patching modules: produces module-equivalences between patching modules out of compatible families of mod-I^k equivalences.

Imports (7)

Imported by 2 files

def Submodule.liftModIdeal Given a linear map f : M / I • M → N / I • N, produce the induced linear map between the corresponding quotients of M / J • M and N / J • N modulo I line 54 source
Source documentation
Given a linear map f : M / I • M → N / I • N, produce the induced linear map between the corresponding quotients of M / J • M and N / J • N modulo I.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ideal, LinearMap, RingHom.id, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: Submodule.liftQ, LinearMap.comp, Submodule.mapQ, Submodule.mkQ
60 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
def Submodule.liftModIdeal {R M N : Type*} [CommRing R]
    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {I : Ideal R}
    (f : M ⧸ (I • ⊤ : Submodule R M) →ₗ[R] N ⧸ (I • ⊤ : Submodule R N)) (J : Ideal R) :
    (M ⧸ (J • ⊤ : Submodule R M)) ⧸ (I • ⊤ : Submodule R (M ⧸ (J • ⊤ : Submodule R M))) →ₗ[R]
    (N ⧸ (J • ⊤ : Submodule R N)) ⧸ (I • ⊤ : Submodule R (N ⧸ (J • ⊤ : Submodule R N))) := by
…
```
def Submodule.liftModIdealEquiv Promote Submodule.liftModIdeal to a linear equivalence: a linear equivalence between R-modules M /IM and N/IN lifts to one between (M/JM)/I and (N/JM)/I line 81 source
Source documentation
Promote Submodule.liftModIdeal to a linear equivalence: a linear equivalence between R-modules M /IM and N/IN lifts to one between (M/JM)/I and (N/JM)/I.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ideal, LinearEquiv, RingHom.id, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: LinearMap, Submodule.liftModIdeal, LinearEquiv.mk, LinearEquiv.symm
62 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
def Submodule.liftModIdealEquiv {R M N : Type*} [CommRing R]
    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {I : Ideal R}
    (f : (M ⧸ (I • ⊤ : Submodule R M)) ≃ₗ[R] N ⧸ (I • ⊤ : Submodule R N)) (J : Ideal R) :
    ((M ⧸ (J • ⊤ : Submodule R M)) ⧸ (I • ⊤ : Submodule R (M ⧸ (J • ⊤ : Submodule R M)))) ≃ₗ[R]
    (N ⧸ (J • ⊤ : Submodule R N)) ⧸ (I • ⊤ : Submodule R (N ⧸ (J • ⊤ : Submodule R N))) where
…
```
instance (instance at line 105) line 105 source
lemma PatchingModule.ker_componentMapModule_mkQ attribute [local instance] UltraProduct.instIsScalarTower in line 115 source
Source comment
attribute [local instance] UltraProduct.instIsScalarTower in

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, TopologicalSpace, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, IsTopologicalRing, OpenIdeals, Eq, Submodule, PatchingModule.Component, IsOpen, HSMul.hSMul, Top.top, LinearMap.ker and 3 more
Proof uses: LinearMap, Eq.mpr, Subtype.mk, id, congrArg, rfl, Finite, AddSubgroup.quotient_finite_of_isOpen, Submodule.toAddSubgroup, LE.le, Submodule.comap, Submodule.map, Eq.symm, propext, Submodule.map_le_iff_le_comap, Submodule.map_smul'', Submodule.smul_mono, le_rfl, le_top, Submodule.mapQ and 87 more
205 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma PatchingModule.ker_componentMapModule_mkQ [IsTopologicalRing Λ] (α : OpenIdeals Λ) :
    LinearMap.ker ((componentMapModule Λ F (fun i ↦
      (𝔫 • ⊤ : Submodule Λ (M i)).mkQ) α.1).restrictScalars Λ) = 𝔫 • ⊤ := by
…
```
Mentions: OpenIdeals, PatchingModule.componentMapModule
lemma PatchingModule.mem_smul_top line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, TopologicalSpace, IsLocalRing, IsNoetherianRing, T2Space, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, IsTopologicalRing, PatchingModule, Iff, Membership.mem, Submodule, HSMul.hSMul and 5 more
Proof uses: Iff.intro, Submodule.map, Subtype, RingHom.id, Submodule.subtype, LinearMap, Submodule.mem_map_of_mem, LinearMap.proj, mem_of_le_of_mem, Submodule.smul_mono, le_rfl, le_top, Eq.mp, congrFun', congrArg, Eq.trans, Submodule.map.congr_simp, Eq.refl, Submodule.map_smul'', Finset and 111 more
190 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma PatchingModule.ker_map_mkQ line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, TopologicalSpace, IsLocalRing, IsNoetherianRing, T2Space, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, IsTopologicalRing, Eq, Submodule, PatchingModule, LinearMap.ker, HSMul.hSMul and 4 more
Proof uses: le_antisymm, OpenIdeals, PatchingModule.Component, IsOpen, Membership.mem, PatchingModule.submodule, Subtype.mk, PatchingModule.componentMapModule, congr_fun, LinearMap, OfNat.ofNat, congr_arg, Subtype, Eq.mp, congrArg, PatchingModule.ker_componentMapModule_mkQ, Eq.mpr, id, propext, PatchingModule.mem_smul_top and 30 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def PatchingModule.quotientTo line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, TopologicalSpace, IsLocalRing, IsNoetherianRing, NonarchimedeanRing, T2Space, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, LinearMap, RingHom.id, PatchingModule, Submodule, HSMul.hSMul and 1 more
Proof uses: Submodule.liftQ, PatchingModule.map, Submodule.mkQ
47 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def PatchingModule.quotientEquiv line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, TopologicalSpace, IsLocalRing, IsNoetherianRing, NonarchimedeanRing, T2Space, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, LinearEquiv, RingHom.id, PatchingModule, Submodule, HSMul.hSMul and 1 more
Proof uses: LinearEquiv.ofBijective, PatchingModule.quotientTo
46 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def PatchingModule.quotientEquivOver line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, TopologicalSpace, IsLocalRing, IsNoetherianRing, NonarchimedeanRing, T2Space, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, LinearEquiv, RingHom.id, Submodule, HSMul.hSMul, Top.top, CompactSpace and 2 more
Proof uses: LinearEquiv.trans, PatchingModule.quotientEquiv, LinearEquiv.restrictScalars, PatchingModule.mapEquiv, LinearEquiv.symm, PatchingModule.constEquiv
49 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra.quotientTo line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Algebra, Ultrafilter, Ideal, HasQuotient.Quotient, Ideal.map, RingHom, Algebra.algebraMap, PatchingAlgebra
Proof uses: Ideal.Quotient.lift, PatchingAlgebra.map, Ideal.Quotient.mk
24 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra.quotientToOver line 348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Algebra, Ultrafilter, Ideal, AlgEquiv, HasQuotient.Quotient, Ideal.map, RingHom, Algebra.algebraMap, IsNoetherianRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, PatchingAlgebra
Proof uses: Nontrivial, RingHom.comp, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, AlgEquiv.symm, PatchingAlgebra.constEquiv, PatchingAlgebra.mapEquiv, PatchingAlgebra.quotientTo
28 instances, coercions and auxiliary constants left out.
lemma PatchingAlgebra.surjective_quotientToOver line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Algebra, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, Ultrafilter, Algebra.UniformlyBoundedRank, Ideal, AlgEquiv, HasQuotient.Quotient, Ideal.map, RingHom, Algebra.algebraMap, IsNoetherianRing, Function.Surjective, PatchingAlgebra, PatchingAlgebra.quotientToOver
Proof uses: Nontrivial, RingHom.domain_nontrivial, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, IsLocalRing.of_surjective', AlgEquiv.symm, AlgEquiv.surjective, IsLocalHom, Ideal.Quotient.mk, IsLocalHom.of_surjective, Ideal.Quotient.mk_surjective, Function.Surjective.comp, PatchingAlgebra.constEquiv, PatchingAlgebra.mapEquiv, PatchingAlgebra.quotientTo, RingEquiv, RingEquiv.surjective, Ideal.Quotient.lift_surjective_of_surjective, PatchingAlgebra.map, PatchingAlgebra.map_surjective
48 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.