Splitting a restricted product over a sum of index types #
A restricted product indexed by ι₁ ⊕ ι₂ is the product of the restricted products over the two
summands. The factors need only carry a multiplication and the reference sets need only be closed
under it (MulMemClass), so the splitting is a MulEquiv for submonoids and subgroups alike.
For a filter 𝓕 on ι₁ ⊕ ι₂ the summand filters are the comaps 𝓕.comap Sum.inl and
𝓕.comap Sum.inr, and the algebraic content is that 𝓕 is recovered from them
(Filter.map_comap_inl_sup_map_comap_inr), so the restrictedness conditions match up in both
directions; the equivalence restrictedProductSum is the restriction of
Equiv.sumPiEquivProdPi to the restricted subtypes. It takes the two summand filters as
arguments together with the equations identifying them with the comaps, so that each can be given
in its preferred form: for the cofinite filter both comaps are cofinite again, because Sum.inl
and Sum.inr are injective (Function.Injective.comap_cofinite_eq). The summand filters need not
be cofinite in general: for 𝓕 = 𝓟 (Set.range Sum.inl) the second comap is ⊥, and the right
factor is the unrestricted product Π j, G (Sum.inr j).
The forward map is continuous for every filter and every reference family
(continuous_restrictedProductSum). The inverse is a map out of a product of two restricted
products, and its continuity depends on the filter and on the reference family. For a principal
filter it is continuous for every family (continuous_restrictedProductSum_symm_of_principal),
and hence so is its composite with the inclusions of principal stages
(continuous_restrictedProductSum_symm_comp_prodMap_inclusion). For the cofinite filter,
Mathlib's universal property with parameters passes from the stages to the restricted products
when the reference subsets are open: over both summands (continuous_restrictedProductSum_symm,
the openness hypothesis under which RestrictedProduct.isTopologicalGroup holds), or over the
right summand alone when the left summand is finite
(continuous_restrictedProductSum_symm_of_finite_left). Under either hypothesis
restrictedProductSum is a homeomorphism. Openness cannot be dropped altogether:
not_continuous_restrictedProductSum_symm, in
TauCeti.Topology.Algebra.RestrictedProduct.NotContinuousMul, exhibits a family with trivial
reference subgroups for which the inverse is discontinuous.
Everything here is also stated for additive structures (addRestrictedProductSum, …).
References #
- N. Bourbaki, General Topology.
- A. Weil, Basic Number Theory.
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.
Instances For
An additive 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.
Instances For
The left component of the splitting is the restriction of coordinates to ι₁.
The left component of the
additive splitting is the restriction of coordinates to ι₁.
The right component of the splitting is the restriction of coordinates to ι₂.
The right component of the
additive splitting is the restriction of coordinates to ι₂.
The inverse of the splitting reads its Sum.inl coordinates off the left factor.
The inverse of the additive
splitting reads its Sum.inl coordinates off the left factor.
The inverse of the splitting reads its Sum.inr coordinates off the right factor.
The inverse of the additive
splitting reads its Sum.inr coordinates off the right factor.
The splitting over a sum is continuous for every filter and every reference family; unlike its inverse, it needs no hypothesis on either.
The additive splitting over a sum is continuous for every filter and every reference family; unlike its inverse, it needs no hypothesis on either.
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.
For a principal filter on
ι₁ ⊕ ι₂ the inverse of the additive 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.
On principal stages the inverse of the splitting over a sum is continuous for every filter and every reference family: for the cofinite filter, openness of the reference subsets is needed only to pass from the stages to the restricted products themselves.
On principal stages the inverse of the additive splitting over a sum is continuous for every filter and every reference family: for the cofinite filter, openness of the reference subsets is needed only to pass from the stages to the restricted products themselves.
The inverse of the splitting over a sum, for the cofinite filter, is continuous when every
reference subset is open. This is the same openness hypothesis under which Mathlib's
RestrictedProduct.isTopologicalGroup holds; the forward direction
continuous_restrictedProductSum needs no such hypothesis.
The inverse of the additive splitting over
a sum, for the cofinite filter, is continuous when every reference subset is open. This is the
same openness hypothesis under which Mathlib's RestrictedProduct.isTopologicalAddGroup holds; the
forward direction continuous_addRestrictedProductSum needs no such hypothesis.
The inverse of the splitting over a sum, for the cofinite filter, is continuous when the left summand is finite and every reference subset over the right summand is open; the reference subsets over the finite summand need not be open.
The inverse of the additive splitting over a sum, for the cofinite filter, is continuous when the left summand is finite and every reference subset over the right summand is open; the reference subsets over the finite summand need not be open.