Documentation

TauCeti.Topology.Algebra.RestrictedProduct.Congr.Right

Changing the factors of a restricted product #

A family of multiplicative equivalences induces an equivalence of restricted products when it carries the reference subgroups bijectively onto one another at all but finitely many indices. The Set.BijOn hypothesis supplies both the forward and inverse restrictedness conditions; a one-sided Set.MapsTo hypothesis would only produce a homomorphism in one direction. It cannot be weakened: for coordinatewise equivalences that eventually map the reference subgroups into one another, the induced homomorphism is surjective exactly when they are eventually bijections of the reference subgroups, and the file ends with a family of identity maps for which it is not.

The algebraic construction is adapted from MulEquiv.restrictedProductCongrRight in the FLT project (ImperialCollegeLondon/FLT, file FLT/Mathlib/Topology/Algebra/RestrictedProduct/Equiv.lean, source commit a9efe585de92be60be84ac1d14ced5a1b0944333, Apache 2.0), by Kevin Buzzard and Salvatore Mercuri. The continuity results are the two directions of FLT's ContinuousMulEquiv.restrictedProductCongrRight.

The general statements have additive counterparts, such as addRestrictedProductCongrRight.

References #

source
def TauCeti.restrictedProductCongrRight {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) :
RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite ≃* RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The multiplicative equivalence of restricted products induced by coordinatewise equivalences that eventually carry the reference subgroups bijectively onto one another.

Instances For
    source
    def TauCeti.addRestrictedProductCongrRight {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i ≃+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) :
    RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite ≃+ RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

    The additive equivalence of restricted products induced by coordinatewise additive equivalences that eventually carry the reference subgroups bijectively onto one another.

    Instances For
      source
      @[simp]
      theorem TauCeti.restrictedProductCongrRight_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) :
      ((restrictedProductCongrRight U U' φ hφ) x) i = (φ i) (x i)

      The forward change-of-factors equivalence applies the given equivalence in each coordinate.

      source
      @[simp]
      theorem TauCeti.addRestrictedProductCongrRight_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i ≃+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) :
      ((addRestrictedProductCongrRight U U' φ hφ) x) i = (φ i) (x i)
      source
      @[simp]
      theorem TauCeti.restrictedProductCongrRight_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (y : RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite) (i : ι) :
      ((restrictedProductCongrRight U U' φ hφ).symm y) i = (φ i).symm (y i)

      The inverse change-of-factors equivalence applies the inverse equivalence in each coordinate.

      source
      @[simp]
      theorem TauCeti.addRestrictedProductCongrRight_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i ≃+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (y : RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite) (i : ι) :
      ((addRestrictedProductCongrRight U U' φ hφ).symm y) i = (φ i).symm (y i)
      source
      theorem TauCeti.map_integralSubgroup_restrictedProductCongrRight {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ (i : ι), Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) :
      Subgroup.map (↑(restrictedProductCongrRight U U' φ ⋯)) (integralSubgroup U) = integralSubgroup U'

      A componentwise equivalence which carries the reference subgroup bijectively at every index carries the everywhere-integral subgroup onto the everywhere-integral subgroup. The hypothesis is deliberately pointwise, rather than eventual: the latter only identifies the ambient restricted products and is insufficient for this conclusion.

      source
      theorem TauCeti.continuous_restrictedProductCongrRight {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (hcont : ∀ (i : ι), Continuous ⇑(φ i)) :
      Continuous ⇑(restrictedProductCongrRight U U' φ hφ)

      The forward change-of-factors equivalence is continuous when its coordinate maps are continuous.

      source
      theorem TauCeti.continuous_addRestrictedProductCongrRight {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i ≃+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (hcont : ∀ (i : ι), Continuous ⇑(φ i)) :
      Continuous ⇑(addRestrictedProductCongrRight U U' φ hφ)
      source
      theorem TauCeti.continuous_restrictedProductCongrRight_symm {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (hcont : ∀ (i : ι), Continuous ⇑(φ i).symm) :
      Continuous ⇑(restrictedProductCongrRight U U' φ hφ).symm

      The inverse change-of-factors equivalence is continuous when the inverse coordinate maps are continuous.

      source
      theorem TauCeti.continuous_addRestrictedProductCongrRight_symm {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i ≃+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)) (hcont : ∀ (i : ι), Continuous ⇑(φ i).symm) :
      Continuous ⇑(addRestrictedProductCongrRight U U' φ hφ).symm
      source
      theorem TauCeti.restrictedProductMap_surjective_iff_eventually_bijOn {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i ≃* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) :
      Function.Surjective ⇑(restrictedProductMap U U' (fun (i : ι) => (φ i).toMonoidHom) hφ) ↔ ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)

      For coordinatewise equivalences that eventually map the reference subgroups into one another, the induced homomorphism of restricted products is surjective exactly when the equivalences are eventually bijections of the reference subgroups. So the Set.BijOn hypothesis of restrictedProductCongrRight is not only sufficient but necessary.

      source
      theorem TauCeti.addRestrictedProductMap_surjective_iff_eventually_bijOn {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i ≃+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) :
      Function.Surjective ⇑(addRestrictedProductMap U U' (fun (i : ι) => (φ i).toAddMonoidHom) hφ) ↔ ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(U i) ↑(U' i)
      source
      theorem TauCeti.not_forall_restrictedProductMap_surjective :
      ¬∀ (U U' : ℕ → Subgroup (Multiplicative ℤ)) (φ : ℕ → Multiplicative ℤ ≃* Multiplicative ℤ) (hφ : ∀ᶠ (i : ℕ) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)), Function.Surjective ⇑(restrictedProductMap U U' (fun (i : ℕ) => (φ i).toMonoidHom) hφ)

      Coordinatewise equivalences that merely map the reference subgroups into one another need not induce an equivalence of restricted products. The witness uses identity maps on Multiplicative ℤ, with every source reference subgroup ⊥ and every target reference subgroup ⊤: the induced map is the inclusion of the finitely supported elements into the full product, which is not surjective.