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

46 declarations, 0 contain sorry, 0 declared as axioms

The patching algebra

Following the Taylor–Wiles–Kisin patching method, we construct the patching algebra attached to a family of local rings R i of uniformly bounded rank: an ultraproduct (along a non-principal ultrafilter F) of the truncations R i / m_i^k.

Imports (9)

Imported by 2 files

class Algebra.UniformlyBoundedRank A family of local rings R i has uniformly bounded rank if for every k there exists a uniform bound on |R i / m(R i)^k| over all i line 45 source
Source documentation
A family of local rings R i has uniformly bounded rank if for every k there exists a uniform bound on |R i / m(R i)^k| over all i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing
2 instances, coercions and auxiliary constants left out.
```
class Algebra.UniformlyBoundedRank : Prop where
…
```
abbrev PatchingAlgebra.Component The k-th component of the patching algebra: the ultraproduct of the rings R i / m(R i)^k along the ultrafilter F line 52 source
Source documentation
The k-th component of the patching algebra: the ultraproduct of the rings R i / m(R i)^k along the ultrafilter F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, Nat
Proof uses: UltraProduct, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal
13 instances, coercions and auxiliary constants left out.
```
abbrev PatchingAlgebra.Component (k : ℕ) := UltraProduct (fun i ↦ R i ⧸ maximalIdeal (R i) ^ k) F
```
Mentions: UltraProduct
instance (instance at line 54) line 54 source
lemma PatchingAlgebra.componentEquiv line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Algebra, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, Ultrafilter, ContinuousSMul, Algebra.TopologicallyFG, Int, Algebra.UniformlyBoundedRank, Nat, Filter.Eventually, Nonempty, AlgEquiv, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow and 1 more
Proof uses: LT.lt, Nat.card, Exists, Algebra.UniformlyBoundedRank.cond, UltraProduct.exists_algEquiv_of_bddAbove_card, Filter.Eventually.of_forall, And, Finite, And.intro, AddSubgroup.quotient_finite_of_isOpen, Submodule.toAddSubgroup, IsLocalRing.isOpen_maximalIdeal_pow'', Submodule.restrictScalars
74 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
instance (instance at line 63) line 63 source
instance (instance at line 67) line 67 source
instance (instance at line 75) line 75 source
instance (instance at line 80) line 80 source
instance (instance at line 85) line 85 source
abbrev PatchingAlgebra.componentMap The transition ring homomorphism between components: Component j → Component k for k ≤ j, induced by R i / m^j → R i / m^k line 90 source
Source documentation
The transition ring homomorphism between components: Component j → Component k for k ≤ j, induced by R i / m^j → R i / m^k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, Nat, LE.le, RingHom, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal
Proof uses: UltraProduct.mapRingHom, Ideal.quotientMap, RingHom.id
27 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
abbrev PatchingAlgebra.componentMap (j k : ℕ) (hjk : k ≤ j) : Component R F j →+* Component R F k :=
…
```
Mentions: PatchingAlgebra.Component
instance (instance at line 94) line 94 source
def PatchingAlgebra.subring Documented declaration: subring line 113 source
Source documentation
The patching algebra is an inverse limit of components; here we construct it explicitly as a subring of the product of components: those families that are compatible under the transition maps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, Subring, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal
Proof uses: Subring.mk, Subsemiring.mk, Submonoid.mk, Subsemigroup.mk, Set.ofPred, LE.le, Eq, RingHom, PatchingAlgebra.componentMap
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def PatchingAlgebra.subring : Subring (Π i, Component R F i) where
…
```
Mentions: PatchingAlgebra.Component
def PatchingAlgebra.subalgebra The patching algebra as a Λ-subalgebra of the product of components line 122 source
Source documentation
The patching algebra as a Λ-subalgebra of the product of components.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Algebra, Ultrafilter, Subalgebra, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal
Proof uses: Subring, PatchingAlgebra.subring, Subalgebra.mk, Subring.toSubsemiring
32 instances, coercions and auxiliary constants left out.
```
def PatchingAlgebra.subalgebra : Subalgebra Λ (Π i, Component R F i) where
…
```
Mentions: PatchingAlgebra.Component
lemma PatchingAlgebra.isClosed_subring line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, IsClosed, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, Subring, PatchingAlgebra.subring
Proof uses: LE.le, Set.ofPred, Eq, RingHom, PatchingAlgebra.componentMap, isClosed_eq, Continuous.comp', continuous_bot, continuous_apply, Eq.mpr, Set.iInter, eq_of_heq, TopologicalSpace, Set, HEq, Eq.refl, HEq.refl, Eq.symm, Set.ext, Iff and 8 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra The patching algebra: the inverse limit of the components R i / m^k glued along the ultrafilter F line 139 source
Source documentation
The patching algebra: the inverse limit of the components R i / m^k glued along the ultrafilter F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter
Proof uses: Subtype, Nat, PatchingAlgebra.Component, Membership.mem, Subring, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring
17 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
def PatchingAlgebra : Type _ := PatchingAlgebra.subring R F
```
Mentions: PatchingAlgebra.subring
instance (instance at line 141) line 141 source
instance (instance at line 144) line 144 source
instance (instance at line 147) line 147 source
instance (instance at line 150) line 150 source
instance (instance at line 153) line 153 source
instance (instance at line 156) line 156 source
instance (instance at line 159) line 159 source
instance (instance at line 162) line 162 source
instance (instance at line 174) line 174 source
instance (instance at line 193) line 193 source
instance (instance at line 208) line 208 source
def PatchingAlgebra.lift A continuous family of ring homomorphisms f i : R∞ →+* R i lifts uniquely to a ring homomorphism R∞ →+* PatchingAlgebra R F line 218 source
Source documentation
A continuous family of ring homomorphisms f i : R∞ →+* R i lifts uniquely to a ring homomorphism R∞ →+* PatchingAlgebra R F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, PatchingAlgebra
Proof uses: RingHom.codRestrict, Nat, UltraProduct, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, Subring, PatchingAlgebra.Component, RingHom.pi, RingHom.comp, UltraProduct.π, Ideal.Quotient.mk, PatchingAlgebra.subring
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def PatchingAlgebra.lift : Rₒₒ →+* PatchingAlgebra R F :=
…
```
Mentions: PatchingAlgebra
lemma PatchingAlgebra.continuous_lift line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, Ultrafilter, Algebra.UniformlyBoundedRank, RingHom, Algebra.TopologicallyFG, Int, Continuous, PatchingAlgebra, PatchingAlgebra.lift
Proof uses: Iff.mpr, TopologicalSpace.induced, Nat, PatchingAlgebra.Component, Membership.mem, Subring, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring, Function.comp, continuous_induced_rng, continuous_pi, LT.lt, Nat.card, Exists, Algebra.UniformlyBoundedRank.cond, UltraProduct.continuous_of_bddAbove_card, Filter.Eventually.of_forall and 11 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma PatchingAlgebra.lift_surjective line 237 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, Ultrafilter, Algebra.UniformlyBoundedRank, RingHom, Algebra.TopologicallyFG, Int, Continuous, Function.Surjective, PatchingAlgebra, PatchingAlgebra.lift
Proof uses: DenseRange, denseRange_inverseLimit, OrderDual, Nat, PatchingAlgebra.Component, LE.le, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.componentMap, continuous_of_discreteTopology, Iff.mpr, Eq, denseRange_discrete, LT.lt, Nat.card, Exists, Algebra.UniformlyBoundedRank.cond, UltraProduct.surjective_of_bddAbove_card and 30 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra.ofPi Auxiliary ring homomorphism from sequences ℕ → ∀ i, R i of representatives modulo the filter F to the product of components, used in the construction of incl line 253 source
Source documentation
Auxiliary ring homomorphism from sequences ℕ → ∀ i, R i of representatives modulo the filter F to the product of components, used in the construction of incl.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal
Proof uses: RingHom.pi, RingHom.comp, eventuallyProd, Bot.bot, Submodule, Ideal.Quotient.mk, Pi.evalRingHom
39 instances, coercions and auxiliary constants left out.
```
def PatchingAlgebra.ofPi :
    (ℕ → Π i, R i) →+* Π k, Component R F k :=
…
```
Mentions: PatchingAlgebra.Component
lemma PatchingAlgebra.ofPi_surjective line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, Function.Surjective, Nat, PatchingAlgebra.Component, RingHom, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.ofPi
Proof uses: Exists, Eq, eventuallyProd, Bot.bot, Submodule, Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, Exists.intro, funext, Eq.mpr, id, congrArg, Eq.symm, eq_of_heq, RingHom.pi, RingHom.comp, Pi.evalRingHom, HEq, DFunLike, HEq.refl and 12 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma PatchingAlgebra.ofPi_apply line 289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, Nat, Eq, PatchingAlgebra.Component, RingHom, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.ofPi, UltraProduct, UltraProduct.π, Ideal.Quotient.mk
Proof uses: rfl
36 instances, coercions and auxiliary constants left out.
def PatchingAlgebra.incl The natural ring homomorphism from the product ∏ i, R i into PatchingAlgebra R F line 295 source
Source documentation
The natural ring homomorphism from the product ∏ i, R i into PatchingAlgebra R F.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, PatchingAlgebra
Proof uses: RingHom.codRestrict, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, Subring, RingHom.comp, PatchingAlgebra.ofPi, RingHom.pi, RingHom.id, PatchingAlgebra.subring
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def PatchingAlgebra.incl :
    (Π i, R i) →+* PatchingAlgebra R F :=
