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

67 declarations, 0 contain sorry, 0 declared as axioms

Inverse limit of algebraic structures

We introduce all kinds of algebraic instances on InverseLimit, and specialize to the cases of modules and rings, showing that they are indeed limits in the respective categories.

Imports (2)

Imported by 2 files

def InverseLimit InverseLimit G f is the Inverse Limit of the objects G i glued by functions f line 28 source
Source documentation
InverseLimit G f is the Inverse Limit of the objects G i glued by functions f.

no axioms what this means
Statement uses: Preorder, LE.le, FunLike
Proof uses: Subtype, Eq
3 instances, coercions and auxiliary constants left out.
```
def InverseLimit : Type _ := {x : (i : ι) → G i // ∀ i j h, f i j h (x j) = (x i)}
…
```
lemma InverseLimit.InverseLimit_def line 32 source
no axioms what this means
Statement uses: Preorder, LE.le, FunLike, Eq, InverseLimit, Subtype
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
instance InverseLimit.(instance at line 37) line 37 source
lemma InverseLimit.prop line 41 source
no axioms what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Eq
Proof uses: Subtype.property
5 instances, coercions and auxiliary constants left out.
lemma InverseLimit.ext_lemma line 44 source
standard axioms: Quot.sound what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Eq
Proof uses: id, Subtype.ext, funext
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.instOne line 55 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, One, OneHomClass, InverseLimit
Proof uses: One.mk, Subtype.mk, Eq, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem InverseLimit.one_def line 58 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, One, OneHomClass, Eq, OfNat.ofNat, InverseLimit
Proof uses: rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 65) line 65 source
theorem InverseLimit.mul_def line 68 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Mul, MulHomClass, Eq, HMul.hMul
Proof uses: rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 73) line 73 source
instance InverseLimit.(instance at line 77) line 77 source
instance InverseLimit.(instance at line 81) line 81 source
instance InverseLimit.(instance at line 88) line 88 source
theorem InverseLimit.smul_def line 91 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, SMul, MulActionHomClass, Eq, HSMul.hSMul
Proof uses: rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 95) line 95 source
instance InverseLimit.(instance at line 102) line 102 source
instance InverseLimit.(instance at line 110) line 110 source
theorem InverseLimit.npow_def line 117 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Monoid, MonoidHomClass, Nat, Eq, HPow.hPow
Proof uses: rfl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 121) line 121 source
instance InverseLimit.(instance at line 129) line 129 source
theorem InverseLimit.inv_def line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Group, MonoidHomClass, Eq, Inv.inv
Proof uses: rfl
25 instances, coercions and auxiliary constants left out.
theorem InverseLimit.div_def line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Group, MonoidHomClass, Eq, HDiv.hDiv
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.
theorem InverseLimit.zpow_def line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, Group, MonoidHomClass, Int, Eq, HPow.hPow
Proof uses: rfl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 154) line 154 source
instance InverseLimit.(instance at line 158) line 158 source
instance InverseLimit.(instance at line 168) line 168 source
instance InverseLimit.(instance at line 172) line 172 source
instance InverseLimit.(instance at line 181) line 181 source
instance InverseLimit.(instance at line 187) line 187 source
instance InverseLimit.(instance at line 192) line 192 source
instance InverseLimit.(instance at line 202) line 202 source
theorem InverseLimit.inv₀_def line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, GroupWithZero, MonoidWithZeroHomClass, Eq, Inv.inv
Proof uses: rfl
19 instances, coercions and auxiliary constants left out.
theorem InverseLimit.div₀_def line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, GroupWithZero, MonoidWithZeroHomClass, Eq, HDiv.hDiv
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
theorem InverseLimit.zpow₀_def line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit, GroupWithZero, MonoidWithZeroHomClass, Int, Eq, HPow.hPow
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 225) line 225 source
instance InverseLimit.(instance at line 236) line 236 source
theorem InverseLimit.natCast_def line 245 source
standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, AddMonoidWithOne, AddMonoidHomClass, OneHomClass, Nat, Eq, InverseLimit
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 255) line 255 source
theorem InverseLimit.intCast_def line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, AddGroupWithOne, AddMonoidHomClass, OneHomClass, Int, Eq, InverseLimit
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
instance InverseLimit.(instance at line 271) line 271 source
instance InverseLimit.(instance at line 276) line 276 source
instance InverseLimit.(instance at line 282) line 282 source
instance InverseLimit.(instance at line 289) line 289 source
instance InverseLimit.(instance at line 294) line 294 source
instance InverseLimit.(instance at line 298) line 298 source
instance InverseLimit.(instance at line 302) line 302 source
instance InverseLimit.(instance at line 311) line 311 source
instance InverseLimit.(instance at line 316) line 316 source
instance InverseLimit.(instance at line 320) line 320 source
instance InverseLimit.(instance at line 324) line 324 source
instance InverseLimit.(instance at line 330) line 330 source
instance InverseLimit.(instance at line 338) line 338 source
instance InverseLimit.(instance at line 346) line 346 source
instance InverseLimit.(instance at line 354) line 354 source
instance InverseLimit.(instance at line 360) line 360 source
instance InverseLimit.(instance at line 369) line 369 source
def InverseLimit.toComponent toComponent G f i is the canonical function from the inverse limit of the G_j to G_i line 388 source
Source documentation
toComponent G f i is the canonical function from the inverse limit of the G_j to G_i. For the monoid homomorphism see toComponentMonoidHom, for the ring homomorphism see toComponentRingHom and for the linear map see toComponentLinearMap.

