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.lean, 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.

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

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

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

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

@[implicit_reducible]

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

@[reducible, inline]

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

Constructor for RestrictedProduct.

@[simp]

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

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]_[𝓕].

@[simp]

theorem RestrictedProduct.structureMap_apply {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} {x : (i : ι) → ↑(A i)} (i : ι) : (structureMap R A 𝓕 x) 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.

@[simp]

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

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}

@[simp]

theorem RestrictedProduct.coe_comp_inclusion {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) : DFunLike.coe ∘ inclusion R A h = DFunLike.coe

theorem RestrictedProduct.image_coe_preimage_inclusion_subset {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) (U : Set (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) 𝓕)) : DFunLike.coe '' (inclusion R A h ⁻¹' U) ⊆ DFunLike.coe '' U

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}

@[simp]

theorem RestrictedProduct.coe_comp_structureMap {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι} : DFunLike.coe ∘ structureMap R A 𝓕 = fun (x : (i : ι) → ↑(A i)) (i : ι) => ↑(x 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.

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[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

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[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

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[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

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[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

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[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

@[implicit_reducible]

instance RestrictedProduct.instPow {ι : 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)) 𝓕) ℕ

@[implicit_reducible]

instance RestrictedProduct.instNSMul {ι : 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)] : SMul ℕ (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

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

theorem RestrictedProduct.nsmul_apply {ι : 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)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℕ) (i : ι) : (n • x) i = n • x i

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance RestrictedProduct.instZPow {ι : 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)) 𝓕) ℤ

@[implicit_reducible]

instance RestrictedProduct.instZSMul {ι : 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)] : SMul ℤ (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

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

theorem RestrictedProduct.zsmul_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 : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) (n : ℤ) (i : ι) : (n • x) i = n • x i

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

@[implicit_reducible]

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)) 𝓕)

def RestrictedProduct.coeMonoidHom {ι : 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)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕 →* (i : ι) → R i

The coercion from the restricted product of monoids A i to the (normal) product is a monoid homomorphism.

def RestrictedProduct.coeAddMonoidHom {ι : 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)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕 →+ (i : ι) → R i

The coercion from the restricted product of additive monoids A i to the (normal) product is an additive monoid homomorphism.

@[implicit_reducible]

instance RestrictedProduct.instModuleCoeOfSMulMemClass {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {R₀ : Type u_4} [Semiring R₀] [(i : ι) → AddCommMonoid (R i)] [(i : ι) → Module R₀ (R i)] [∀ (i : ι), AddSubmonoidClass (S i) (R i)] [∀ (i : ι), SMulMemClass (S i) R₀ (R i)] : Module R₀ (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)

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.

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.

@[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.

@[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.mapAlong {ι₁ : 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.mapAlong 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 mapAlongMonoidHom, mapAlongAddMonoidHom and mapAlongRingHom for variants.

@[simp]

theorem RestrictedProduct.mapAlong_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 : ι₂) : (mapAlong R₁ R₂ f hf φ hφ x) j = φ j (x (f j))

def RestrictedProduct.map {ι : Type u_1} {𝓕 : Filter ι} {G : ι → Type u_9} {H : ι → Type u_10} {C : (i : ι) → Set (G i)} {D : (i : ι) → Set (H i)} (φ : (i : ι) → G i → H i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.MapsTo (φ i) (C i) (D i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) 𝓕) : RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => D i) 𝓕

The maps between restricted products over a fixed index type, given maps on the factors.

@[simp]

theorem RestrictedProduct.map_apply {ι : Type u_1} {𝓕 : Filter ι} {G : ι → Type u_9} {H : ι → Type u_10} {C : (i : ι) → Set (G i)} {D : (i : ι) → Set (H i)} (φ : (i : ι) → G i → H i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.MapsTo (φ i) (C i) (D i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) 𝓕) (j : ι) : (map φ hφ x) j = φ j (x j)

def RestrictedProduct.mapAlongMonoidHom {ι₁ : 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]_[𝓕₂] of monoids, RestrictedProduct.mapAlongMonoidHom 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.

def RestrictedProduct.mapAlongAddMonoidHom {ι₁ : 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]_[𝓕₂] of additive monoids, RestrictedProduct.mapAlongAddMonoidHom gives an 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.

@[simp]

theorem RestrictedProduct.mapAlongMonoidHom_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 : ι₂) : ((mapAlongMonoidHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))

@[simp]

theorem RestrictedProduct.mapAlongAddMonoidHom_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 : ι₂) : ((mapAlongAddMonoidHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))

def RestrictedProduct.mapAlongRingHom {ι₁ : 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 of rings Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂], RestrictedProduct.mapAlongRingHom 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.

@[simp]

theorem RestrictedProduct.mapAlongRingHom_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 : ι₂) : ((mapAlongRingHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))

def RestrictedProduct.mulSingle {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) (x : G i) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(A i)) Filter.cofinite

The function supported at i, with value x there, and 1 elsewhere.

def RestrictedProduct.single {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) (x : G i) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(A i)) Filter.cofinite

The function supported at i, with value x there, and 0 elsewhere.

@[simp]

theorem RestrictedProduct.coe_mulSingle_apply {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) (x : G i) (j : ι) : (mulSingle A i x) j = Pi.mulSingle i x j

@[simp]

