Documentation

TauCeti.Topology.Algebra.RestrictedProduct.Finite

Restricted products over a finite index type #

Over a finite index type the cofinite filter is ⊥, so every element of the plain product is restricted and the restricted product Πʳ i, [G i, U i] is the plain product Π i, G i. This file records that identification as a multiplicative equivalence with its coordinate formulas, proves that it is a homeomorphism for every reference family, and identifies the everywhere-integral subgroup with the product of the reference subgroups.

Everything here is also stated for additive groups (addRestrictedProductOfFinite, …).

This is not Mathlib's RestrictedProduct.homeoTop, which is the ⊤-filter statement and identifies the restricted product with the everywhere-integral product Π i, U i.

References #

source
def TauCeti.restrictedProductOfFinite {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [Finite ι] (U : (i : ι) → Subgroup (G i)) :
RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite ≃* ((i : ι) → G i)

Over a finite index type, the restricted product is the plain product, coordinatewise the identity in both directions.

Instances For
    source
    def TauCeti.addRestrictedProductOfFinite {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [Finite ι] (U : (i : ι) → AddSubgroup (G i)) :
    RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite ≃+ ((i : ι) → G i)

    Over a finite index type, the restricted product of additive groups is the plain product, coordinatewise the identity in both directions.

    Instances For
      source
      @[simp]
      theorem TauCeti.restrictedProductOfFinite_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [Finite ι] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) :
      (restrictedProductOfFinite U) x i = x i

      The finite collapse is the identity on coordinates.

      source
      @[simp]
      theorem TauCeti.addRestrictedProductOfFinite_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [Finite ι] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) :
      (addRestrictedProductOfFinite U) x i = x i

      The additive finite collapse is the identity on coordinates.

      source
      @[simp]
      theorem TauCeti.restrictedProductOfFinite_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [Finite ι] (U : (i : ι) → Subgroup (G i)) (x : (i : ι) → G i) (i : ι) :
      ((restrictedProductOfFinite U).symm x) i = x i

      The inverse of the finite collapse is the identity on coordinates.

      source
      @[simp]
      theorem TauCeti.addRestrictedProductOfFinite_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [Finite ι] (U : (i : ι) → AddSubgroup (G i)) (x : (i : ι) → G i) (i : ι) :
      ((addRestrictedProductOfFinite U).symm x) i = x i

      The inverse of the additive finite collapse is the identity on coordinates.

      source
      @[simp]
      theorem TauCeti.map_restrictedProductOfFinite_integralSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [Finite ι] (U : (i : ι) → Subgroup (G i)) :
      Subgroup.map (↑(restrictedProductOfFinite U)) (integralSubgroup U) = Subgroup.pi Set.univ U

      Over a finite index type, the everywhere-integral subgroup is carried onto the product of the reference subgroups.

      source
      @[simp]
      theorem TauCeti.map_addRestrictedProductOfFinite_integralAddSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [Finite ι] (U : (i : ι) → AddSubgroup (G i)) :
      AddSubgroup.map (↑(addRestrictedProductOfFinite U)) (integralAddSubgroup U) = AddSubgroup.pi Set.univ U

      Over a finite index type, the everywhere-integral additive subgroup is carried onto the product of the reference additive subgroups.

      source
      theorem TauCeti.continuous_restrictedProductOfFinite {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [Finite ι] (U : (i : ι) → Subgroup (G i)) [(i : ι) → TopologicalSpace (G i)] :
      Continuous ⇑(restrictedProductOfFinite U)

      The finite collapse is continuous for every reference family.

      source
      theorem TauCeti.continuous_addRestrictedProductOfFinite {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [Finite ι] (U : (i : ι) → AddSubgroup (G i)) [(i : ι) → TopologicalSpace (G i)] :
      Continuous ⇑(addRestrictedProductOfFinite U)

      The additive finite collapse is continuous for every reference family.

      source
      theorem TauCeti.continuous_restrictedProductOfFinite_symm {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [Finite ι] (U : (i : ι) → Subgroup (G i)) [(i : ι) → TopologicalSpace (G i)] :
      Continuous ⇑(restrictedProductOfFinite U).symm

      The inverse of the finite collapse is continuous for every reference family: on a finite index type the cofinite filter is ⊥, and the ⊥-filter restricted product carries the product topology.

      source
      theorem TauCeti.continuous_addRestrictedProductOfFinite_symm {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [Finite ι] (U : (i : ι) → AddSubgroup (G i)) [(i : ι) → TopologicalSpace (G i)] :
      Continuous ⇑(addRestrictedProductOfFinite U).symm

      The inverse of the additive finite collapse is continuous for every reference family: on a finite index type the cofinite filter is ⊥, and the ⊥-filter restricted product carries the product topology.