NormalizedDenseSubgroup.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A dense countable subgroup preserved by one normalizer

Starting with a countable dense set, add all its integer conjugates by the chosen normalizer and generate a subgroup. This keeps countability and density while ensuring that the same invariant sigma algebra is available for both ergodic decomposition and normalizer covariance.

def OAI.DukePrimeDegree.integerConjugates line 21
lemma OAI.DukePrimeDegree.integerConjugates_normalizer line 24

theorem OAI.DukePrimeDegree.exists_countable_dense_normalized_subgroup line 40

Source documentation

An actual ambient normalizer can be retained when passing to a countable dense subgroup of a given topological subgroup.

theorem exists_countable_dense_normalized_subgroup
    {G : Type*} [Group G] [TopologicalSpace G]
    (H : Subgroup G) [TopologicalSpace.SeparableSpace H]
    (a : G) (ha : a ∈ Subgroup.normalizer (H : Set G)) :
    ∃ (S : Subgroup G) (hSH : S ≤ H), Countable S ∧
      DenseRange (fun h : S => (⟨h.val, hSH h.property⟩ : H)) ∧
      a ∈ Subgroup.normalizer (S : Set G) := by
…