Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Deformations_ContinuousSMulDiscrete.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Deformations/RepresentationTheory/ContinuousSMulDiscrete.lean

Continuity of actions on discrete sets: open-orbit-fibre condition

This module introduces a single-field proposition class ContinuousSMulDiscrete G M, for a type G carrying a topology and acting on a bare type M by scalar multiplication with no topology on M required. Its only field isOpen_smul_eq asserts that for all x, y : M the set \{g : G \mid g \cdot x = y\} is open in G; that is, each fibre of each orbit map g \mapsto g \cdot x over a point of M is open. This is exactly continuity of the action when M is given the discrete topology, and the point of the formulation is that it can be imposed on an M that already carries some other (possibly non-discrete) topology.

Four auxiliary results pin the notion down. continuousSMulDiscrete_iff shows that if M is endowed with a topology which is discrete, then ContinuousSMulDiscrete G M holds if and only if the joint action map G \times M \to M is continuous in Mathlib's sense (ContinuousSMul G M); the two directions are recorded separately as a low-priority instance producing ContinuousSMul from the class and as ContinuousSMulDiscrete.of_continuousSMul in the opposite direction. continuousSMulDiscrete_iff_isOpen_stabilizer treats the case of a group G with continuous multiplication acting on M: there the class is equivalent to openness of the stabiliser subgroup \mathrm{Stab}_G(x), as a subset of G, for every x : M, the proof translating an arbitrary fibre \{g \mid g \cdot x = y\} to a stabiliser by left translation (the empty fibre being open trivially). The forward implication alone is isolated as ContinuousSMulDiscrete.isOpen_stabilizer, which needs no continuity of multiplication on G.

Relation to Mathlib

Mathlib has ContinuousSMul, which requires a topology on the acted-upon type; ContinuousSMulDiscrete is the project's variant that dispenses with it, and the module supplies the comparison lemmas and an instance ContinuousSMul whenever the given topology on M is discrete.

Where it is used

The condition packaged here is the usual continuity requirement for an action of a profinite group, such as a Galois group, on a discrete module, stated so that it may be used for modules carrying an unrelated topology; it belongs to the topological infrastructure for Galois deformation theory.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_Deformations_ContinuousSMulDiscrete.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

section

variable {G M : Type*} [TopologicalSpace G] [SMul G M]

class ContinuousSMulDiscrete (G M : Type*) [TopologicalSpace G] [SMul G M] : Prop where
  isOpen_smul_eq (G) (x y : M) : IsOpen { g : G | g • x = y }

lemma continuousSMulDiscrete_iff [TopologicalSpace M] [DiscreteTopology M] :
    ContinuousSMulDiscrete G M ↔ ContinuousSMul G M := by
  refine ⟨fun H ↦ ⟨continuous_discrete_rng.mpr fun y ↦ ?_⟩, fun H ↦ ⟨fun x y ↦ ?_⟩⟩
  · convert_to IsOpen (⋃ x, { g : G | g • x = y } ×ˢ {x})
    · ext; simp
    · exact isOpen_iUnion fun _ ↦
        .prod (ContinuousSMulDiscrete.isOpen_smul_eq _ _ _) (isOpen_discrete _)
  · exact ((isOpen_discrete {y}).preimage continuous_smul).preimage (Continuous.prodMk_left x)

instance (priority := low) [TopologicalSpace M] [DiscreteTopology M]
  [ContinuousSMulDiscrete G M] : ContinuousSMul G M := by
  rwa [← continuousSMulDiscrete_iff]

lemma ContinuousSMulDiscrete.of_continuousSMul [TopologicalSpace M]
    [DiscreteTopology M] [ContinuousSMul G M] : ContinuousSMulDiscrete G M := by
  rwa [continuousSMulDiscrete_iff]

lemma continuousSMulDiscrete_iff_isOpen_stabilizer {G M : Type*} [TopologicalSpace G]
    [Group G] [ContinuousMul G] [MulAction G M] :
    ContinuousSMulDiscrete G M ↔ ∀ x : M, IsOpen (MulAction.stabilizer G x : Set G) := by
  refine ⟨fun H x ↦ ContinuousSMulDiscrete.isOpen_smul_eq _ _ _, fun H ↦ ⟨fun x y ↦ ?_⟩⟩
  obtain h | ⟨g, rfl⟩ := Set.eq_empty_or_nonempty {g : G | g • x = y}
  · exact h ▸ isOpen_empty
  · convert (H x).preimage (Homeomorph.mulLeft g⁻¹).continuous using 1
    ext g'
    simp [mul_smul, inv_smul_eq_iff]

lemma ContinuousSMulDiscrete.isOpen_stabilizer (G : Type*) {M : Type*} [TopologicalSpace G]
    [Group G] [MulAction G M] [ContinuousSMulDiscrete G M] (x : M) :
      IsOpen (MulAction.stabilizer G x : Set G) := ContinuousSMulDiscrete.isOpen_smul_eq _ _ _

end

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).