FLT/DedekindDomain/FiniteAdeleRing/IsDirectLimitRestricted.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite adele ring as a direct limit

We show that the restricted product defining the finite adele ring of a Dedekind domain is the direct limit of its S-finite-adele subrings, where S ranges over finite sets of finite places.

Imports (8)
Imported by 2 files
  1. instance RestrictedProduct.(instance at line 36) line 36 source
  2. instance RestrictedProduct.instDirectedSystem line 40 source

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

    Statement uses: Filter, SetLike, DirectedSystem, OrderDual, Set, Filter.sets, Membership.mem, RestrictedProduct, Filter.principal, LE.le, RestrictedProduct.inclusion, Filter.monotone_principal

    Proof uses: DirectedSystem.mk, rfl, le_rfl

    26 instances, coercions and auxiliary constants left out.

  3. instance RestrictedProduct.(instance at line 58) line 58 source
  4. instance RestrictedProduct.directed line 62 source

    no axioms what this means

    Statement uses: Filter, IsDirected, OrderDual, Set, Filter.sets, LE.le, Membership.mem

    Proof uses: IsDirected.mk, Exists, And, Subtype.mk, Exists.intro, Inter.inter, Filter.inter_sets, And.intro, Set.inter_subset_left, Set.inter_subset_right

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. instance RestrictedProduct.(instance at line 73) line 73 source
  6. instance RestrictedProduct.instIsDirectLimit line 79 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Filter, CommRing, AddCommGroup, Module, Submodule, Preorder, Nonempty, IsDirected, LE.le, Antitone, Eq, iInf, IsDirectLimit, RestrictedProduct, LinearMap, RingHom.id, RestrictedProduct.inclusionLinearMap, Eq.trans_le, iInf_le

    Proof uses: IsDirectLimit.mk, id, Exists, Membership.mem, Set, Set.ofPred, Filter.Eventually, Eq.rec, Subtype.property, RestrictedProduct.mapAlongLinearMap, LinearMap.id, Iff.mp, Filter.mem_iInf_of_directed, Antitone.directed_ge, Exists.intro, RestrictedProduct.exists_inclusion_eq_of_eventually, Eq.mpr, congrArg, Iff.mpr, iInf_le_iff and 7 more

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  7. instance RestrictedProduct.instIsDirectLimit' line 100 source

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

    Statement uses: Filter, CommRing, AddCommGroup, Module, Submodule, IsDirectLimit, OrderDual, Set, Filter.sets, Membership.mem, RestrictedProduct, Filter.principal, LE.le, LinearMap, RingHom.id, RestrictedProduct.inclusionLinearMap, Filter.monotone_principal, Iff.mpr, Filter.le_principal_iff, Subtype.property

    Proof uses: Filter.eq_iInf_of_mem_iff_exists_mem, Iff.intro, Exists, Exists.intro, Subtype.mk, subset_refl, Filter.mem_of_superset

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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