…
```
Mentions: PatchingAlgebra
abbrev PatchingAlgebra.componentMapRingHom Functoriality on components: a family of local ring homomorphisms f i : R i →+* R' i induces a ring homomorphism between the k-th components of the two patching systems line 312 source
Source documentation
Functoriality on components: a family of local ring homomorphisms f i : R i →+* R' i induces a ring homomorphism between the k-th components of the two patching systems.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, IsLocalHom, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal
Proof uses: UltraProduct.mapRingHom, Ideal.quotientMap
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
abbrev PatchingAlgebra.componentMapRingHom (k : ℕ) :
    Component R F k →+* Component R' F k :=
…
```
Mentions: PatchingAlgebra.Component
lemma PatchingAlgebra.componentMapRingHom_surjective line 328 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, IsLocalHom, Function.Surjective, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.componentMapRingHom
Proof uses: UltraProduct.mapRingHom_surjective, Ideal.quotientMap, Eq, Function.comp, Ideal.Quotient.mk, Exists, Function.Surjective.comp, Ideal.Quotient.mk_surjective, Exists.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, Ideal.quotientMap_mk, eq_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra.map Functoriality of PatchingAlgebra in the family of local rings line 339 source
Source documentation
Functoriality of PatchingAlgebra in the family of local rings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, IsLocalHom, PatchingAlgebra
Proof uses: RingHom.restrict, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, Subring, RingHom.pi, RingHom.comp, PatchingAlgebra.componentMapRingHom, Pi.evalRingHom, PatchingAlgebra.subring
27 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def PatchingAlgebra.map :
    PatchingAlgebra R F →+* PatchingAlgebra R' F :=
