Restricted products of sets, groups and rings

We define the restricted product of R : ι → Type* of types, relative to a family of subsets A : (i : ι) → Set (R i) and a filter 𝓕 : Filter ι. This is the set of all x : Π i, R i such that the set {j | x j ∈ A j} belongs to 𝓕. We denote it by Πʳ i, [R i, A i]_[𝓕].

The main case of interest, which we shall refer to as the "classical restricted product", is that of 𝓕 = cofinite. Recall that this is the filter of all subsets of ι, which are cofinite in the sense that they have finite complement. Hence, the associated restricted product is the set of all x : Π i, R i such that x j ∈ A j for all but finitely many js. We denote it simply by Πʳ i, [R i, A i].

Another notable case is that of the principal filter 𝓕 = 𝓟 s corresponding to some subset s of ι. The associated restricted product Πʳ i, [R i, A i]_[𝓟 s] is the set of all x : Π i, R i such that x j ∈ A j for all j ∈ s. Put another way, this is just (Π i ∈ s, A i) × (Π i ∉ s, R i), modulo the obvious isomorphism.

We endow these types with the obvious algebraic structures. We also show various compatibility results.

See also the file Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace , which puts the structure of a topological space on a restricted product of topological spaces.

Main definitions

• RestrictedProduct: the restricted product of a family R of types, relative to a family A of subsets and a filter 𝓕 on the indexing set. This is denoted Πʳ i, [R i, A i]_[𝓕], or simply Πʳ i, [R i, A i] when 𝓕 = cofinite.
• RestrictedProduct.instDFunLike: interpret an element of Πʳ i, [R i, A i]_[𝓕] as an element of Π i, R i using the DFunLike machinery.
• RestrictedProduct.structureMap: the inclusion map from Π i, A i to Πʳ i, [R i, A i]_[𝓕].

Notation

• Πʳ i, [R i, A i]_[𝓕] is RestrictedProduct R A 𝓕.
• Πʳ i, [R i, A i] is RestrictedProduct R A cofinite.

Tags

restricted product, adeles, ideles

Definition and elementary maps

def RestrictedProduct {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) : Type (max u_1 u_2)

The restricted product of a family R : ι → Type* of types, relative to subsets A : (i : ι) → Set (R i) and the filter 𝓕 : Filter ι, is the set of all x : Π i, R i such that the set {j | x j ∈ A j} belongs to 𝓕. We denote it by Πʳ i, [R i, A i]_[𝓕].

The most common use case is with 𝓕 = cofinite, in which case the restricted product is the set of all x : Π i, R i such that x j ∈ A j for all but finitely many j. We denote it simply by Πʳ i, [R i, A i].

Similarly, if S is a principal filter, the restricted product Πʳ i, [R i, A i]_[𝓟 s] is the set of all x : Π i, R i such that ∀ j ∈ S, x j ∈ A j.

Equations