no axioms what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit
Proof uses: Eq
4 instances, coercions and auxiliary constants left out.
```
def toComponent (i : ι) : InverseLimit G f → G i := fun (z : InverseLimit G f) ↦ z.1 i
```
Mentions: InverseLimit
lemma InverseLimit.toComponent_def line 390 source
no axioms what this means
Statement uses: Preorder, LE.le, FunLike, Eq, InverseLimit, InverseLimit.toComponent
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
def InverseLimit.toComponentMonoidHom MonoidHom version of toComponent G f i line 396 source
Source documentation
MonoidHom version of toComponent G f i

standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, Group, MonoidHomClass, MonoidHom, InverseLimit
Proof uses: MonoidHom.mk, OneHom.mk, InverseLimit.toComponent
15 instances, coercions and auxiliary constants left out.
```
def toComponentMonoidHom (i : ι) [∀ i, Group (G i)] [∀ i j h, MonoidHomClass (T h) (G j) (G i)] :
    InverseLimit G f →* G i where
…
```
Mentions: InverseLimit
def InverseLimit.toComponentRingHom RingHom version of toComponent G f i line 406 source
Source documentation
RingHom version of toComponent G f i

standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, Ring, RingHomClass, RingHom, InverseLimit
Proof uses: RingHom.mk, MonoidHom.mk, OneHom.mk, InverseLimit.toComponent
16 instances, coercions and auxiliary constants left out.
```
def toComponentRingHom (i : ι) [∀ i, Ring (G i)] [∀ i j h, RingHomClass (T h) (G j) (G i)] :
    InverseLimit G f →+* G i where
…
```
Mentions: InverseLimit
def InverseLimit.toComponentLinearMap LinearMap version of toComponent G f i line 418 source
Source documentation
LinearMap version of toComponent G f i

standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, Ring, AddCommGroup, Module, LinearMapClass, LinearMap, RingHom.id, InverseLimit, RingHom
Proof uses: LinearMap.mk, AddHom.mk, InverseLimit.toComponent
27 instances, coercions and auxiliary constants left out.
```
def toComponentLinearMap (i : ι) {R : Type*} [Ring R]
  [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)] [∀ i j h, LinearMapClass (T h) R (G j) (G i)] :
    InverseLimit G f →ₗ[R] G i where
…
```
Mentions: InverseLimit
def InverseLimit.InverseSystemHom InverseSystemHom G f maps states that a indexed family of maps : W →G i have image in the InverseLimit G f subset of the product line 436 source
Source documentation
InverseSystemHom G f maps states that a indexed family of maps : W →G i have image in the InverseLimit G f subset of the product

no axioms what this means
Statement uses: Preorder, LE.le, FunLike
Proof uses: Eq
3 instances, coercions and auxiliary constants left out.
```
def InverseSystemHom := ∀ i j (h : i ≤ j) w, (f i j h) (maps j w) = maps i w
…
```
def InverseLimit.lift lift G f maps inverseSystemHom is the canonical function from W to the inverse limit of the G_j built by x ↦ Π maps_j x line 446 source
Source documentation
lift G f maps inverseSystemHom is the canonical function from W to the inverse limit of the G_j built by x ↦ Π maps_j x. For the monoid homomorphism see liftMonoidHom, for the ring homomorphism see liftRingHom, for the linear map see liftLinearMap.

no axioms what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit.InverseSystemHom, InverseLimit
Proof uses: Subtype.mk, Eq
3 instances, coercions and auxiliary constants left out.
```
def lift : W → InverseLimit G f :=
…
```
Mentions: InverseLimit
lemma InverseLimit.lift_def line 449 source
no axioms what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit.InverseSystemHom, Eq, InverseLimit, InverseLimit.lift, Subtype.mk
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
def InverseLimit.liftMonoidHom MonoidHom version of lift G f maps inverseSystemHom line 458 source
Source documentation
MonoidHom version of lift G f maps inverseSystemHom

standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit.InverseSystemHom, Group, MonoidHomClass, MonoidHom, InverseLimit
Proof uses: MonoidHom.mk, OneHom.mk, InverseLimit.lift
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def liftMonoidHom [∀ i, Group (G i)] [∀ i j h, MonoidHomClass (T h) (G j) (G i)]
    [Group W] [∀ i, MonoidHomClass (M i) W (G i)] :
    W →* InverseLimit G f where
…
```
Mentions: InverseLimit
def InverseLimit.liftRingHom RingHom version of lift G f maps inverseSystemHom line 470 source
Source documentation
RingHom version of lift G f maps inverseSystemHom

standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit.InverseSystemHom, Ring, RingHomClass, RingHom, InverseLimit
Proof uses: RingHom.mk, MonoidHom.mk, OneHom.mk, InverseLimit.lift
16 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def liftRingHom [∀ i, Ring (G i)] [∀ i j h, RingHomClass (T h) (G j) (G i)]
    [Ring W] [∀ i, RingHomClass (M i) W (G i)] :
    W →+* InverseLimit G f where
…
```
Mentions: InverseLimit
def InverseLimit.liftLinearMap LinearMap version of lift G f maps inverseSystemHom line 484 source
Source documentation
LinearMap version of lift G f maps inverseSystemHom

standard axioms: Quot.sound, propext what this means
Statement uses: Preorder, LE.le, FunLike, InverseLimit.InverseSystemHom, Ring, AddCommGroup, Module, LinearMapClass, LinearMap, RingHom.id, InverseLimit, RingHom
Proof uses: LinearMap.mk, AddHom.mk, InverseLimit.lift
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def liftLinearMap {R : Type*} [Ring R]
    [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)] [∀ i j h, LinearMapClass (T h) R (G j) (G i)]
    [AddCommGroup W] [Module R W] [∀ i, LinearMapClass (M i) R W (G i)] :
    W →ₗ[R] InverseLimit G f where
…
```
Mentions: InverseLimit