Reindexing a restricted product along an equivalence of index types #
An equivalence e : ι' ≃ ι of index types identifies the restricted product of a family G of
types indexed by ι with the restricted product of the pulled-back family j ↦ G (e j) indexed
by ι', coordinatewise: x corresponds to j ↦ x (e j). This is the restricted-product
analogue of Equiv.piCongrLeft. The restrictedness conditions match because e carries the
cofinite filter to the cofinite filter (Function.Injective.comap_cofinite_eq), so no filter
compatibility hypothesis is needed. Both directions are maps out of a single restricted product
and are coordinatewise a homeomorphism of the ambient products on every principal stage, so both
are continuous for every reference family.
The identification is stated at two levels.
restrictedProductCongrLeftEquiv A e, for an arbitrary familyAof reference sets, is the plain equivalence in the orientation ofEquiv.piCongrLeft, from the pulled-back family overι'to the family overι. It is pinned byrestrictedProductCongrLeftEquiv_apply_apply, the value ate jbeing the value atj, and its inverse byrestrictedProductCongrLeftEquiv_symm_apply.restrictedProductCongrLeft U eis the same equivalence as a multiplicative equivalence, for a familyUof reference sets closed under multiplication, andrestrictedProductReindex U eis its inverse,x ↦ (j ↦ x (e j)). The latter is the orientation in which a restricted product is decomposed along a finite set of indices, by reindexing alongEquiv.sumCompl. Both are also stated for additive reference families (addRestrictedProductCongrLeft,addRestrictedProductReindex).
The statement shape and the pinning equation … y (e j) = y j follow the declarations
Equiv.restrictedProductCongrLeft and MulEquiv.restrictedProductCongrLeft of 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, specialised to the cofinite filter on both sides. restrictedProductReindex
and its coordinate lemmas follow FLT's Equiv.restrictedProductCongrLeft', the same equivalence
in the orientation x ↦ (j ↦ x (e j)).
References #
- N. Bourbaki, General Topology.
- A. Weil, Basic Number Theory.
Reindexing a restricted product along an equivalence e : ι' ≃ ι of index types, in the
orientation of Equiv.piCongrLeft: from the restricted product of the pulled-back family over
ι' to the restricted product over ι. The image of y has coordinate y j at e j, and the
inverse sends x to j ↦ x (e j); it is Mathlib's RestrictedProduct.mapAlong along e with
identity coordinate maps.
Instances For
The reindexed element has coordinate y j at e j; as e is surjective, this pins
restrictedProductCongrLeftEquiv.
The inverse of the reindexing equivalence sends x to j ↦ x (e j).
Reindexing is continuous for every reference family.
The inverse of the reindexing equivalence is continuous for every reference family.
Reindexing a restricted product along an equivalence e : ι' ≃ ι of index types, as a
multiplicative equivalence, from the restricted product of the pulled-back family over ι' to
the restricted product over ι. The image of y has coordinate y j at e j.
Instances For
Reindexing a restricted product along an
equivalence e : ι' ≃ ι of index types, as an additive equivalence, from the restricted product
of the pulled-back family over ι' to the restricted product over ι. The image of y has
coordinate y j at e j.
Instances For
The underlying equivalence of restrictedProductCongrLeft is the reindexing equivalence of
the underlying reference sets.
The underlying equivalence of
addRestrictedProductCongrLeft is the reindexing equivalence of the underlying reference sets.
The reindexed element has coordinate y j at e j; as e is surjective, this pins
restrictedProductCongrLeft.
The additively reindexed
element has coordinate y j at e j; as e is surjective, this pins
addRestrictedProductCongrLeft.
The inverse of restrictedProductCongrLeft sends x to j ↦ x (e j).
The inverse of
addRestrictedProductCongrLeft sends x to j ↦ x (e j).
Reindexing a restricted product along an equivalence e : ι' ≃ ι of index types, in the
orientation x ↦ (j ↦ x (e j)): the inverse of restrictedProductCongrLeft.
Instances For
Reindexing a restricted product along an equivalence
e : ι' ≃ ι of index types, as an additive equivalence, in the orientation
x ↦ (j ↦ x (e j)): the inverse of addRestrictedProductCongrLeft.
Instances For
The inverse of restrictedProductCongrLeft is restrictedProductReindex.
The inverse of
addRestrictedProductCongrLeft is addRestrictedProductReindex.
The inverse of restrictedProductReindex is restrictedProductCongrLeft.
The inverse of
addRestrictedProductReindex is addRestrictedProductCongrLeft.
restrictedProductReindex sends x to j ↦ x (e j).
addRestrictedProductReindex
sends x to j ↦ x (e j).
The inverse of restrictedProductReindex has coordinate y j at e j; as e is
surjective, this pins it.
The inverse of
addRestrictedProductReindex has coordinate y j at e j; as e is surjective, this pins it.
restrictedProductCongrLeft is continuous for every reference family.
addRestrictedProductCongrLeft is
continuous for every reference family.
The inverse of restrictedProductCongrLeft is continuous for every reference family.
The inverse of
addRestrictedProductCongrLeft is continuous for every reference family.
restrictedProductReindex is continuous for every reference family.
addRestrictedProductReindex is continuous
for every reference family.
The inverse of restrictedProductReindex is continuous for every reference family.
The inverse of
addRestrictedProductReindex is continuous for every reference family.