• RestrictedProduct R A 𝓕 = { x : (i : ι) → R i // ∀ᶠ (i : ι) in 𝓕, x i ∈ A i }

def RestrictedProduct.«termΠʳ_,[_,_]_[_]» : Lean.ParserDescr

Πʳ i, [R i, A i]_[𝓕] is RestrictedProduct R A 𝓕.

Equations

• One or more equations did not get rendered due to their size.

def RestrictedProduct.«termΠʳ_,[_,_]_[_]».«delab_app.RestrictedProduct» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def RestrictedProduct.«termΠʳ_,[_,_]» : Lean.ParserDescr

Πʳ i, [R i, A i] is RestrictedProduct R A cofinite.

Equations

• One or more equations did not get rendered due to their size.

def RestrictedProduct.«termΠʳ_,[_,_]».«delab_app.RestrictedProduct» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

instance RestrictedProduct.instDFunLike {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : DFunLike (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕) ι R

Equations

• RestrictedProduct.instDFunLike R A = { coe := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕) (i : ι) => ↑x i, coe_injective' := ⋯ }

theorem RestrictedProduct.ext {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} {x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} (h : ∀ (i : ι), x i = y i) : x = y

theorem RestrictedProduct.ext_iff {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} {x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} : x = y ↔ ∀ (i : ι), x i = y i

theorem RestrictedProduct.range_coe {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : Set.range DFunLike.coe = {x : (a : ι) → R a | ∀ᶠ (i : ι) in 𝓕, x i ∈ A i}

theorem RestrictedProduct.range_coe_principal {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {S : Set ι} : Set.range DFunLike.coe = S.pi A

@[simp]

theorem RestrictedProduct.eventually {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕) : ∀ᶠ (i : ι) in 𝓕, x i ∈ A i

def RestrictedProduct.structureMap {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) (x : (i : ι) → ↑(A i)) : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕

The structure map of the restricted product is the obvious inclusion from Π i, A i into Πʳ i, [R i, A i]_[𝓕].

Equations

• RestrictedProduct.structureMap R A 𝓕 x = ⟨fun (i : ι) => ↑(x i), ⋯⟩

def RestrictedProduct.inclusion {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓖) : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕

If 𝓕 ≤ 𝓖, the restricted product Πʳ i, [R i, A i]_[𝓖] is naturally included in Πʳ i, [R i, A i]_[𝓕]. This is the corresponding map.

Equations

• RestrictedProduct.inclusion R A h x = ⟨⇑x, ⋯⟩

theorem RestrictedProduct.inclusion_eq_id {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) : inclusion R A ⋯ = id

theorem RestrictedProduct.exists_inclusion_eq_of_eventually {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} (hx𝓖 : ∀ᶠ (i : ι) in 𝓖, x i ∈ A i) : ∃ (x' : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓖), inclusion R A h x' = x

theorem RestrictedProduct.exists_structureMap_eq_of_forall {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕} (hx : ∀ (i : ι), ↑x i ∈ A i) : ∃ (x' : (i : ι) → ↑(A i)), structureMap R A 𝓕 x' = x

theorem RestrictedProduct.range_inclusion {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) : Set.range (inclusion R A h) = {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕 | ∀ᶠ (i : ι) in 𝓖, x i ∈ A i}

theorem RestrictedProduct.range_structureMap {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : Set.range (structureMap R A 𝓕) = {f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕 | ∀ (i : ι), ↑f i ∈ A i}

Algebraic instances on restricted products

In this section, we endow the restricted product with its algebraic instances. To avoid any unnecessary coercions, we use subobject classes for the subset B i of each R i.

instance RestrictedProduct.instOneCoeOfOneMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → One (R i)] [∀ (i : ι), OneMemClass (S i) (R i)] : One (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instOneCoeOfOneMemClass R = { one := ⟨fun (x : ι) => 1, ⋯⟩ }

instance RestrictedProduct.instZeroCoeOfZeroMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Zero (R i)] [∀ (i : ι), ZeroMemClass (S i) (R i)] : Zero (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instZeroCoeOfZeroMemClass R = { zero := ⟨fun (x : ι) => 0, ⋯⟩ }

@[simp]

theorem RestrictedProduct.one_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → One (R i)] [∀ (i : ι), OneMemClass (S i) (R i)] (i : ι) : 1 i = 1

@[simp]

theorem RestrictedProduct.zero_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Zero (R i)] [∀ (i : ι), ZeroMemClass (S i) (R i)] (i : ι) : 0 i = 0

instance RestrictedProduct.instInvCoeOfInvMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Inv (R i)] [∀ (i : ι), InvMemClass (S i) (R i)] : Inv (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instInvCoeOfInvMemClass R = { inv := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => (x i)⁻¹, ⋯⟩ }

instance RestrictedProduct.instNegCoeOfNegMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Neg (R i)] [∀ (i : ι), NegMemClass (S i) (R i)] : Neg (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instNegCoeOfNegMemClass R = { neg := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => -x i, ⋯⟩ }

@[simp]

theorem RestrictedProduct.inv_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Inv (R i)] [∀ (i : ι), InvMemClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : x⁻¹ i = (x i)⁻¹

@[simp]

theorem RestrictedProduct.neg_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Neg (R i)] [∀ (i : ι), NegMemClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (-x) i = -x i

instance RestrictedProduct.instMulCoeOfMulMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Mul (R i)] [∀ (i : ι), MulMemClass (S i) (R i)] : Mul (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instMulCoeOfMulMemClass R = { mul := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i * y i, ⋯⟩ }

instance RestrictedProduct.instAddCoeOfAddMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Add (R i)] [∀ (i : ι), AddMemClass (S i) (R i)] : Add (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instAddCoeOfAddMemClass R = { add := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i + y i, ⋯⟩ }

@[simp]

theorem RestrictedProduct.mul_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Mul (R i)] [∀ (i : ι), MulMemClass (S i) (R i)] (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (x * y) i = x i * y i

@[simp]

theorem RestrictedProduct.add_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Add (R i)] [∀ (i : ι), AddMemClass (S i) (R i)] (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (x + y) i = x i + y i

instance RestrictedProduct.instSMulCoeOfSMulMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {G : Type u_4} [(i : ι) → SMul G (R i)] [∀ (i : ι), SMulMemClass (S i) G (R i)] : SMul G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instSMulCoeOfSMulMemClass R = { smul := fun (g : G) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => g • x i, ⋯⟩ }

instance RestrictedProduct.instVAddCoeOfVAddMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {G : Type u_4} [(i : ι) → VAdd G (R i)] [∀ (i : ι), VAddMemClass (S i) G (R i)] : VAdd G (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instVAddCoeOfVAddMemClass R = { vadd := fun (g : G) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => g +ᵥ x i, ⋯⟩ }

@[simp]

theorem RestrictedProduct.smul_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {G : Type u_4} [(i : ι) → SMul G (R i)] [∀ (i : ι), SMulMemClass (S i) G (R i)] (g : G) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (g • x) i = g • x i

@[simp]

theorem RestrictedProduct.vadd_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {G : Type u_4} [(i : ι) → VAdd G (R i)] [∀ (i : ι), VAddMemClass (S i) G (R i)] (g : G) (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (g +ᵥ x) i = g +ᵥ x i

instance RestrictedProduct.instDivCoeOfSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → DivInvMonoid (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] : Div (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instDivCoeOfSubgroupClass R = { div := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i / y i, ⋯⟩ }

instance RestrictedProduct.instSubCoeOfAddSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → SubNegMonoid (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] : Sub (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instSubCoeOfAddSubgroupClass R = { sub := fun (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⟨fun (i : ι) => x i - y i, ⋯⟩ }

@[simp]

theorem RestrictedProduct.div_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → DivInvMonoid (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (x / y) i = x i / y i

@[simp]

theorem RestrictedProduct.sub_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → SubNegMonoid (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] (x y : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (i : ι) : (x - y) i = x i - y i

instance RestrictedProduct.instPowCoeNatOfSubmonoidClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] : Pow (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) ℕ

Equations

• RestrictedProduct.instPowCoeNatOfSubmonoidClass R = { pow := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℕ) => ⟨fun (i : ι) => x i ^ n, ⋯⟩ }

theorem RestrictedProduct.pow_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℕ) (i : ι) : (x ^ n) i = x i ^ n

instance RestrictedProduct.instAddMonoidCoeOfAddSubmonoidClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → AddMonoid (R i)] [∀ (i : ι), AddSubmonoidClass (S i) (R i)] : AddMonoid (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instAddMonoidCoeOfAddSubmonoidClass R = Function.Injective.addMonoid (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instMonoidCoeOfSubmonoidClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] : Monoid (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instMonoidCoeOfSubmonoidClass R = Function.Injective.monoid (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instPowCoeIntOfSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → DivInvMonoid (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] : Pow (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) ℤ

Equations

• RestrictedProduct.instPowCoeIntOfSubgroupClass R = { pow := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℤ) => ⟨fun (i : ι) => x i ^ n, ⋯⟩ }

theorem RestrictedProduct.zpow_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → DivInvMonoid (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℤ) (i : ι) : (x ^ n) i = x i ^ n

instance RestrictedProduct.instNatCastCoeOfAddSubmonoidWithOneClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → AddMonoidWithOne (R i)] [∀ (i : ι), AddSubmonoidWithOneClass (S i) (R i)] : NatCast (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instNatCastCoeOfAddSubmonoidWithOneClass R = { natCast := fun (n : ℕ) => ⟨fun (x : ι) => ↑n, ⋯⟩ }

instance RestrictedProduct.instIntCastCoeOfSubringClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] : IntCast (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instIntCastCoeOfSubringClass R = { intCast := fun (n : ℤ) => ⟨fun (x : ι) => ↑n, ⋯⟩ }

instance RestrictedProduct.instAddGroupCoeOfAddSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → AddGroup (R i)] [∀ (i : ι), AddSubgroupClass (S i) (R i)] : AddGroup (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instAddGroupCoeOfAddSubgroupClass R = Function.Injective.addGroup (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instGroupCoeOfSubgroupClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Group (R i)] [∀ (i : ι), SubgroupClass (S i) (R i)] : Group (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instGroupCoeOfSubgroupClass R = Function.Injective.group (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instRingCoeOfSubringClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] : Ring (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instRingCoeOfSubringClass R = Function.Injective.ring (fun (f : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RestrictedProduct.instCommRingCoeOfSubringClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → CommRing (R i)] [∀ (i : ι), SubringClass (S i) (R i)] : CommRing (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

Equations

• RestrictedProduct.instCommRingCoeOfSubringClass R = { toRing := RestrictedProduct.instRingCoeOfSubringClass R, mul_comm := ⋯ }

def RestrictedProduct.evalMonoidHom {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} (j : ι) [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕 →* R j

RestrictedProduct.evalMonoidHom j is the monoid homomorphism from the restricted product Πʳ i, [R i, B i]_[𝓕] to the component R j.

Equations

• RestrictedProduct.evalMonoidHom R j = { toFun := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => x j, map_one' := ⋯, map_mul' := ⋯ }

def RestrictedProduct.evalAddMonoidHom {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} (j : ι) [(i : ι) → AddMonoid (R i)] [∀ (i : ι), AddSubmonoidClass (S i) (R i)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕 →+ R j

RestrictedProduct.evalAddMonoidHom j is the monoid homomorphism from the restricted product Πʳ i, [R i, B i]_[𝓕] to the component R j.

Equations

• RestrictedProduct.evalAddMonoidHom R j = { toFun := fun (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) => x j, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RestrictedProduct.evalMonoidHom_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (j : ι) : (evalMonoidHom R j) x = x j

def RestrictedProduct.evalRingHom {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} (j : ι) [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕 →+* R j

RestrictedProduct.evalRingHom j is the ring homomorphism from the restricted product Πʳ i, [R i, B i]_[𝓕] to the component R j.

Equations

• RestrictedProduct.evalRingHom R j = { toMonoidHom := RestrictedProduct.evalMonoidHom R j, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RestrictedProduct.evalRingHom_apply {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} [(i : ι) → Ring (R i)] [∀ (i : ι), SubringClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (j : ι) : (evalRingHom R j) x = x j

def RestrictedProduct.map {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) (φ : (j : ι₂) → R₁ (f j) → R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j)) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => A₁ i) 𝓕₁) : RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => A₂ j) 𝓕₂

Given two restricted products Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, A₂ j]_[𝓕₂], RestrictedProduct.map gives a function between them. The data needed is a function f : ι₂ → ι₁ such that 𝓕₂ tends to 𝓕₁ along f, and functions φ j : R₁ (f j) → R₂ j sending A₁ (f j) into A₂ j for an 𝓕₂-large set of j's.

See also mapMonoidHom, mapAddMonoidHom and mapRingHom for variants.

Equations

• RestrictedProduct.map R₁ R₂ f hf φ hφ x = ⟨fun (j : ι₂) => φ j (x (f j)), ⋯⟩

@[simp]

theorem RestrictedProduct.map_apply {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) (φ : (j : ι₂) → R₁ (f j) → R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo (φ j) (A₁ (f j)) (A₂ j)) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => A₁ i) 𝓕₁) (j : ι₂) : (map R₁ R₂ f hf φ hφ x) j = φ j (x (f j))

def RestrictedProduct.mapMonoidHom {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [(i : ι₁) → Monoid (R₁ i)] [(i : ι₂) → Monoid (R₂ i)] [∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)] (φ : (j : ι₂) → R₁ (f j) →* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(B₁ i)) 𝓕₁ →* RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(B₂ j)) 𝓕₂

Given two restricted products Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂], RestrictedProduct.mapMonoidHom gives a monoid homomorphism between them. The data needed is a function f : ι₂ → ι₁ such that 𝓕₂ tends to 𝓕₁ along f, and monoid homomorphisms φ j : R₁ (f j) → R₂ j sending B₁ (f j) into B₂ j for an 𝓕₂-large set of j's.

Equations

• RestrictedProduct.mapMonoidHom R₁ R₂ f hf φ hφ = { toFun := RestrictedProduct.map R₁ R₂ f hf (fun (j : ι₂) (r : R₁ (f j)) => (φ j) r) hφ, map_one' := ⋯, map_mul' := ⋯ }

def RestrictedProduct.mapAddMonoidHom {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [(i : ι₁) → AddMonoid (R₁ i)] [(i : ι₂) → AddMonoid (R₂ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] (φ : (j : ι₂) → R₁ (f j) →+ R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(B₁ i)) 𝓕₁ →+ RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(B₂ j)) 𝓕₂

Given two restricted products Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂], RestrictedProduct.mapAddMonoidHom gives a additive monoid homomorphism between them. The data needed is a function f : ι₂ → ι₁ such that 𝓕₂ tends to 𝓕₁ along f, and additive monoid homomorphisms φ j : R₁ (f j) → R₂ j sending B₁ (f j) into B₂ j for an 𝓕₂-large set of j's.

Equations

• RestrictedProduct.mapAddMonoidHom R₁ R₂ f hf φ hφ = { toFun := RestrictedProduct.map R₁ R₂ f hf (fun (j : ι₂) (r : R₁ (f j)) => (φ j) r) hφ, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RestrictedProduct.mapMonoidHom_apply {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [(i : ι₁) → Monoid (R₁ i)] [(i : ι₂) → Monoid (R₂ i)] [∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)] (φ : (j : ι₂) → R₁ (f j) →* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(B₁ i)) 𝓕₁) (j : ι₂) : ((mapMonoidHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))

@[simp]

theorem RestrictedProduct.mapAddMonoidHom_apply {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [(i : ι₁) → AddMonoid (R₁ i)] [(i : ι₂) → AddMonoid (R₂ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] (φ : (j : ι₂) → R₁ (f j) →+ R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(B₁ i)) 𝓕₁) (j : ι₂) : ((mapAddMonoidHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))

def RestrictedProduct.mapRingHom {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [(i : ι₁) → Ring (R₁ i)] [(i : ι₂) → Ring (R₂ i)] [∀ (i : ι₁), SubringClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubringClass (S₂ i) (R₂ i)] (φ : (j : ι₂) → R₁ (f j) →+* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(B₁ i)) 𝓕₁ →+* RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(B₂ j)) 𝓕₂

Given two restricted products Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂], RestrictedProduct.mapRingHom gives a ring homomorphism between them. The data needed is a function f : ι₂ → ι₁ such that 𝓕₂ tends to 𝓕₁ along f, and ring homomorphisms φ j : R₁ (f j) → R₂ j sending B₁ (f j) into B₂ j for an 𝓕₂-large set of j's.

Equations

• RestrictedProduct.mapRingHom R₁ R₂ f hf φ hφ = { toMonoidHom := RestrictedProduct.mapMonoidHom R₁ R₂ f hf (fun (j : ι₂) => ↑(φ j)) hφ, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RestrictedProduct.mapRingHom_apply {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁) (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [(i : ι₁) → Ring (R₁ i)] [(i : ι₂) → Ring (R₂ i)] [∀ (i : ι₁), SubringClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubringClass (S₂ i) (R₂ i)] (φ : (j : ι₂) → R₁ (f j) →+* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(B₁ i)) 𝓕₁) (j : ι₂) : ((mapRingHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))