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

65 declarations, 0 contain sorry, 0 declared as axioms

The patching module

The patching module attached to a family of R i-modules M i of uniformly bounded rank: the ultraproduct of the truncations M i / I^k M i along a non-principal ultrafilter, viewed as a module over the patching algebra.

Imports (13)

Imported by 2 files

class Module.UniformlyBoundedRank A family of R-modules M i has uniformly bounded rank if there exists a single bound n : ℕ such that for every i, the rank of M i over R / Ann (M i) is less than n line 46 source
Source documentation
A family of R-modules M i has uniformly bounded rank if there exists a single bound n : ℕ such that for every i, the rank of M i over R / Ann (M i) is less than n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module
3 instances, coercions and auxiliary constants left out.
```
class Module.UniformlyBoundedRank : Prop where
…
```
def Module.UniformlyBoundedRank.bound line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.UniformlyBoundedRank, Nat
Proof uses: Exists.choose, LT.lt, Cardinal, Module.rank, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank.cond
15 instances, coercions and auxiliary constants left out.
lemma Module.UniformlyBoundedRank.rank_lt_bound line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.UniformlyBoundedRank, LT.lt, Cardinal, Module.rank, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank.bound
Proof uses: Exists.choose_spec, Nat, Module.UniformlyBoundedRank.cond
24 instances, coercions and auxiliary constants left out.
lemma Module.UniformlyBoundedRank.finrank_lt_bound line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.UniformlyBoundedRank, LT.lt, Nat, Module.finrank, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank.bound
Proof uses: Module.finrank_lt_of_rank_lt, Module.UniformlyBoundedRank.rank_lt_bound
15 instances, coercions and auxiliary constants left out.
instance (instance at line 66) line 66 source
instance (instance at line 70) line 70 source
lemma Module.UniformlyBoundedRank.exists_finsupp_surjective line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Exists, LinearMap, RingHom.id, Finsupp, Fin, Module.UniformlyBoundedRank.bound, Function.Surjective
Proof uses: Subsingleton, Nontrivial, Or, Eq, subsingleton_or_nontrivial, Or.inl, Exists.intro, OfNat.ofNat, Subsingleton.elim, Or.inr, Eq.mpr, Ne, Top.top, id, congrArg, propext, Ideal.Quotient.nontrivial_iff, Not, ne_eq, Submodule.annihilator and 39 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Module.UniformlyBoundedRank.finite_quotient_smul line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Finite, Submodule, HSMul.hSMul, Top.top
Proof uses: LinearMap, RingHom.id, Finsupp, Fin, Module.UniformlyBoundedRank.bound, Function.Surjective, Exists, Module.UniformlyBoundedRank.exists_finsupp_surjective, Pi.liftQuotientₗ, LinearMap.comp, LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, Pi.liftQuotientₗ_surjective, Function.Surjective.comp, LinearEquiv.surjective, Finite.of_surjective
57 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Module.UniformlyBoundedRank.card_quotient_le line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Finite, LE.le, Nat, Nat.card, Submodule, HSMul.hSMul, Top.top, HPow.hPow, Module.UniformlyBoundedRank.bound
Proof uses: LinearMap, RingHom.id, Finsupp, Fin, Function.Surjective, Exists, Module.UniformlyBoundedRank.exists_finsupp_surjective, Pi.liftQuotientₗ, LinearMap.comp, LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, Pi.liftQuotientₗ_surjective, Function.Surjective.comp, LinearEquiv.surjective, LE.le.trans_eq, Nat.card_le_card_of_surjective, Fintype, Nonempty, Eq, nonempty_fintype and 17 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Module.UniformlyBoundedRank.exists_rank line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Exists, Nat, Filter.Eventually, Nonempty, LinearEquiv, RingHom.id, Fin
Proof uses: Module.UniformlyBoundedRank.bound, HAdd.hAdd, OfNat.ofNat, Eq.mpr, id, Eq, congrArg, Eq.symm, propext, Ultrafilter.eventually_exists_iff, Filter.Eventually.of_forall, Subsingleton, Nontrivial, Or, subsingleton_or_nontrivial, Or.inl, Exists.intro, Fin.mk, Nat.zero_lt_succ, Or.inr and 36 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
def Module.UniformlyBoundedRank.rank line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Nat
Proof uses: Exists.choose, Filter.Eventually, Nonempty, LinearEquiv, RingHom.id, Fin, Module.UniformlyBoundedRank.exists_rank
23 instances, coercions and auxiliary constants left out.
lemma Module.UniformlyBoundedRank.rank_spec line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Filter.Eventually, Nonempty, LinearEquiv, RingHom.id, Fin, Module.UniformlyBoundedRank.rank
Proof uses: Exists.choose_spec, Nat, Module.UniformlyBoundedRank.exists_rank
32 instances, coercions and auxiliary constants left out.
def Module.UniformlyBoundedRank.linearMap line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, LinearMap, RingHom.id, Fin, Module.UniformlyBoundedRank.rank
Proof uses: dite, Nonempty, LinearEquiv, Classical.propDecidable, LinearMap.comp, LinearEquiv.symm, Nonempty.some, LinearMap.compLeft, Algebra.linearMap, Not, OfNat.ofNat
35 instances, coercions and auxiliary constants left out.
lemma Module.UniformlyBoundedRank.linearMap_surjective line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Filter.Eventually, Function.Surjective, Fin, Module.UniformlyBoundedRank.rank, LinearMap, RingHom.id, Module.UniformlyBoundedRank.linearMap
Proof uses: Filter.mp_mem, Set.ofPred, Nonempty, LinearEquiv, Module.UniformlyBoundedRank.rank_spec, Filter.univ_mem', Membership.mem, Set, id, Eq.mpr, dite, Classical.propDecidable, LinearMap.comp, LinearEquiv.symm, Nonempty.some, LinearMap.compLeft, Algebra.linearMap, Not, OfNat.ofNat, Eq and 10 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Module.UniformlyBoundedRank.linearMap_eq_zero line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Filter.Eventually, Fin, Module.UniformlyBoundedRank.rank, Iff, Eq, LinearMap, RingHom.id, Module.UniformlyBoundedRank.linearMap, OfNat.ofNat, Membership.mem
Proof uses: Filter.mp_mem, Set.ofPred, Nonempty, LinearEquiv, Module.UniformlyBoundedRank.rank_spec, Filter.univ_mem', Set, id, Eq.mpr, dite, Classical.propDecidable, LinearMap.comp, LinearEquiv.symm, Nonempty.some, LinearMap.compLeft, Algebra.linearMap, Not, congrArg, Module.UniformlyBoundedRank.linearMap.eq_1, dite_eq_left and 9 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev PatchingModule.Component Documented declaration: Component line 185 source
Source documentation
The α-th component of the patching module associated to (i) a family of modules M i over a commutative ring R, (ii) an ultrafilter on the index set for the M i and (iii) an ideal of R. This is the ultraproduct of M i / α • M i along the ultrafilter F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Ideal
Proof uses: UltraProduct, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
15 instances, coercions and auxiliary constants left out.
```
abbrev PatchingModule.Component (α : Ideal R) :=
…
```
def PatchingModule.liftComponent A family of linear maps f i : M₀ →ₗ[R] M i lifts to a linear map M₀ / α • M₀ → Component α line 193 source
Source documentation
A family of linear maps f i : M₀ →ₗ[R] M i lifts to a linear map M₀ / α • M₀ → Component α.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Ideal, LinearMap, RingHom.id, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.Component
Proof uses: LinearMap.comp, UltraProduct, UltraProduct.πₗ, LinearMap.pi, Submodule.mapQ
49 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def PatchingModule.liftComponent (α : Ideal R) (f : ∀ i, M₀ →ₗ[R] M i) :
    M₀ ⧸ (α • ⊤ : Submodule R M₀) →ₗ[R] Component R M F α :=
