FLT/Patching/System.lean

GitHub source file

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

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

19 declarations, 0 contain sorry, 0 declared as axioms

Compatibility data for the patching system

The class PatchingAlgebra.smulData packaging the compatibility data between the local rings R i, the modules M i, and a system of open ideals: enough to make the limit modules into modules over the patching algebra.

Imports (3)
Imported by 2 files
  1. instance (instance at line 45) line 45 source
  2. lemma Submodule.map_algebraMap_smul line 59 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, AddCommGroup, Module, Algebra, IsScalarTower, Ideal, Submodule, Eq, HSMul.hSMul, Ideal.map, RingHom, Algebra.algebraMap

    Proof uses: le_antisymm, Eq.mpr, LE.le, Membership.mem, id, congrArg, propext, Submodule.smul_le, Submodule.span_induction, Set.image, Set, And, algebraMap_smul, AddSubmonoid.smul_mem_smul, Submodule.toAddSubmonoid, Eq.rec, OfNat.ofNat, ZeroMemClass.zero_mem, Eq.symm, zero_smul and 11 more

    94 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

  3. lemma maximalIdeal_pow_bound_le_smul_top line 92 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, AddCommGroup, Module, IsScalarTower, TopologicalSpace, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, IsNoetherianRing, IsTopologicalRing, OpenIdeals, LE.le, Submodule, HSMul.hSMul, HPow.hPow and 6 more

    Proof uses: Eq.mpr, Ideal.map, RingHom, Algebra.algebraMap, id, Eq, congrArg, Eq.symm, Submodule.map_algebraMap_smul, Finite, AddSubgroup.quotient_finite_of_isOpen, Submodule.toAddSubgroup, Subtype.property, Module.UniformlyBoundedRank.finite_quotient_smul, Iff.mp, AddSubgroup, Equiv.finite_iff, AddEquiv.toEquiv, QuotientAddGroup.quotientAddEquivOfEq, Eq.refl and 11 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

  4. class PatchingAlgebra.smulData Documented declaration: smulData line 113 source

    Source documentation

    Compatibility data between the local rings R i and modules M i and the open ideals of Λ: consists of an antitone function f : OpenIdeals Λ → ℕ such that m(R i)^(f α) • M i ⊆ α • M i for all i.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, AddCommGroup, Module, IsScalarTower, TopologicalSpace

    15 instances, coercions and auxiliary constants left out.

    class PatchingAlgebra.smulData where
