FLT/Deformations/IsProartinian.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

8 declarations, 0 contain sorry, 0 declared as axioms

Proartinian topological rings

A topological ring is proartinian if it is linearly topologized, complete and Hausdorff, and every open ideal is the open kernel of a continuous homomorphism to a finite (Artinian) ring. We provide the basic API and show that complete Noetherian local rings with finite residue field are proartinian under their adic topology.

Imports (5)
Imported by 2 files
  1. class IsProartinian A topological ring is proartinian if it is linearly topologized, complete hausdorff, and all its discrete quotients are artinian line 34 source

    Source documentation

    A topological ring is proartinian if it is linearly topologized, complete hausdorff, and all its discrete quotients are artinian.

    This is also called the category of "pseudo-compact" rings in section 0 of Exp VII_B of SGA3.

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing

    3 instances, coercions and auxiliary constants left out.

    class IsProartinian : Prop extends IsLinearTopology R R, T0Space R,
    letI := IsTopologicalAddGroup.rightUniformSpace R; CompleteSpace R where
…
  2. lemma isProartinian_iff_isArtinianRing line 41 source

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, DiscreteTopology, Iff, IsProartinian, IsArtinianRing

    Proof uses: Iff.intro, HasQuotient.Quotient, Ideal, Bot.bot, IsProartinian.isArtinianRing_quotient, isOpen_discrete, Function.Surjective.isArtinianRing, RingEquiv, RingEquiv.quotientBot, RingEquiv.surjective, IsProartinian.mk, IsTopologicalAddGroup.rightUniformSpace, IsOpen, inferInstance

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  3. instance (instance at line 48) line 48 source
  4. instance (instance at line 51) line 51 source
  5. lemma isOpen_maximalIdeal_of_isProartinian line 63 source

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, IsLocalRing, IsProartinian, IsOpen, Ideal, IsLocalRing.maximalIdeal

    Proof uses: And, Ideal.IsMaximal, Exists, IsLinearTopology.exists_ideal_isMaximal_and_isOpen, Eq.rec, Eq, Iff.mp, IsLocalRing.isMaximal_iff

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  6. lemma exists_maximalIdeal_pow_le_of_isProartinian line 68 source

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, IsLocalRing, IsProartinian, Ideal, IsOpen, Exists, Nat, LE.le, HPow.hPow, IsLocalRing.maximalIdeal

    Proof uses: dite, Eq, Top.top, Exists.intro, OfNat.ofNat, of_eq_true, Eq.trans, True, congr, congrArg, pow_one, Not, IsArtinianRing, HasQuotient.Quotient, IsProartinian.isArtinianRing_quotient, Nontrivial, Iff.mpr, Ne, Ideal.Quotient.nontrivial_iff, IsLocalRing.of_surjective' and 22 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  7. lemma isContinuous_of_isProartinian_of_isLocalHom line 83 source

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, IsLocalRing, IsLocalRing.IsAdicTopology, RingHom, IsProartinian, IsLocalHom, Continuous

    Proof uses: continuous_of_continuousAt_zero, Eq.mpr, ContinuousAt, OfNat.ofNat, Filter.Tendsto, nhds, id, Eq, congrArg, Filter, map_zero, Ideal, IsOpen, Exists, Nat, And, True, Membership.mem, Set, HPow.hPow and 31 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  8. lemma isLocalHom_of_isContinuous_of_isProartinian line 96 source

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, IsLocalRing, IsProartinian, RingHom, Continuous, IsLocalHom

    Proof uses: IsLocalHom.mk, IsUnit, Classical.byContradiction, Not, Nat, LE.le, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, Ideal.comap, Exists, False, exists_maximalIdeal_pow_le_of_isProartinian, IsOpen.preimage, isOpen_maximalIdeal_of_isProartinian, Ideal.pow_mem_pow, Eq.mpr, id, Eq, congrArg and 2 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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