Restricted products of topological groups and rational diagonals
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
DefinitionTauCeti.awayDecomposition#
For a finite set S of indices, the decomposition of a restricted product as the plain
product of the factors at S times the restricted product away from S, coordinatewise the
identity in both directions: x goes to ((x i)_{i ∈ S}, (x i)_{i ∉ S}), and (y, z) goes to
the element with coordinate y ⟨i, _⟩ at i ∈ S and z ⟨i, _⟩ at i ∉ S.
It is the composite of the reindexing along Equiv.sumCompl (· ∈ S), the splitting over the sum
S ⊕ {i // i ∉ S}, and the collapse of the restricted product over the finite index type S.
TauCeti.awayDecomposition.{u, v} {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (S : Set ι)
(hS : S.Finite) (U : (i : ι) → Subgroup (G i)) :
TauCeti.RestrictedProductGroup U ≃*
TauCeti.RestrictedProductGroupWithFactor ((i : ↑S) → G ↑i) fun j => U ↑j
Uses 1 · Used by 1
TheoremTauCeti.continuous_awayDecomposition_symm#
The inverse of the decomposition is continuous when the reference subgroups away from S are
open; the reference subgroups at S play no role, since the finite factor carries no integrality
condition. Together with continuous_awayDecomposition this makes the decomposition a
homeomorphism for such families.
TauCeti.continuous_awayDecomposition_symm.{u, v} {ι : Type u} {G : ι → Type v}
[(i : ι) → Group (G i)] (S : Set ι) (hS : S.Finite) (U : (i : ι) → Subgroup (G i))
[(i : ι) → TopologicalSpace (G i)] (hU : ∀ i ∉ S, IsOpen ↑(U i)) :
Continuous ⇑(TauCeti.awayDecomposition S hS U).symm
Uses 2
TheoremTauCeti.not_isTopologicalGroup_restrictedProduct_rat_bot#
The restricted product Πʳ n : ℕ, [Multiplicative ℚ, ⊥] is not a topological group: the
hypothesis Fact (∀ i, IsOpen (A i)) of Mathlib's RestrictedProduct.isTopologicalGroup cannot be
dropped.
TauCeti.not_isTopologicalGroup_restrictedProduct_rat_bot :
¬IsTopologicalGroup (RestrictedProduct (fun x => Multiplicative ℚ) (fun x => ↑⊥) Filter.cofinite)
Lean
Formalized in Tau Ceti as TauCeti.not_isTopologicalGroup_restrictedProduct_rat_bot.
Sources
- Tau Ceti documentation:
TauCeti.not_isTopologicalGroup_restrictedProduct_rat_bot - Source of
TauCeti.not_isTopologicalGroup_restrictedProduct_rat_botin TauCeti/Topology/Algebra/RestrictedProduct/NotContinuousMul.lean - Tau Ceti roadmap status: Restricted products of topological groups and rational diagonals
TheoremTauCeti.not_continuous_restrictedProductSum_symm#
The inverse of the splitting restrictedProductSum of a restricted product over a sum of index
types is not continuous in general: for Πʳ k : ℕ ⊕ ℕ, [Multiplicative ℚ, ⊥], with the trivial,
non-open, reference subgroup at every index, it is a discontinuous bijection. The openness
hypothesis of continuous_restrictedProductSum_symm therefore cannot be dropped.
TauCeti.not_continuous_restrictedProductSum_symm :
¬Continuous ⇑(TauCeti.restrictedProductSum (fun x => ⊥) ⋯ ⋯).symm
Lean
Formalized in Tau Ceti as TauCeti.not_continuous_restrictedProductSum_symm.
Sources
Uses 1
DefinitionTauCeti.restrictedProductSum#
A restricted product over ι₁ ⊕ ι₂ with respect to a filter 𝓕 is the product of the
restricted products over the two summands with respect to the comaps of 𝓕 along Sum.inl and
Sum.inr, coordinatewise the identity in both directions.
TauCeti.restrictedProductSum.{u₁, u₂, v, w} {ι₁ : Type u₁} {ι₂ : Type u₂} {G : ι₁ ⊕ ι₂ → Type v}
{S : ι₁ ⊕ ι₂ → Type w} [(k : ι₁ ⊕ ι₂) → Mul (G k)] [(k : ι₁ ⊕ ι₂) → SetLike (S k) (G k)]
[∀ (k : ι₁ ⊕ ι₂), MulMemClass (S k) (G k)] {𝓕 : Filter (ι₁ ⊕ ι₂)} {𝓕₁ : Filter ι₁}
{𝓕₂ : Filter ι₂} (U : (k : ι₁ ⊕ ι₂) → S k) (h₁ : Filter.comap Sum.inl 𝓕 = 𝓕₁)
(h₂ : Filter.comap Sum.inr 𝓕 = 𝓕₂) :
RestrictedProduct (fun k => G k) (fun k => ↑(U k)) 𝓕 ≃*
RestrictedProduct (fun i => G (Sum.inl i)) (fun i => ↑(U (Sum.inl i))) 𝓕₁ ×
RestrictedProduct (fun j => G (Sum.inr j)) (fun j => ↑(U (Sum.inr j))) 𝓕₂
TheoremTauCeti.continuous_restrictedProductSum_symm_of_principal#
For a principal filter on ι₁ ⊕ ι₂ the inverse of the splitting is continuous for every
reference family, so that the splitting is a homeomorphism: the target is a principal stage,
whose topology is induced from the product.
TauCeti.continuous_restrictedProductSum_symm_of_principal.{u₁, u₂, v, w} {ι₁ : Type u₁}
{ι₂ : Type u₂} {G : ι₁ ⊕ ι₂ → Type v} {S : ι₁ ⊕ ι₂ → Type w} [(k : ι₁ ⊕ ι₂) → Mul (G k)]
[(k : ι₁ ⊕ ι₂) → SetLike (S k) (G k)] [∀ (k : ι₁ ⊕ ι₂), MulMemClass (S k) (G k)] {𝓕₁ : Filter ι₁}
{𝓕₂ : Filter ι₂} (U : (k : ι₁ ⊕ ι₂) → S k) [(k : ι₁ ⊕ ι₂) → TopologicalSpace (G k)]
{T : Set (ι₁ ⊕ ι₂)} (hT₁ : Filter.comap Sum.inl (Filter.principal T) = 𝓕₁)
(hT₂ : Filter.comap Sum.inr (Filter.principal T) = 𝓕₂) :
Continuous ⇑(TauCeti.restrictedProductSum U hT₁ hT₂).symm
Lean
Formalized in Tau Ceti as TauCeti.continuous_restrictedProductSum_symm_of_principal.
Sources
Uses 1
TheoremTauCeti.continuous_rationalDiagonal#
The diagonal is continuous when the coordinate maps are continuous and there is one cofinite
set of indices at which every γ is integral. Pointwise eventual integrality alone builds the
map but is not enough for continuity, because the restricted-product topology is finer than the
topology induced from the full product.
TauCeti.continuous_rationalDiagonal.{u, v, w} {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)]
{Γ : Type w} [MulOneClass Γ] [TopologicalSpace Γ] [(i : ι) → TopologicalSpace (G i)]
(φ : (i : ι) → Γ →* G i) (U : (i : ι) → Subgroup (G i))
(h : ∀ (γ : Γ), ∀ᶠ (i : ι) in Filter.cofinite, (φ i) γ ∈ U i)
(hcont : ∀ (i : ι), Continuous ⇑(φ i)) (S : Set ι) (hS : S ∈ Filter.cofinite)
(huniform : ∀ (γ : Γ), ∀ i ∈ S, (φ i) γ ∈ U i) : Continuous ⇑(TauCeti.rationalDiagonal φ U h)
TheoremTauCeti.continuous_eval_and_not_continuous_rationalDiagonal_range_coeMonoidHom#
The uniform integrality set in continuous_rationalDiagonal cannot be dropped. Take
discrete groups with trivial reference subgroups, infinitely many of them nontrivial, and for Γ
the range of the coercion from the restricted product to the full product, that is, the finitely
supported elements, with the topology induced from the full product. The coordinate maps are
continuous and every element of Γ is eventually integral (it is the coercion of an element of
the restricted product), but the diagonal is not continuous:
it would make the restricted-product topology the one induced from the full product,
contradicting not_isInducing_coe_bot.
TauCeti.continuous_eval_and_not_continuous_rationalDiagonal_range_coeMonoidHom.{u, v} {ι : Type u}
{G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)]
[∀ (i : ι), DiscreteTopology (G i)] (hG : {i | Nontrivial (G i)}.Infinite) :
(∀ (i : ι),
Continuous ⇑((Pi.evalMonoidHom G i).comp RestrictedProduct.coeMonoidHom.range.subtype)) ∧
¬Continuous
⇑(TauCeti.rationalDiagonal
(fun i => (Pi.evalMonoidHom G i).comp RestrictedProduct.coeMonoidHom.range.subtype)
(fun x => ⊥) ⋯)
Lean
Formalized in Tau Ceti as TauCeti.continuous_eval_and_not_continuous_rationalDiagonal_range_coeMonoidHom.
Sources
- Tau Ceti documentation:
TauCeti.continuous_eval_and_not_continuous_rationalDiagonal_range_coeMonoidHom - Source of
TauCeti.continuous_eval_and_not_continuous_rationalDiagonal_range_coeMonoidHomin TauCeti/Topology/Algebra/RestrictedProduct/Diagonal.lean - Tau Ceti roadmap status: Restricted products of topological groups and rational diagonals
TheoremTauCeti.restrictedProductMap_surjective_iff#
A componentwise restricted-product homomorphism is surjective exactly when every coordinate map is surjective and, at all but finitely many indices, the coordinate map carries the source reference subgroup onto the target one. Surjectivity of each coordinate map alone is not enough: an element of the target may lie in the target reference subgroups at infinitely many indices where no preimage lies in the source reference subgroup.
TauCeti.restrictedProductMap_surjective_iff.{u, v, w} {ι : 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 ⇑(TauCeti.restrictedProductMap U U' φ hφ) ↔
(∀ (i : ι), Function.Surjective ⇑(φ i)) ∧
∀ᶠ (i : ι) in Filter.cofinite, Set.SurjOn ⇑(φ i) ↑(U i) ↑(U' i)
Uses 1
DefinitionTauCeti.restrictedProductMap#
The componentwise homomorphism of restricted products induced by a family that eventually maps each reference subgroup into the corresponding target subgroup.
TauCeti.restrictedProductMap.{u, v, w} {ι : 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)) :
RestrictedProduct (fun i => G i) (fun i => ↑(U i)) Filter.cofinite →*
RestrictedProduct (fun i => H i) (fun i => ↑(U' i)) Filter.cofinite
DefinitionTauCeti.restrictedProductCongr#
The multiplicative equivalence between the restricted products with respect to two reference families that agree at all but finitely many indices. It is the identity in every coordinate.
TauCeti.restrictedProductCongr.{u, v} {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)]
(U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) :
RestrictedProduct (fun i => G i) (fun i => ↑(U i)) Filter.cofinite ≃*
RestrictedProduct (fun i => G i) (fun i => ↑(U' i)) Filter.cofinite
Used by 1
DefinitionTauCeti.doubleCosetCongr#
Transport of a double-coset space along a change of reference family. The subgroups on the
right are the images of those on the left under restrictedProductCongr, not the integral
subgroups of the new family; see exists_map_integralSubgroup_ne.
TauCeti.doubleCosetCongr.{u, v} {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)]
(U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i)
(Γ K : Subgroup (RestrictedProduct (fun i => G i) (fun i => ↑(U i)) Filter.cofinite)) :
DoubleCoset.Quotient ↑Γ ↑K ≃
DoubleCoset.Quotient ↑(Subgroup.map (↑(TauCeti.restrictedProductCongr U U' h)) Γ)
↑(Subgroup.map (↑(TauCeti.restrictedProductCongr U U' h)) K)
Uses 1
DefinitionTauCeti.addAwayDecomposition#
For a finite set S of indices, the decomposition of a
restricted product of additive groups as the plain product of the factors at S times the
restricted product away from S, coordinatewise the identity in both directions: x goes to
((x i)_{i ∈ S}, (x i)_{i ∉ S}), and (y, z) goes to the element with coordinate y ⟨i, _⟩ at
i ∈ S and z ⟨i, _⟩ at i ∉ S.
It is the composite of the reindexing along Equiv.sumCompl (· ∈ S), the splitting over the sum
S ⊕ {i // i ∉ S}, and the collapse of the restricted product over the finite index type S.
TauCeti.addAwayDecomposition.{u, v} {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)]
(S : Set ι) (hS : S.Finite) (U : (i : ι) → AddSubgroup (G i)) :
TauCeti.RestrictedProductAddGroup U ≃+
TauCeti.RestrictedProductAddGroupWithFactor ((i : ↑S) → G ↑i) fun j => U ↑j
DefinitionTauCeti.addRationalDiagonal#
The diagonal additive homomorphism into a restricted product
induced by a family of additive homomorphisms whose values are eventually in the reference
subgroups. The eventual-integrality evidence h is an argument, not a consequence of the
construction.
TauCeti.addRationalDiagonal.{u, v, w} {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)]
{Γ : Type w} [AddZeroClass Γ] (φ : (i : ι) → Γ →+ G i) (U : (i : ι) → AddSubgroup (G i))
(h : ∀ (γ : Γ), ∀ᶠ (i : ι) in Filter.cofinite, (φ i) γ ∈ U i) :
Γ →+ RestrictedProduct (fun i => G i) (fun i => ↑(U i)) Filter.cofinite
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.