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

18 declarations, 0 contain sorry, 0 declared as axioms

Restricted product of modules as a module over restricted product of rings

If R : ι → Type* is a family of rings, B : (i : ι) → Subring (R i) is a family of subrings, M : ι → Type* is a family of types, with M i having an R i-module structure and C : (i : ι) → Submodule (B i) (M i), then Πʳ i, [M i, C i]_[𝓕] has a Πʳ i, [R i, B i]_[𝓕]-module structure.

Main definitions

RestrictedProduct.module' is the module structure defined above.
RestrictedProduct.linearMapComponent is the component M j →ₗ[R j] M' j given by a linear map Πʳ i, [M i, C i]_[𝓕] →ₗ[Πʳ i, [R i, B i]_[𝓕]] Πʳ i, [M' i, C' i]_[𝓕].
ContinuousLinearEquiv.restrictedProductPi is the continuous linear equivalence between Πʳ i, [(R i)^n, (B i)^n] and Πʳ i, [(R i), (B i)]^n.

Main theorems

RestrictedProduct.isOpenMap_linearMap_of_surjective : a condition for a linear map to be surjective based on properties of its components.
Instances for ContinuousSMul (Πʳ i, [R i, B i]_[𝓟 T]) (Πʳ i, [M i, C i]_[𝓟 T]) and ContinuousSMul (Πʳ i, [R i, B i]) (Πʳ i, [M i, C i]).
RestrictedProduct.isModuleTopology : Πʳ i, [M i, C i] has the Πʳ i, [R i, B i]-module topology if (M i) have the (R i)-module topology and (B i) and (C i) are open.

Imports (10)

Imported by 3 files

instance RestrictedProduct.(instance at line 67) line 67 source
lemma RestrictedProduct.smul_apply' line 73 source
standard axioms: Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, Filter, AddCommGroup, Module, SMulMemClass, Subtype, Membership.mem, RestrictedProduct, Eq, HSMul.hSMul
Proof uses: rfl
54 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance RestrictedProduct.(instance at line 77) line 77 source
lemma RestrictedProduct.single_smul line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, DecidableEq, RestrictedProduct, Filter.cofinite, Eq, HSMul.hSMul, RestrictedProduct.single
Proof uses: RestrictedProduct.ext, Not, Or, em, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Pi.single_eq_same, eq_self, OfNat.ofNat, Zero, ZeroMemClass, RestrictedProduct.single_eq_of_ne', zero_smul
86 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.smul_single line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, DecidableEq, RestrictedProduct, Filter.cofinite, Eq, HSMul.hSMul, RestrictedProduct.single
Proof uses: RestrictedProduct.ext, Not, Or, em, of_eq_true, Eq.trans, True, congr, congrArg, Pi.single_eq_same, eq_self, OfNat.ofNat, Zero, ZeroMemClass, RestrictedProduct.single_eq_of_ne', smul_zero
71 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.single_eq_smul line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, DecidableEq, RestrictedProduct, Filter.cofinite, Eq, HSMul.hSMul, RestrictedProduct.single, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, RestrictedProduct.single_smul, RestrictedProduct.single.congr_simp, one_smul, eq_self
86 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.linearMapComponent Components of a linear map line 116 source
Source documentation
Components of a linear map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, DecidableEq, LinearMap, RestrictedProduct, Filter.cofinite, RingHom.id
Proof uses: LinearMap.mk, AddHom.mk, RestrictedProduct.single
67 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
noncomputable def linearMapComponent
    (f : Πʳ i, [M i, C i] →ₗ[Πʳ i, [R i, B i]] Πʳ i, [M₂ i, C₂ i]) (i : ι) : M i →ₗ[R i] M₂ i where
