Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Mathlib_Topology_Algebra_ContinuousMonoidHom.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Continuous additive and multiplicative equivalences: products, quotients, units

This module collects constructions of continuous isomorphisms for topological groups and monoids. ContinuousAddEquiv.toIntContinuousLinearEquiv turns a continuous additive isomorphism e : M \simeq M_2 of topological abelian groups into a continuous \mathbb{Z}-linear equivalence M \simeq_{L[\mathbb{Z}]} M_2: the underlying map is e viewed as \mathbb{Z}-linear, with continuity of e and of e^{-1} as the two continuity fields. ContinuousAddEquiv.quotientPi concerns a finite index type \iota and a family of topological abelian groups G_i (each a topological additive group) together with subgroups p_i \le G_i; it exhibits a continuous additive isomorphism \bigl(\prod_i G_i\bigr)/\prod_i p_i \simeq \prod_i (G_i/p_i), where the subgroup of the product is AddSubgroup.pi Set.univ p. It is obtained from the imported Submodule.quotientPiContinuousLinearEquiv, which gives the corresponding R-linear homeomorphism for submodules p_i \le G_i over a commutative ring R (the companion Submodule.Quotient.continuousLinearEquiv transports a continuous linear equivalence G \simeq H carrying G' onto H' to a continuous linear equivalence G/G' \simeq H/H'), applied to the \mathbb{Z}-submodules underlying the p_i.

The remaining declarations are multiplicative, each with an additive counterpart generated by to_additive. For a family M_j of topological magmas indexed by a type with a unique element, ContinuousMulEquiv.piUnique is evaluation at the distinguished index, a continuous multiplicative isomorphism \prod_j M_j \simeq M_{\mathrm{default}}. For a decidable predicate p on \iota and topological magmas Y_i, ContinuousMulEquiv.piEquivPiSubtypeProd upgrades the standard homeomorphism \prod_i Y_i \simeq \bigl(\prod_{p(i)} Y_i\bigr) \times \bigl(\prod_{\neg p(i)} Y_i\bigr) to a multiplicative one. ContinuousMulEquiv.units_map sends a continuous multiplicative isomorphism f : M \simeq N of topological monoids to the induced continuous isomorphism M^\times \simeq N^\times of unit groups. Finally, ContinuousMulEquiv.coe_toHomeomorph records that the underlying homeomorphism of such an f has the same underlying function as f.

Relation to Mathlib

These are additions to Mathlib's ContinuousMulEquiv/ContinuousAddEquiv and continuous-linear-equivalence API: continuous refinements of the existing Mathlib equivalences MulEquiv.piUnique, Homeomorph.piEquivPiSubtypeProd, Units.mapEquiv, AddMonoidHom.toIntLinearMap and Submodule.quotientPi, rather than notions specific to this project.

Where it is used

The constructions are general-purpose tools of topological algebra, used when products of topological groups and their quotients by componentwise subgroups have to be compared, and when an index set is split according to a predicate.

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

Source file: Definitions/Def_Mathlib_Topology_Algebra_ContinuousMonoidHom.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_Mathlib_Topology_Algebra_Module_Quotient

section

def ContinuousAddEquiv.toIntContinuousLinearEquiv {M M₂ : Type*} [AddCommGroup M]
    [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) :
    M ≃L[ℤ] M₂ where
  __ := e.toIntLinearEquiv
  continuous_toFun := e.continuous
  continuous_invFun := e.continuous_invFun

def ContinuousAddEquiv.quotientPi {ι : Type*} {G : ι → Type*} [(i : ι) → AddCommGroup (G i)]
    [(i : ι) → TopologicalSpace (G i)]
    [(i : ι) → IsTopologicalAddGroup (G i)]
    [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] :
    ((i : ι) → G i) ⧸ AddSubgroup.pi (_root_.Set.univ) p ≃ₜ+ ((i : ι) → G i ⧸ p i) :=
  (Submodule.quotientPiContinuousLinearEquiv
    (fun (i : ι) => AddSubgroup.toIntSubmodule (p i))).toContinuousAddEquiv

@[to_additive

                                                              ]
def ContinuousMulEquiv.piUnique {ι : Type*} (M : ι → Type*) [(j : ι) → Mul (M j)]
    [(j : ι) → TopologicalSpace (M j)] [Unique ι] :
    ((j : ι) → M j) ≃ₜ* M default where
  __ := MulEquiv.piUnique M
  continuous_toFun := continuous_apply default
  continuous_invFun := by simpa [continuous_pi_iff, Unique.forall_iff] using continuous_id'

@[to_additive piEquivPiSubtypeProd

                                                                  ]
def ContinuousMulEquiv.piEquivPiSubtypeProd {ι : Type*} (p : ι → Prop) (Y : ι → Type*)
    [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Mul (Y i)] [DecidablePred p] :
    ((i : ι) → Y i) ≃ₜ* ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i) :=
  {Homeomorph.piEquivPiSubtypeProd p Y with map_mul' _ _ := rfl}

def ContinuousMulEquiv.units_map {M N : Type*} [TopologicalSpace M] [TopologicalSpace N]
    [Monoid M] [Monoid N] (f : M ≃ₜ* N) : Mˣ ≃ₜ* Nˣ :=
  {
  __ := Units.mapEquiv f
  continuous_toFun := by apply Continuous.units_map _ f.continuous_toFun
  continuous_invFun := by apply Continuous.units_map _ f.continuous_invFun
      }

@[to_additive]
theorem ContinuousMulEquiv.coe_toHomeomorph {M N : Type*} [TopologicalSpace M]
    [TopologicalSpace N] [CommMonoid M] [CommMonoid N]
    (f : M ≃ₜ* N) : f.toHomeomorph = ⇑f := rfl

Statements phrased using this module (0)

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