theorem RestrictedProduct.coe_single_apply {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) (x : G i) (j : ι) : (single A i x) j = Pi.single i x j

theorem RestrictedProduct.comp_mulSingle {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) : DFunLike.coe ∘ mulSingle A i = Pi.mulSingle i

theorem RestrictedProduct.comp_single {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) : DFunLike.coe ∘ single A i = Pi.single i

theorem RestrictedProduct.mulSingle_injective {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) : Function.Injective (mulSingle A i)

theorem RestrictedProduct.single_injective {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) : Function.Injective (single A i)

theorem RestrictedProduct.mulSingle_inj {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) {x y : G i} : mulSingle A i x = mulSingle A i y ↔ x = y

theorem RestrictedProduct.single_inj {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) {x y : G i} : single A i x = single A i y ↔ x = y

theorem RestrictedProduct.mulSingle_eq_same {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) (r : G i) : (mulSingle A i r) i = r

theorem RestrictedProduct.single_eq_same {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) (r : G i) : (single A i r) i = r

theorem RestrictedProduct.mulSingle_eq_of_ne {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] {i j : ι} (r : G i) (h : j ≠ i) : (mulSingle A i r) j = 1

theorem RestrictedProduct.single_eq_of_ne {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] {i j : ι} (r : G i) (h : j ≠ i) : (single A i r) j = 0

theorem RestrictedProduct.mulSingle_eq_of_ne' {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] {i j : ι} (r : G i) (h : i ≠ j) : (mulSingle A i r) j = 1

theorem RestrictedProduct.single_eq_of_ne' {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] {i j : ι} (r : G i) (h : i ≠ j) : (single A i r) j = 0

@[simp]

theorem RestrictedProduct.mulSingle_one {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) : mulSingle A i 1 = 1

@[simp]

theorem RestrictedProduct.single_zero {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) : single A i 0 = 0

@[simp]

theorem RestrictedProduct.mulSingle_eq_one_iff {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) {x : G i} : mulSingle A i x = 1 ↔ x = 1

@[simp]

theorem RestrictedProduct.single_eq_zero_iff {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) {x : G i} : single A i x = 0 ↔ x = 0

theorem RestrictedProduct.mulSingle_ne_one_iff {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → One (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] (i : ι) {x : G i} : mulSingle A i x ≠ 1 ↔ x ≠ 1

theorem RestrictedProduct.single_ne_zero_iff {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Zero (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι) {x : G i} : single A i x ≠ 0 ↔ x ≠ 0

theorem RestrictedProduct.mulSingle_mul {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → MulOneClass (G i)] [∀ (i : ι), OneMemClass (S i) (G i)] [∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r s : G i) : mulSingle A i (r * s) = mulSingle A i r * mulSingle A i s

theorem RestrictedProduct.single_add {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → AddZeroClass (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] [∀ (i : ι), AddMemClass (S i) (G i)] (i : ι) (r s : G i) : single A i (r + s) = single A i r + single A i s

@[simp]

theorem RestrictedProduct.mul_single {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → MulZeroClass (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] [∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r : G i) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(A i)) Filter.cofinite) : single A i (x i * r) = x * single A i r

@[simp]

theorem RestrictedProduct.single_mul {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → MulZeroClass (G i)] [∀ (i : ι), ZeroMemClass (S i) (G i)] [∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r : G i) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(A i)) Filter.cofinite) : single A i (r * x i) = single A i r * x

theorem RestrictedProduct.mulSingle_inv {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Group (G i)] [∀ (i : ι), SubgroupClass (S i) (G i)] (i : ι) (r : G i) : mulSingle A i r⁻¹ = (mulSingle A i r)⁻¹

theorem RestrictedProduct.single_neg {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → AddGroup (G i)] [∀ (i : ι), AddSubgroupClass (S i) (G i)] (i : ι) (r : G i) : single A i (-r) = -single A i r

theorem RestrictedProduct.mulSingle_div {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Group (G i)] [∀ (i : ι), SubgroupClass (S i) (G i)] (i : ι) (r s : G i) : mulSingle A i (r / s) = mulSingle A i r / mulSingle A i s

theorem RestrictedProduct.single_sub {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → AddGroup (G i)] [∀ (i : ι), AddSubgroupClass (S i) (G i)] (i : ι) (r s : G i) : single A i (r - s) = single A i r - single A i s

theorem RestrictedProduct.mulSingle_pow {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Monoid (G i)] [∀ (i : ι), SubmonoidClass (S i) (G i)] (i : ι) (r : G i) (n : ℕ) : mulSingle A i (r ^ n) = mulSingle A i r ^ n

theorem RestrictedProduct.single_nsmul {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → AddMonoid (G i)] [∀ (i : ι), AddSubmonoidClass (S i) (G i)] (i : ι) (r : G i) (n : ℕ) : single A i (n • r) = n • single A i r

theorem RestrictedProduct.mulSingle_zpow {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Group (G i)] [∀ (i : ι), SubgroupClass (S i) (G i)] (i : ι) (r : G i) (n : ℤ) : mulSingle A i (r ^ n) = mulSingle A i r ^ n

theorem RestrictedProduct.single_zsmul {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → AddGroup (G i)] [∀ (i : ι), AddSubgroupClass (S i) (G i)] (i : ι) (r : G i) (n : ℤ) : single A i (n • r) = n • single A i r