…
```
lemma RestrictedProduct.linearMap_component_apply line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, DecidableEq, LinearMap, RestrictedProduct, Filter.cofinite, RingHom.id, Eq, RestrictedProduct.linearMapComponent, RestrictedProduct.single
Proof uses: rfl
65 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.linearMap_apply_eq_component line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, DecidableEq, LinearMap, RestrictedProduct, Filter.cofinite, RingHom.id, Eq, RestrictedProduct.linearMapComponent
Proof uses: Eq.mpr, RestrictedProduct.single, id, congrArg, RestrictedProduct.linearMap_component_apply, HSMul.hSMul, OfNat.ofNat, Eq.symm, RestrictedProduct.single_eq_smul, map_smul, RestrictedProduct.single_smul, RestrictedProduct.single_eq_same, one_smul, Eq.refl
86 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance RestrictedProduct.(instance at line 144) line 144 source
instance RestrictedProduct.(instance at line 151) line 151 source
theorem RestrictedProduct.isOpenMap_linearMap_of_surjective line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, TopologicalSpace, DecidableEq, IsOpen, LinearMap, RestrictedProduct, Filter.cofinite, RingHom.id, IsOpenMap, RestrictedProduct.linearMapComponent, Filter.Eventually, Set.SurjOn
Proof uses: RestrictedProduct.isOpenMap_of_open_components, RestrictedProduct.linearMap_apply_eq_component
59 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.piSubringSubmodule If B i is subring of R i then (B i)^n is a B i-submodule of (R i)^n line 182 source
Source documentation
If B i is subring of R i then (B i)^n is a B i-submodule of (R i)^n.

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, Submodule, Subtype, Membership.mem
Proof uses: Submodule.pi, Set.univ, Subring.toSubmodule, Subring.ofClass
18 instances, coercions and auxiliary constants left out.
```
def piSubringSubmodule (i : ι) : Submodule (B i) (n → R i) :=
…
```
def RestrictedProduct._root_.LinearEquiv.restrictedProductPi Canonical linear equivalence between Π' R^n and (Π' R)^n line 187 source
Source documentation
Canonical linear equivalence between Π' R^n and (Π' R)^n
```
def _root_.LinearEquiv.restrictedProductPi [Fintype n] :
    Πʳ i, [n → R i, piSubringSubmodule B n i]_[ℱ] ≃ₗ[Πʳ i, [R i, B i]_[ℱ]]
      n → Πʳ i, [R i, B i]_[ℱ] where
…
```
Mentions: RestrictedProduct.piSubringSubmodule
lemma RestrictedProduct.isOpen_piSubringSubmodule line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, TopologicalSpace, Finite, IsOpen, Submodule, Subtype, Membership.mem, RestrictedProduct.piSubringSubmodule
Proof uses: Eq.mpr, Submodule.pi, Set.univ, Subring.toSubmodule, Subring.ofClass, id, Eq, congrArg, RestrictedProduct.piSubringSubmodule.eq_1, Set.pi, Set, Submodule.coe_pi, isOpen_set_pi, Set.finite_univ
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct._root_.ContinuousLinearEquiv.restrictedProductPi Canonical continuous linear equivalence between Π' R^n and (Π' R)^n line 212 source
Source documentation
Canonical continuous linear equivalence between Π' R^n and (Π' R)^n
```
def _root_.ContinuousLinearEquiv.restrictedProductPi [Fintype n]
    (hOpen : ∀ i, IsOpen (B i : Set (R i))) :
    Πʳ i, [n → R i, piSubringSubmodule B n i] ≃L[Πʳ i, [R i, B i]] n → Πʳ i, [R i, B i] where
…
```
Mentions: RestrictedProduct.piSubringSubmodule
lemma RestrictedProduct.moduleToplogy_of_prod line 227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, TopologicalSpace, IsTopologicalRing, Finite, IsOpen, IsModuleTopology, RestrictedProduct, Filter.cofinite, Submodule, Subtype, Membership.mem, RestrictedProduct.piSubringSubmodule
Proof uses: Fintype, Fintype.ofFinite, Fact, Fact.mk, IsModuleTopology.iso, ContinuousLinearEquiv.symm, RingHom.id, ContinuousLinearEquiv.restrictedProductPi
62 instances, coercions and auxiliary constants left out.
theorem RestrictedProduct.isModuleTopology line 240 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, AddCommGroup, Module, AddSubgroupClass, SMulMemClass, Subtype, Membership.mem, TopologicalSpace, IsTopologicalRing, IsModuleTopology, Module.Finite, RestrictedProduct, Filter.cofinite, IsOpen
Proof uses: Fact, Fact.mk, Nat, Exists, LinearMap, RingHom.id, Fin, Function.Surjective, Module.Finite.exists_fin', ContinuousLinearEquiv, Submodule, RestrictedProduct.piSubringSubmodule, ContinuousLinearEquiv.restrictedProductPi, LinearMap.comp, ContinuousAdd, IsModuleTopology.toContinuousAdd, ContinuousSMul, RestrictedProduct.moduleToplogy_of_prod, Function.Surjective.comp, ContinuousLinearEquiv.surjective and 19 more
126 instances, coercions and auxiliary constants left out.

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