…
```
Mentions: PatchingAlgebra
lemma PatchingAlgebra.map_apply line 359 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, IsLocalHom, PatchingAlgebra, Nat, Eq, PatchingAlgebra.Component, Membership.mem, Subring, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring, PatchingAlgebra.map, PatchingAlgebra.componentMapRingHom
Proof uses: rfl
42 instances, coercions and auxiliary constants left out.
lemma PatchingAlgebra.map_comp_apply line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, IsLocalHom, PatchingAlgebra, Eq, PatchingAlgebra.map, RingHom.comp
Proof uses: Subtype.ext, Nat, PatchingAlgebra.Component, Membership.mem, Subring, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring, funext, PatchingAlgebra.ofPi, Exists, PatchingAlgebra.ofPi_surjective, of_eq_true, Eq.trans, UltraProduct, UltraProduct.π, Ideal.Quotient.mk, True and 8 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma PatchingAlgebra.map_comp line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingHom, IsLocalHom, Eq, PatchingAlgebra, PatchingAlgebra.map, RingHom.comp
Proof uses: RingHom.ext, PatchingAlgebra.map_comp_apply
14 instances, coercions and auxiliary constants left out.
lemma PatchingAlgebra.map_id line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, Eq, RingHom, PatchingAlgebra, PatchingAlgebra.map, RingHom.id
Proof uses: RingHom.ext, Nat, PatchingAlgebra.Component, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.ofPi, Membership.mem, Subring, PatchingAlgebra.subring, Exists, PatchingAlgebra.ofPi_surjective, Subtype.ext, funext, of_eq_true, Eq.trans, UltraProduct, UltraProduct.π, Ideal.Quotient.mk and 9 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra.mapEquiv A family of ring isomorphisms R i ≃+* R' i lifts to an isomorphism of patching algebras line 401 source
Source documentation
A family of ring isomorphisms R i ≃+* R' i lifts to an isomorphism of patching algebras.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Ultrafilter, RingEquiv, PatchingAlgebra
Proof uses: RingHom, PatchingAlgebra.map, RingEquiv.toRingHom, RingEquiv.mk, Equiv.mk, OneHom.toFun, RingEquiv.symm
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def PatchingAlgebra.mapEquiv (f : ∀ i, R i ≃+* R' i) :
    PatchingAlgebra R F ≃+* PatchingAlgebra R' F where
…
```
Mentions: PatchingAlgebra
lemma RingHom.continuous_of_finite_of_compact line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Semiring, RingHom, TopologicalSpace, CompactSpace, Finite, IsTopologicalRing, T2Space, IsNoetherianRing, ContinuousAdd, Continuous
Proof uses: IsOpen, Ideal, RingHom.ker, AddSubgroup.FiniteIndex, Submodule.toAddSubgroup, HasQuotient.Quotient, AddSubgroup, Finite.of_injective, RingHom.kerLift, RingHom.kerLift_injective, AddSubgroup.finiteIndex_of_finite_quotient, IsClosed, IsCompact.isClosed, IsLocalRing.isCompact_of_isNoetherianRing, AddSubgroup.isOpen_of_isClosed_of_finiteIndex, continuous_of_continuousAt_zero, Eq.mpr, ContinuousAt, OfNat.ofNat, Filter.Tendsto and 25 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma PatchingAlgebra.map_surjective line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, Ultrafilter, Algebra.UniformlyBoundedRank, RingHom, IsLocalHom, Function.Surjective, PatchingAlgebra, PatchingAlgebra.map
Proof uses: Nat, Set, PatchingAlgebra.Component, Set.preimage, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.componentMapRingHom, Singleton.singleton, Membership.mem, Subring, PatchingAlgebra.subring, OrderDual, LE.le, Subtype.mk, PatchingAlgebra.componentMap, Eq, Subtype.property, Eq.mpr and 33 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma PatchingAlgebra.algebraMap_continuous line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ultrafilter, CommRing, IsLocalRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsNoetherianRing, IsLocalRing.IsAdicTopology, Continuous, PatchingAlgebra, RingHom, Algebra.algebraMap
Proof uses: Iff.mpr, TopologicalSpace.induced, Nat, PatchingAlgebra.Component, Membership.mem, Subring, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring, Function.comp, continuous_induced_rng, continuous_pi, RingHom.comp, UltraProduct, UltraProduct.π, RingHom.pi, Ideal.Quotient.mk, Algebra.UniformlyBoundedRank and 8 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma PatchingAlgebra.algebraMap_surjective line 480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ultrafilter, CommRing, IsLocalRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsNoetherianRing, IsLocalRing.IsAdicTopology, Function.Surjective, PatchingAlgebra, RingHom, Algebra.algebraMap
Proof uses: DenseRange, denseRange_inverseLimit, OrderDual, Nat, PatchingAlgebra.Component, LE.le, HasQuotient.Quotient, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.componentMap, continuous_of_discreteTopology, Iff.mpr, Eq, denseRange_discrete, Finite, AddSubgroup.quotient_finite_of_isOpen, Submodule.toAddSubgroup, IsLocalRing.isOpen_maximalIdeal_pow, UltraProduct and 29 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def PatchingAlgebra.constEquiv line 500 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ultrafilter, CommRing, IsLocalRing, TopologicalSpace, IsTopologicalRing, CompactSpace, IsNoetherianRing, IsLocalRing.IsAdicTopology, AlgEquiv, PatchingAlgebra
Proof uses: AlgEquiv.ofBijective, Algebra.ofId
17 instances, coercions and auxiliary constants left out.

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