…
```
Mentions: PatchingModule.Component
def OpenIdeals The set of open ideals of a topological ring R line 201 source
Source documentation
The set of open ideals of a topological ring R.

no axioms what this means
Statement uses: TopologicalSpace, CommRing
Proof uses: Subtype, Ideal, IsOpen
6 instances, coercions and auxiliary constants left out.
```
def OpenIdeals : Type _ := { α : Ideal R // IsOpen (X := R) α }
```
instance (instance at line 203) line 203 source
instance (instance at line 206) line 206 source
abbrev PatchingModule.componentMap The transition linear map between components for ideals α ≤ β: Component α → Component β line 211 source
Source documentation
The transition linear map between components for ideals α ≤ β: Component α → Component β.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Ideal, LE.le, LinearMap, RingHom.id, PatchingModule.Component, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: UltraProduct, UltraProduct.map, Submodule.mapQ, LinearMap.id
46 instances, coercions and auxiliary constants left out.
```
abbrev PatchingModule.componentMap {α β : Ideal R} (h : α ≤ β) :
    Component R M F α →ₗ[R] Component R M F β :=
…
```
Mentions: PatchingModule.Component
def PatchingModule.submodule The patching module as a submodule of the product of components: those families compatible with the transition maps as α ≤ β ranges over open ideals line 225 source
Source documentation
The patching module as a submodule of the product of components: those families compatible with the transition maps as α ≤ β ranges over open ideals. This is just an explicit construction of the patching module (a projective limit of components) as a subset of a product of components.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, Submodule, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, HasQuotient.Quotient, HSMul.hSMul, Top.top
Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, LE.le, Eq, LinearMap, RingHom.id, PatchingModule.componentMap, Membership.mem, Set
60 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def PatchingModule.submodule : Submodule (ι → R) (Π α : OpenIdeals R, Component R M F α.1) where
…
```
Mentions: OpenIdeals, PatchingModule.Component
lemma PatchingModule.isClosed_submodule line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, IsClosed, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.submodule
Proof uses: LE.le, Set.ofPred, Eq, LinearMap, RingHom.id, PatchingModule.componentMap, isClosed_eq, id, Continuous, Continuous.comp', UltraProduct, UltraProduct.map, Submodule.mapQ, LinearMap.id, continuous_bot, continuous_apply, Eq.mpr, Set.iInter, eq_of_heq, Set and 13 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def PatchingModule The patching module for a family M i of modules over a commutative topological ring R line 248 source
Source documentation
The patching module for a family M i of modules over a commutative topological ring R. This is an inverse limit over α of ultraproducts of M i / α • M i along the ultrafilter F, where α ranges over open ideals of R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter
Proof uses: Subtype, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, Membership.mem, Submodule, HasQuotient.Quotient, HSMul.hSMul, Top.top, PatchingModule.submodule
26 instances, coercions and auxiliary constants left out.
```
def PatchingModule : Type _ := PatchingModule.submodule R M F
```
Mentions: PatchingModule.submodule
instance (instance at line 250) line 250 source
instance (instance at line 253) line 253 source
instance (instance at line 256) line 256 source
lemma PatchingModule.smul_apply line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, PatchingModule, OpenIdeals, Eq, PatchingModule.Component, Ideal, IsOpen, Membership.mem, Submodule, HasQuotient.Quotient, HSMul.hSMul, Top.top, PatchingModule.submodule
Proof uses: rfl
73 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
instance (instance at line 264) line 264 source
instance (instance at line 267) line 267 source
instance (instance at line 270) line 270 source
instance (instance at line 273) line 273 source
instance (instance at line 284) line 284 source
instance (instance at line 287) line 287 source
instance (instance at line 290) line 290 source
def PatchingModule.π The projection from the patching module onto its α-th component, for an open ideal α of R line 298 source
Source documentation
The projection from the patching module onto its α-th component, for an open ideal α of R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, OpenIdeals, LinearMap, RingHom.id, PatchingModule, PatchingModule.Component, Ideal, IsOpen, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: LinearMap.comp, LinearMap.proj, Submodule.subtype, PatchingModule.submodule
50 instances, coercions and auxiliary constants left out.
```
def PatchingModule.π (α : OpenIdeals R) :
    PatchingModule R M F →ₗ[ι → R] PatchingModule.Component R M F α.1 :=
…
```
Mentions: OpenIdeals, PatchingModule, PatchingModule.Component
def PatchingModule.ofPi Auxiliary linear map from indexed sequences of representatives to the product of components, used to construct PatchingModule.incl line 304 source
Source documentation
Auxiliary linear map from indexed sequences of representatives to the product of components, used to construct PatchingModule.incl.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, OpenIdeals, RingHom.id, PatchingModule.Component, Ideal, IsOpen, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: LinearMap.piMap', LinearMap.comp, UltraProduct.πₗ, Submodule.mkQ
49 instances, coercions and auxiliary constants left out.
```
def PatchingModule.ofPi :
    (OpenIdeals R → Π i, M i) →ₗ[OpenIdeals R → ι → R]
      Π α : OpenIdeals R, Component R M F α.1 :=
…
```
Mentions: OpenIdeals, PatchingModule.Component
lemma PatchingModule.ofPi_apply line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, OpenIdeals, Eq, PatchingModule.Component, Ideal, IsOpen, LinearMap, RingHom.id, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.ofPi, UltraProduct, UltraProduct.πₗ, Submodule.Quotient.mk
Proof uses: rfl
53 instances, coercions and auxiliary constants left out.
lemma PatchingModule.ofPi_surjective line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, Function.Surjective, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, LinearMap, RingHom.id, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.ofPi
Proof uses: Eq, UltraProduct, UltraProduct.πₗ, Submodule.Quotient.mk, Exists.intro, funext, of_eq_true, Eq.trans, Filter.Eventually, True, congrArg, Eq.symm, congrFun', Filter, eq_self, Classical.choose, Submodule.Quotient.mk_surjective, Classical.choose_spec, UltraProduct.πₗ_surjective
55 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def PatchingModule.incl The natural (ι → R)-linear map ∏ i, M i → PatchingModule R M F line 324 source
Source documentation
The natural (ι → R)-linear map ∏ i, M i → PatchingModule R M F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, PatchingModule
Proof uses: LinearMap.codRestrict, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.submodule, LinearMap.comp, PatchingModule.ofPi, LinearMap.pi, LinearMap.id
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def PatchingModule.incl :
    (Π i, M i) →ₗ[ι → R] PatchingModule R M F :=
…
```
Mentions: PatchingModule
lemma PatchingModule.incl_apply line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, OpenIdeals, Eq, PatchingModule.Component, Ideal, IsOpen, Membership.mem, Submodule, HasQuotient.Quotient, HSMul.hSMul, Top.top, PatchingModule.submodule, LinearMap, RingHom.id, PatchingModule, PatchingModule.incl and 3 more
Proof uses: rfl
65 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance (instance at line 339) line 339 source
abbrev PatchingModule.componentMapModule Functoriality of PatchingModule.Component in the family of modules: a family of linear maps f i : M i →ₗ[R] N i induces a map between the α-th components line 362 source
Source documentation
Functoriality of PatchingModule.Component in the family of modules: a family of linear maps f i : M i →ₗ[R] N i induces a map between the α-th components.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, Ideal, PatchingModule.Component, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top
Proof uses: UltraProduct.map, Submodule.mapQ
33 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
abbrev PatchingModule.componentMapModule (α : Ideal R) :
    Component R M F α →ₗ[ι → R] Component R N F α :=
…
```
Mentions: PatchingModule.Component
lemma PatchingModule.componentMapModule_surjective line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, Function.Surjective, Ideal, PatchingModule.Component, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.componentMapModule
Proof uses: UltraProduct.map_surjective, Submodule.mapQ, Eq.mpr, Eq, LinearMap.range, id, congrArg, Eq.symm, propext, LinearMap.range_eq_top, Submodule.liftQ, LinearMap.comp, Submodule.mkQ, Submodule.mapQ.eq_1, Submodule.range_liftQ, Function.Surjective.comp, Submodule.mkQ_surjective
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def PatchingModule.map Functoriality of PatchingModule in the family of modules line 383 source
Source documentation
Functoriality of PatchingModule in the family of modules.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, PatchingModule
Proof uses: LinearMap.restrict, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, LinearMap.piMap', PatchingModule.componentMapModule, PatchingModule.submodule, Membership.mem, LE.le
41 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def PatchingModule.map :
    PatchingModule R M F →ₗ[ι → R] PatchingModule R N F :=
…
```
Mentions: PatchingModule
lemma PatchingModule.map_apply line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, PatchingModule, OpenIdeals, Eq, PatchingModule.Component, Ideal, IsOpen, Membership.mem, Submodule, HasQuotient.Quotient, HSMul.hSMul, Top.top, PatchingModule.submodule, PatchingModule.map and 1 more
Proof uses: rfl
58 instances, coercions and auxiliary constants left out.
lemma PatchingModule.map_comp_apply line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, PatchingModule, Eq, PatchingModule.map, LinearMap.comp
Proof uses: Subtype.ext, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, Membership.mem, Submodule, HasQuotient.Quotient, HSMul.hSMul, Top.top, PatchingModule.submodule, funext, PatchingModule.ofPi, Exists, PatchingModule.ofPi_surjective, of_eq_true, Eq.trans, UltraProduct, UltraProduct.πₗ, Submodule.Quotient.mk and 7 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma PatchingModule.map_comp line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, Eq, PatchingModule, PatchingModule.map, LinearMap.comp
Proof uses: LinearMap.ext, PatchingModule.map_comp_apply
18 instances, coercions and auxiliary constants left out.
lemma PatchingModule.map_id line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, Eq, LinearMap, RingHom.id, PatchingModule, PatchingModule.map, LinearMap.id
Proof uses: LinearMap.ext, Subtype.ext, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, Membership.mem, Submodule, HasQuotient.Quotient, HSMul.hSMul, Top.top, PatchingModule.submodule, funext, UltraProduct, UltraProduct.πₗ, Exists, UltraProduct.πₗ_surjective, of_eq_true, Eq.trans, True and 8 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def PatchingModule.mapEquiv A family of linear equivalences M i ≃ₗ[R] N i lifts to a linear equivalence between the corresponding patching modules line 426 source
Source documentation
A family of linear equivalences M i ≃ₗ[R] N i lifts to a linear equivalence between the corresponding patching modules.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, LinearEquiv, RingHom.id, PatchingModule
Proof uses: LinearMap, PatchingModule.map, LinearEquiv.mk, LinearEquiv.symm
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def PatchingModule.mapEquiv (f : ∀ i, M i ≃ₗ[R] N i) :
    PatchingModule R M F ≃ₗ[ι → R] PatchingModule R N F where
…
```
Mentions: PatchingModule
lemma PatchingModule.map_surjective line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, IsTopologicalRing, CompactSpace, AddCommGroup, Module, Ultrafilter, LinearMap, RingHom.id, IsLocalRing, IsLocalRing.IsAdicTopology, Module.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Function.Surjective, PatchingModule, PatchingModule.map
Proof uses: OpenIdeals, Set, PatchingModule.Component, IsOpen, Set.preimage, Submodule, HSMul.hSMul, Top.top, PatchingModule.componentMapModule, Singleton.singleton, Membership.mem, PatchingModule.submodule, LE.le, Subtype.mk, PatchingModule.componentMap, Eq, UltraProduct, UltraProduct.πₗ, Exists, UltraProduct.πₗ_surjective and 41 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
def PatchingModule.toConst The natural map from a fixed module M to the patching module of the constant family fun _ ↦ M line 484 source
Source documentation
The natural map from a fixed module M to the patching module of the constant family fun _ ↦ M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, Ultrafilter, AddCommGroup, Module, LinearMap, RingHom.id, PatchingModule
Proof uses: LinearMap.comp, PatchingModule.incl, LinearMap.pi, LinearMap.id
20 instances, coercions and auxiliary constants left out.
```
def PatchingModule.toConst (M) [AddCommGroup M] [Module R M] :
    M →ₗ[R] PatchingModule R (fun _ ↦ M) F :=
…
```
Mentions: PatchingModule
lemma PatchingModule.toConst_surjective line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, IsTopologicalRing, CompactSpace, Ultrafilter, AddCommGroup, Module, Module.Finite, Function.Surjective, PatchingModule, LinearMap, RingHom.id, PatchingModule.toConst
Proof uses: moduleTopology, IsModuleTopology, IsModuleTopology.mk, rfl, IsModuleTopology.compactSpace, Continuous, IsModuleTopology.continuous_of_linearMap, DenseRange, denseRange_inverseLimit, OpenIdeals, PatchingModule.Component, Ideal, IsOpen, LE.le, HasQuotient.Quotient, Submodule, HSMul.hSMul, Top.top, PatchingModule.componentMap, continuous_of_discreteTopology and 43 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def PatchingModule.constEquiv line 517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, IsTopologicalRing, CompactSpace, Ultrafilter, IsLocalRing, T2Space, IsNoetherianRing, AddCommGroup, Module, Module.Finite, LinearEquiv, RingHom.id, PatchingModule
Proof uses: LinearEquiv.ofBijective, PatchingModule.toConst
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
class IsPatchingSystem A family of modules M i is a patching system along the filter F if for every open ideal α ⊆ R, the annihilator Ann (M i) is F-eventually contained in α line 534 source
Source documentation
A family of modules M i is a patching system along the filter F if for every open ideal α ⊆ R, the annihilator Ann (M i) is F-eventually contained in α.

standard axioms: Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Filter
3 instances, coercions and auxiliary constants left out.
```
class IsPatchingSystem (F : Filter ι) : Prop where
…
```
def IsPatchingSystem.linearMap line 545 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, LinearMap, RingHom.id, Fin, Module.UniformlyBoundedRank.rank, Submodule, HSMul.hSMul, Top.top
Proof uses: Pi.liftQuotientₗ, Module.UniformlyBoundedRank.linearMap
31 instances, coercions and auxiliary constants left out.
lemma IsPatchingSystem.linearMap_compLeft line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, Fin, Module.UniformlyBoundedRank.rank, Eq, Submodule, HSMul.hSMul, Top.top, LinearMap, RingHom.id, IsPatchingSystem.linearMap, LinearMap.compLeft, Algebra.linearMap and 2 more
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap.ker, LinearEquiv, LinearEquiv.trans, Subtype, Membership.mem, LinearMap.range, LinearEquiv.symm, LinearEquiv.ofTop, LinearMap.quotKerEquivRange, Submodule.liftQ, LinearMap.comp, Submodule.mkQ, LinearMap.quotKerEquivRange_symm_apply_image, Eq.rec, trivial and 2 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsPatchingSystem.linearMap_bijective line 558 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem, IsOpen, Filter.Eventually, Function.Bijective, Fin, Module.UniformlyBoundedRank.rank, Submodule, HSMul.hSMul, Top.top, LinearMap and 2 more
Proof uses: Filter.mp_mem, Set.ofPred, LE.le, IsPatchingSystem.cond, Iff, Eq, Module.UniformlyBoundedRank.linearMap, OfNat.ofNat, Membership.mem, Set, Module.UniformlyBoundedRank.linearMap_eq_zero, Function.Surjective, Module.UniformlyBoundedRank.linearMap_surjective, Filter.univ_mem', id, Pi.liftQuotientₗ_bijective, LinearMap.ker, Eq.mpr, LinearMap.compLeft, Algebra.linearMap and 8 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def PatchingModule.equivComponent line 569 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, IsTopologicalRing, CompactSpace, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem, IsOpen, LinearEquiv, RingHom.id, Fin, Module.UniformlyBoundedRank.rank, PatchingModule.Component, Submodule and 2 more
Proof uses: LinearEquiv.ofBijective, LinearMap.comp, UltraProduct, UltraProduct.πₗ, LinearMap.pi, IsPatchingSystem.linearMap
69 instances, coercions and auxiliary constants left out.
def PatchingModule.mapOfIsPatchingSystem line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, IsTopologicalRing, CompactSpace, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem, LinearMap, RingHom.id, Fin, Module.UniformlyBoundedRank.rank, PatchingModule
Proof uses: LinearMap.codRestrict, OpenIdeals, PatchingModule.Component, IsOpen, Submodule, HSMul.hSMul, Top.top, Submodule.restrictScalars, PatchingModule.submodule, LinearMap.pi, LinearMap.comp, PatchingModule.equivComponent, LinearMap.compLeft, Algebra.linearMap, LE.le
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma PatchingModule.continuous_ofPi line 587 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, IsTopologicalRing, CompactSpace, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem, Continuous, Fin, Module.UniformlyBoundedRank.rank, PatchingModule, LinearMap, RingHom.id, PatchingModule.mapOfIsPatchingSystem
Proof uses: LinearMap.continuous_on_pi
42 instances, coercions and auxiliary constants left out.
lemma PatchingModule.mapOfIsPatchingSystem_bijective line 612 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, CompactSpace, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem, NonarchimedeanRing, T2Space, Function.Bijective, Fin, Module.UniformlyBoundedRank.rank, PatchingModule, LinearMap, RingHom.id and 1 more
Proof uses: And.intro, Function.Injective, Function.Surjective, Eq.mpr, Eq, OfNat.ofNat, id, congrArg, propext, injective_iff_map_eq_zero, RingHom, funext, OpenIdeals, PatchingModule.Component, IsOpen, LinearEquiv, Submodule, HSMul.hSMul, Top.top, PatchingModule.equivComponent and 53 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
instance (instance at line 635) line 635 source
instance (instance at line 638) line 638 source
lemma PatchingModule.rank_patchingModule line 643 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, CommRing, CompactSpace, AddCommGroup, Module, Ultrafilter, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem, NonarchimedeanRing, T2Space, Nontrivial, Eq, Cardinal, Module.rank, PatchingModule, Module.UniformlyBoundedRank.rank
Proof uses: Eq.mp, Cardinal.lift, Fin, Eq.trans, congrArg, Cardinal.sum, rank_pi, HMul.hMul, Cardinal.mk, OfNat.ofNat, funext, Module.rank_self, Cardinal.sum_const, congr, Fintype.card, Cardinal.mk_fintype, Nat, Fintype.card_fin, Cardinal.lift_natCast, Cardinal.lift_uzero and 7 more
44 instances, coercions and auxiliary constants left out.

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