Module

RestrictedTateModule.lean

Nyll.ProCGroups.Abelian.RestrictedTateModule

16 declarations indexed from sourceView source ↗

Module documentation

Compatible actual torsion families on a multiplicative set of indices

Restricting positive indices to a submonoid preserves products and therefore the actual multiplication transitions. Each coordinate is an actual torsion point, and the topology is the subspace topology of discrete torsion levels.

Imports2

Nyll.ProCGroups.Abelian.FullTateModule
Mathlib.Algebra.Group.Submonoid.Defs

Imported by3

def

restrictedCompatibleTorsionFamilies

L25 ↗

ProCGroups.restrictedCompatibleTorsionFamilies

Documentation

The actual compatible families over a multiplicative set of positive indices.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)

Lean source · full declaration

def restrictedCompatibleTorsionFamilies : AddSubgroup (∀ n : S, torsionLevel M n.1) where
  carrier := {x | ∀ n m : S, torsionTransition M n.1 m.1 (x (n * m)) = x n}
  zero_mem' := fun n m => (torsionTransition M n.1 m.1).map_zero
  add_mem' := by
    intro x y hx hy n m
    change torsionTransition M n.1 m.1 (x (n * m) + y (n * m)) = x n + y n
    rw [map_add, hx n m, hy n m]
  neg_mem' := by
    intro x hx n m
    change torsionTransition M n.1 m.1 (-x (n * m)) = -x n
    rw [map_neg, hx n m]

def

RestrictedTateModule

L38 ↗

ProCGroups.RestrictedTateModule

Documentation

The Tate module formed from the actual torsion levels with indices in S.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)

Lean source · statement

def RestrictedTateModule : Type u

instance

(anonymous instance)

L42 ↗

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule

Lean source · statement

instance : AddCommGroup (RestrictedTateModule M S)

def

projection

L46 ↗

ProCGroups.RestrictedTateModule.projection

Documentation

Projection to the actual torsion group at an allowed index.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule

Lean source · full declaration

def projection (n : S) : RestrictedTateModule M S →+ torsionLevel M n.1 where
  toFun x := x.1 n
  map_zero' := rfl
  map_add' _ _ := rfl

def

evaluation

L52 ↗

ProCGroups.RestrictedTateModule.evaluation

Documentation

Evaluation in the original group of points.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule

Lean source · statement

def evaluation (n : S) : RestrictedTateModule M S →+ M

theorem

ext

L58 ↗

ProCGroups.RestrictedTateModule.ext

Documentation

Compatible families are equal if their actual points at every allowed index agree.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}

Lean source · statement

theorem ext {x y : RestrictedTateModule M S}
    (h : ∀ n : S, evaluation M S n x = evaluation M S n y) : x = y

theorem

evaluation_compatible

L65 ↗

ProCGroups.RestrictedTateModule.evaluation_compatible

Documentation

The defining transitions are multiplication in the original group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}

Lean source · statement

theorem evaluation_compatible (x : RestrictedTateModule M S) (n m : S) :
    (m.1 : ℕ) • evaluation M S (n * m) x = evaluation M S n x

instance

(anonymous instance)

L71 ↗

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)

Lean source · statement

instance (n : ℕ+) : TopologicalSpace (torsionLevel M n)

instance

(anonymous instance)

L74 ↗

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n

Lean source · statement

instance (n : ℕ+) : DiscreteTopology (torsionLevel M n)

instance

(anonymous instance)

L76 ↗

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : TopologicalSpace (RestrictedTateModule M S)

instance

(anonymous instance)

L79 ↗

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : IsTopologicalAddGroup (RestrictedTateModule M S)

instance

(anonymous instance)

L82 ↗

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : T2Space (RestrictedTateModule M S)

instance

(anonymous instance)

L85 ↗

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance : TotallyDisconnectedSpace (RestrictedTateModule M S)

theorem

continuous_projection

L89 ↗

ProCGroups.RestrictedTateModule.continuous_projection

Documentation

Every coordinate projection is continuous for the discrete torsion topology.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

theorem continuous_projection (n : S) : Continuous (projection M S n)

theorem

isClosed_restrictedCompatibleTorsionFamilies

L93 ↗

ProCGroups.RestrictedTateModule.isClosed_restrictedCompatibleTorsionFamilies

Documentation

Compatibility is a closed condition in the product of the actual discrete levels.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

theorem isClosed_restrictedCompatibleTorsionFamilies :
    IsClosed (restrictedCompatibleTorsionFamilies M S :
      Set (∀ n : S, torsionLevel M n.1))

instance

(anonymous instance)

L104 ↗

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups
universe u
variable (M : Type u) [AddCommGroup M] (S : Submonoid ℕ+)
namespace RestrictedTateModule
variable {M S}
variable (M S)
local instance (n : ℕ+) : TopologicalSpace (torsionLevel M n) :=
  FullTateModule.torsionLevelTopology M n
local instance (n : ℕ+) : DiscreteTopology (torsionLevel M n) := ⟨rfl⟩

Lean source · statement

instance [∀ n : S, Finite (torsionLevel M n.1)] : CompactSpace (RestrictedTateModule M S)

Module documentation

Compatible actual torsion families on a multiplicative set of indices

Declarations