…
  5. instance IsPatchingSystem.isModuleQuotient line 122 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, AddCommGroup, Module, IsScalarTower, TopologicalSpace, PatchingAlgebra.smulData, OpenIdeals, HasQuotient.Quotient, Ideal, HPow.hPow, Nat, IsLocalRing.maximalIdeal, PatchingAlgebra.smulData.f, Submodule, HSMul.hSMul, IsOpen, Top.top

    Proof uses: Module.IsTorsionBySet.module

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  6. instance IsPatchingSystem.isModuleQuotient' line 130 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, AddCommGroup, Module, IsScalarTower, TopologicalSpace, PatchingAlgebra.smulData, OpenIdeals, HasQuotient.Quotient, Ideal, HPow.hPow, Nat, IsLocalRing.maximalIdeal, PatchingAlgebra.smulData.f, Submodule, HSMul.hSMul, IsOpen, Top.top

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

    Open to load the checked before-and-after goal states.

  7. instance (instance at line 136) line 136 source
  8. instance (instance at line 141) line 141 source
  9. instance (instance at line 167) line 167 source
  10. instance (instance at line 177) line 177 source
  11. instance (instance at line 188) line 188 source
  12. instance (instance at line 194) line 194 source
  13. instance (instance at line 224) line 224 source
  14. lemma PatchingAlgebra.faithfulSMul line 246 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, AddCommGroup, Module, IsScalarTower, Ultrafilter, NonarchimedeanRing, T2Space, Algebra.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, IsPatchingSystem and 21 more

    Proof uses: PatchingAlgebra.lift, AlgHom.toRingHom, PatchingAlgebra.lift_surjective, Subtype.ext, Nat, PatchingAlgebra.Component, Membership.mem, Subring, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring, funext, Iff.mpr, UltraProduct, UltraProduct.π, RingHom.pi, RingHom.comp, Ideal.Quotient.mk, Filter.Eventually, UltraProduct.π_eq_iff and 57 more

    151 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

    Open to load the checked before-and-after goal states.

  15. lemma Ultrafilter.eventually_eventually_eq_of_finite line 286 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finite, Ultrafilter, Filter.Eventually, Eq

    Proof uses: Exists, Iff.mp, Ultrafilter.eventually_exists_iff, of_eq_true, Eq.trans, True, congrFun', Filter, congrArg, funext, propext, Iff.intro, Exists.elim, rfl, Exists.intro, eq_self, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem and 4 more

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  16. lemma smul_lemma₀ line 310 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, AddCommGroup, Module, IsScalarTower, Ultrafilter, TopologicalSpace, NonarchimedeanRing, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, IsNoetherianRing, Module.Finite, AlgEquiv, Ideal.map, RingHom and 20 more

    Proof uses: Subtype.ext, OpenIdeals, PatchingModule.Component, IsOpen, Membership.mem, PatchingModule.submodule, funext, Nat, PatchingAlgebra.Component, Subring, HPow.hPow, IsLocalRing.maximalIdeal, PatchingAlgebra.subring, Subtype.mk, PatchingModule.ofPi, Exists, PatchingModule.ofPi_surjective, PatchingAlgebra.ofPi, PatchingAlgebra.ofPi_surjective, LE.le and 78 more

    198 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

    Open to load the checked before-and-after goal states.

  17. lemma smul_lemma₁ line 372 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Ultrafilter, TopologicalSpace, IsLocalRing, IsNoetherianRing, NonarchimedeanRing, T2Space, CompactSpace, AddCommGroup, Module, IsTopologicalRing, IsLocalRing.IsAdicTopology, Algebra, Module.Finite, IsScalarTower, Eq, PatchingModule, LinearEquiv, RingHom.id, PatchingModule.constEquiv and 4 more

    Proof uses: rfl

    62 instances, coercions and auxiliary constants left out.

  18. lemma smul_lemma line 387 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, AddCommGroup, Module, IsScalarTower, Ultrafilter, TopologicalSpace, IsNoetherianRing, NonarchimedeanRing, T2Space, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank, CompactSpace, IsTopologicalRing, IsLocalRing.IsAdicTopology, Module.Finite and 17 more

    Proof uses: Exists, Submodule.Quotient.mk_surjective, LinearEquiv.injective, PatchingModule.constEquiv, Eq.trans, LinearEquiv.symm, LinearMap, LinearEquiv.trans, PatchingModule.quotientEquiv, LinearEquiv.restrictScalars, PatchingModule.mapEquiv, LinearEquiv.apply_symm_apply, Nontrivial, RingHom.domain_nontrivial, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, IsLocalHom, IsLocalHom.of_surjective, Ideal.Quotient.mk_surjective, Eq.mpr and 36 more

    161 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

    Open to load the checked before-and-after goal states.

  19. lemma support_eq_top line 422 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, IsLocalRing, Algebra, TopologicalSpace, IsTopologicalRing, CompactSpace, IsLocalRing.IsAdicTopology, AddCommGroup, Module, IsScalarTower, Ultrafilter, IsNoetherianRing, NonarchimedeanRing, T2Space, Algebra.UniformlyBoundedRank, Module.Free, HasQuotient.Quotient, Ideal, Module.annihilator, Module.UniformlyBoundedRank and 30 more

    Proof uses: Module.Finite, IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Or.inl, False, Filter.NeBot.ne', Subsingleton.elim, Filter, Bot.bot, Eq.refl, Or.inr, Nonempty.some, inferInstance, Module.Finite.equiv, Module.Finite.of_restrictScalars_finite, FaithfulSMul, PatchingAlgebra, PatchingModule and 57 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.