Isomorphisms of restricted products

Restricted products of isomorphic things are isomorphic.

Restricted products of matrices/products/units are isomorphic to matrices/products/units of the restricted product.

Restricted product over a principal filter is isomorphic to a product.

We don't allow topological isomorphisms; they have to go into TopologicalSpace because of imports.

def Equiv.restrictedProductCongrRight {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {A₁ : (i : ι) → Set (R₁ i)} {A₂ : (i : ι) → Set (R₂ i)} {𝓕 : Filter ι} (φ : (i : ι) → R₁ i ≃ R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn (⇑(φ i)) (A₁ i) (A₂ i)) : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => A₁ i) 𝓕 ≃ RestrictedProduct (fun (i : ι) => R₂ i) (fun (i : ι) => A₂ i) 𝓕

The equivalence between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets.

@[simp]

theorem Equiv.restrictedProductCongrRight_symm_apply {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {A₁ : (i : ι) → Set (R₁ i)} {A₂ : (i : ι) → Set (R₂ i)} {𝓕 : Filter ι} (φ : (i : ι) → R₁ i ≃ R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn (⇑(φ i)) (A₁ i) (A₂ i)) (x : RestrictedProduct (fun (i : ι) => R₂ i) (fun (i : ι) => A₂ i) 𝓕) : (restrictedProductCongrRight φ hφ).symm x = RestrictedProduct.map (fun (i : ι) => ⇑(φ i).symm) ⋯ x

@[simp]

theorem Equiv.restrictedProductCongrRight_apply {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {A₁ : (i : ι) → Set (R₁ i)} {A₂ : (i : ι) → Set (R₂ i)} {𝓕 : Filter ι} (φ : (i : ι) → R₁ i ≃ R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn (⇑(φ i)) (A₁ i) (A₂ i)) (x : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => A₁ i) 𝓕) : (restrictedProductCongrRight φ hφ) x = RestrictedProduct.map (fun (i : ι) => ⇑(φ i)) ⋯ x

def MulEquiv.restrictedProductCongrRight {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} [(i : ι) → Monoid (R₁ i)] [(i : ι) → Monoid (R₂ i)] [∀ (i : ι), SubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι), SubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} (φ : (i : ι) → R₁ i ≃* R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕 ≃* RestrictedProduct (fun (i : ι) => R₂ i) (fun (i : ι) => ↑(A₂ i)) 𝓕

The MulEquiv between restricted products built from MulEquivs on the factors.

def AddEquiv.restrictedProductCongrRight {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} [(i : ι) → AddMonoid (R₁ i)] [(i : ι) → AddMonoid (R₂ i)] [∀ (i : ι), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι), AddSubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} (φ : (i : ι) → R₁ i ≃+ R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕 ≃+ RestrictedProduct (fun (i : ι) => R₂ i) (fun (i : ι) => ↑(A₂ i)) 𝓕

The AddEquiv between restricted products built from AddEquivs on the factors.

@[simp]

theorem AddEquiv.restrictedProductCongrRight_apply {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} [(i : ι) → AddMonoid (R₁ i)] [(i : ι) → AddMonoid (R₂ i)] [∀ (i : ι), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι), AddSubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} (φ : (i : ι) → R₁ i ≃+ R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) (x : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕) : (restrictedProductCongrRight φ hφ) x = RestrictedProduct.map (fun (i : ι) => ⇑(φ i)) ⋯ x

@[simp]

theorem MulEquiv.restrictedProductCongrRight_apply {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} [(i : ι) → Monoid (R₁ i)] [(i : ι) → Monoid (R₂ i)] [∀ (i : ι), SubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι), SubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} (φ : (i : ι) → R₁ i ≃* R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) (x : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕) : (restrictedProductCongrRight φ hφ) x = RestrictedProduct.map (fun (i : ι) => ⇑(φ i)) ⋯ x

def MulEquiv.restrictedProductUnits {ι : Type u_6} {ℱ : Filter ι} {M : ι → Type u_7} [(i : ι) → Monoid (M i)] {S : ι → Type u_8} [(i : ι) → SetLike (S i) (M i)] [∀ (i : ι), SubmonoidClass (S i) (M i)] {A : (i : ι) → S i} : (RestrictedProduct (fun (i : ι) => M i) (fun (i : ι) => ↑(A i)) ℱ)ˣ ≃* RestrictedProduct (fun (i : ι) => (M i)ˣ) (fun (i : ι) => ↑(Submonoid.ofClass (A i)).units) ℱ

The isomorphism between the units of a restricted product of monoids, and the restricted product of the units of the monoids.

def RingEquiv.restrictedProductCongrRight {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} [(i : ι) → Semiring (R₁ i)] [(i : ι) → Semiring (R₂ i)] [∀ (i : ι), SubsemiringClass (S₁ i) (R₁ i)] [∀ (i : ι), SubsemiringClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} (φ : (i : ι) → R₁ i ≃+* R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕 ≃+* RestrictedProduct (fun (i : ι) => R₂ i) (fun (i : ι) => ↑(A₂ i)) 𝓕

The ring isomorphism between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets.

@[simp]

theorem RingEquiv.restrictedProductCongrRight_apply {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} [(i : ι) → Semiring (R₁ i)] [(i : ι) → Semiring (R₂ i)] [∀ (i : ι), SubsemiringClass (S₁ i) (R₁ i)] [∀ (i : ι), SubsemiringClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} (φ : (i : ι) → R₁ i ≃+* R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) (x : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕) : (restrictedProductCongrRight φ hφ) x = RestrictedProduct.map (fun (i : ι) => ⇑(φ i)) ⋯ x

def LinearEquiv.restrictedProductCongrRight {ι : Type u_1} {R₁ : ι → Type u_2} {R₂ : ι → Type u_3} {S₁ : ι → Type u_4} {S₂ : ι → Type u_5} [(i : ι) → SetLike (S₁ i) (R₁ i)] [(i : ι) → SetLike (S₂ i) (R₂ i)] {𝓕 : Filter ι} {T : Type u_6} [Semiring T] [(i : ι) → AddCommMonoid (R₁ i)] [(i : ι) → AddCommMonoid (R₂ i)] [(i : ι) → Module T (R₁ i)] [(i : ι) → Module T (R₂ i)] [∀ (i : ι), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι), AddSubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι) → S₁ i} {A₂ : (i : ι) → S₂ i} [∀ (i : ι), SMulMemClass (S₁ i) T (R₁ i)] [∀ (i : ι), SMulMemClass (S₂ i) T (R₂ i)] (φ : (i : ι) → R₁ i ≃ₗ[T] R₂ i) (hφ : ∀ᶠ (i : ι) in 𝓕, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ i)) : RestrictedProduct (fun (i : ι) => R₁ i) (fun (i : ι) => ↑(A₁ i)) 𝓕 ≃ₗ[T] RestrictedProduct (fun (i : ι) => R₂ i) (fun (i : ι) => ↑(A₂ i)) 𝓕

The LinearEquiv between restricted products built from LinearEquivs on the factors.

def Equiv.restrictedProductCongrLeft' {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => A₁ i) 𝓕₁ ≃ RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => A₁ (e.symm j)) 𝓕₂

The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

@[simp]

theorem Equiv.restrictedProductCongrLeft'_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => A₁ i) 𝓕₁) : (e.restrictedProductCongrLeft' h) x = ⟨fun (i : ι₂) => x (e.symm i), ⋯⟩

theorem Equiv.restrictedProductCongrLeft'_symm_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (y : RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => A₁ (e.symm j)) 𝓕₂) : (e.restrictedProductCongrLeft' h).symm y = ⟨fun (j : ι₁) => (piCongrLeft' R₁ e).symm (⇑y) j, ⋯⟩

@[simp]

theorem Equiv.restrictedProductCongrLeft'_symm_apply_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (x : RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => A₁ (e.symm j)) 𝓕₂) (j : ι₂) : ((e.restrictedProductCongrLeft' h).symm x) (e.symm j) = x j

def Equiv.restrictedProductCongrLeft {ι₁ : Type u_1} {ι₂ : Type u_2} {R₂ : ι₂ → Type u_5} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₂ : (i : ι₂) → Set (R₂ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) : RestrictedProduct (fun (i : ι₁) => R₂ (e i)) (fun (i : ι₁) => A₂ (e i)) 𝓕₁ ≃ RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => A₂ j) 𝓕₂

The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

@[simp]

theorem Equiv.restrictedProductCongrLeft_apply_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₂ : ι₂ → Type u_5} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₂ : (i : ι₂) → Set (R₂ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (x : RestrictedProduct (fun (i : ι₁) => R₂ (e i)) (fun (i : ι₁) => A₂ (e i)) 𝓕₁) (i : ι₁) : ((e.restrictedProductCongrLeft h) x) (e i) = x i

def MulEquiv.restrictedProductCongrLeft' {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Monoid (R₁ i)] [∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] {A₁ : (i : ι₁) → S₁ i} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃* RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => ↑(A₁ (e.symm j))) 𝓕₂

The multiplicative monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

def AddEquiv.restrictedProductCongrLeft' {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → AddMonoid (R₁ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] {A₁ : (i : ι₁) → S₁ i} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃+ RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => ↑(A₁ (e.symm j))) 𝓕₂

The additive monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

@[simp]

theorem AddEquiv.restrictedProductCongrLeft'_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → AddMonoid (R₁ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] {A₁ : (i : ι₁) → S₁ i} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => (fun (i : ι₁) => ↑(A₁ i)) i) 𝓕₁) : (restrictedProductCongrLeft' e h) x = ⟨fun (i : ι₂) => x (e.symm i), ⋯⟩

@[simp]

theorem MulEquiv.restrictedProductCongrLeft'_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Monoid (R₁ i)] [∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] {A₁ : (i : ι₁) → S₁ i} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => (fun (i : ι₁) => ↑(A₁ i)) i) 𝓕₁) : (restrictedProductCongrLeft' e h) x = ⟨fun (i : ι₂) => x (e.symm i), ⋯⟩

def MulEquiv.restrictedProductCongrLeft {ι₁ : Type u_1} {ι₂ : Type u_2} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₂) → Monoid (R₂ i)] [∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)] {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) : RestrictedProduct (fun (i : ι₁) => R₂ (e i)) (fun (i : ι₁) => ↑(A₂ (e i))) 𝓕₁ ≃* RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The multiplicative monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

def AddEquiv.restrictedProductCongrLeft {ι₁ : Type u_1} {ι₂ : Type u_2} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₂) → AddMonoid (R₂ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) : RestrictedProduct (fun (i : ι₁) => R₂ (e i)) (fun (i : ι₁) => ↑(A₂ (e i))) 𝓕₁ ≃+ RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The additive monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

def RingEquiv.restrictedProductCongrLeft' {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Semiring (R₁ i)] [∀ (i : ι₁), SubsemiringClass (S₁ i) (R₁ i)] {A₁ : (i : ι₁) → S₁ i} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃+* RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => ↑(A₁ (e.symm j))) 𝓕₂

The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

@[simp]

theorem RingEquiv.restrictedProductCongrLeft'_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Semiring (R₁ i)] [∀ (i : ι₁), SubsemiringClass (S₁ i) (R₁ i)] {A₁ : (i : ι₁) → S₁ i} (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => (fun (i : ι₁) => ↑(A₁ i)) i) 𝓕₁) : (restrictedProductCongrLeft' e h) x = ⟨fun (i : ι₂) => x (e.symm i), ⋯⟩

def RingEquiv.restrictedProductCongrLeft {ι₁ : Type u_1} {ι₂ : Type u_2} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₂) → Semiring (R₂ i)] [∀ (i : ι₂), SubsemiringClass (S₂ i) (R₂ i)] {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) : RestrictedProduct (fun (i : ι₁) => R₂ (e i)) (fun (i : ι₁) => ↑(A₂ (e i))) 𝓕₁ ≃+* RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

def LinearEquiv.restrictedProductCongrLeft' {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {T : Type u_7} [Semiring T] {A₁ : (i : ι₁) → S₁ i} [(i : ι₁) → AddCommMonoid (R₁ i)] [(i : ι₁) → Module T (R₁ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₁), SMulMemClass (S₁ i) T (R₁ i)] (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃ₗ[T] RestrictedProduct (fun (j : ι₂) => R₁ (e.symm j)) (fun (j : ι₂) => ↑(A₁ (e.symm j))) 𝓕₂

The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

@[simp]

theorem LinearEquiv.restrictedProductCongrLeft'_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {T : Type u_7} [Semiring T] {A₁ : (i : ι₁) → S₁ i} [(i : ι₁) → AddCommMonoid (R₁ i)] [(i : ι₁) → Module T (R₁ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₁), SMulMemClass (S₁ i) T (R₁ i)] (e : ι₁ ≃ ι₂) (h : 𝓕₂ = Filter.map (⇑e) 𝓕₁) (a✝ : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁) : (restrictedProductCongrLeft' e h) a✝ = ⟨fun (i : ι₂) => a✝ (e.symm i), ⋯⟩

def LinearEquiv.restrictedProductCongrLeft {ι₁ : Type u_1} {ι₂ : Type u_2} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {T : Type u_7} [Semiring T] {A₂ : (i : ι₂) → S₂ i} [(i : ι₂) → AddCommMonoid (R₂ i)] [(i : ι₂) → Module T (R₂ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] [∀ (i : ι₂), SMulMemClass (S₂ i) T (R₂ i)] (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) : RestrictedProduct (fun (i : ι₁) => R₂ (e i)) (fun (i : ι₁) => ↑(A₂ (e i))) 𝓕₁ ≃ₗ[T] RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

def Equiv.restrictedProductCongr {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {R₂ : ι₂ → Type u_5} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃ R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn (⇑(φ i)) (A₁ i) (A₂ (e i))) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => A₁ i) 𝓕₁ ≃ RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => A₂ j) 𝓕₂

The equivalence between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

@[simp]

theorem Equiv.restrictedProductCongr_apply_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {R₂ : ι₂ → Type u_5} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} {e : ι₁ ≃ ι₂} {h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂} {φ : (i : ι₁) → R₁ i ≃ R₂ (e i)} {hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn (⇑(φ i)) (A₁ i) (A₂ (e i))} {x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => A₁ i) 𝓕₁} {i : ι₁} : ((e.restrictedProductCongr h φ hφ) x) (e i) = (φ i) (x i)

@[simp]

theorem Equiv.restrictedProductCongr_symm_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {R₂ : ι₂ → Type u_5} {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {A₁ : (i : ι₁) → Set (R₁ i)} {A₂ : (i : ι₂) → Set (R₂ i)} {e : ι₁ ≃ ι₂} {h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂} {φ : (i : ι₁) → R₁ i ≃ R₂ (e i)} {hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn (⇑(φ i)) (A₁ i) (A₂ (e i))} {x : RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => A₂ j) 𝓕₂} : ⇑((e.restrictedProductCongr h φ hφ).symm x) = fun (a : ι₁) => (φ a).symm (x (e a))

def MulEquiv.restrictedProductCongr {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Monoid (R₁ i)] [(i : ι₂) → Monoid (R₂ i)] [∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃* R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃* RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The multiplicative monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

def AddEquiv.restrictedProductCongr {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → AddMonoid (R₁ i)] [(i : ι₂) → AddMonoid (R₂ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃+ R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃+ RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The additive monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

@[simp]

theorem MulEquiv.restrictedProductCongr_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Monoid (R₁ i)] [(i : ι₂) → Monoid (R₂ i)] [∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃* R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) (a✝ : RestrictedProduct (fun (i : ι₁) => (fun (x : ι₁) => R₁ x) i) (fun (i : ι₁) => (fun (i : ι₁) => ↑(A₁ i)) i) 𝓕₁) : (restrictedProductCongr e h φ hφ) a✝ = (e.restrictedProductCongrLeft h) (RestrictedProduct.map (fun (i : ι₁) => ⇑(φ i)) ⋯ a✝)

@[simp]

theorem AddEquiv.restrictedProductCongr_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → AddMonoid (R₁ i)] [(i : ι₂) → AddMonoid (R₂ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃+ R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) (a✝ : RestrictedProduct (fun (i : ι₁) => (fun (x : ι₁) => R₁ x) i) (fun (i : ι₁) => (fun (i : ι₁) => ↑(A₁ i)) i) 𝓕₁) : (restrictedProductCongr e h φ hφ) a✝ = (e.restrictedProductCongrLeft h) (RestrictedProduct.map (fun (i : ι₁) => ⇑(φ i)) ⋯ a✝)

def RingEquiv.restrictedProductCongr {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Semiring (R₁ i)] [(i : ι₂) → Semiring (R₂ i)] [∀ (i : ι₁), SubsemiringClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubsemiringClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃+* R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃+* RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The ring isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

@[simp]

theorem RingEquiv.restrictedProductCongr_apply_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Semiring (R₁ i)] [(i : ι₂) → Semiring (R₂ i)] [∀ (i : ι₁), SubsemiringClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubsemiringClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} {e : ι₁ ≃ ι₂} {h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂} {φ : (i : ι₁) → R₁ i ≃+* R₂ (e i)} {hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))} {x : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁} {i : ι₁} : ((restrictedProductCongr e h φ hφ) x) (e i) = (φ i) (x i)

@[simp]

theorem RingEquiv.restrictedProductCongr_symm_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Semiring (R₁ i)] [(i : ι₂) → Semiring (R₂ i)] [∀ (i : ι₁), SubsemiringClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubsemiringClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} {e : ι₁ ≃ ι₂} {h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂} {φ : (i : ι₁) → R₁ i ≃+* R₂ (e i)} {hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))} {x : RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂} : ⇑((restrictedProductCongr e h φ hφ).symm x) = fun (a : ι₁) => (φ a).symm (x (e a))

def LinearEquiv.restrictedProductCongr {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} {T : Type u_7} [Semiring T] [(i : ι₁) → AddCommMonoid (R₁ i)] [(i : ι₂) → AddCommMonoid (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} [(i : ι₁) → Module T (R₁ i)] [(i : ι₂) → Module T (R₂ i)] [∀ (i : ι₁), AddSubmonoidClass (S₁ i) (R₁ i)] [∀ (i : ι₂), AddSubmonoidClass (S₂ i) (R₂ i)] [∀ (i : ι₁), SMulMemClass (S₁ i) T (R₁ i)] [∀ (i : ι₂), SMulMemClass (S₂ i) T (R₂ i)] (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃ₗ[T] R₂ (e i)) (hφ : ∀ᶠ (i : ι₁) in 𝓕₁, Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) : RestrictedProduct (fun (i : ι₁) => R₁ i) (fun (i : ι₁) => ↑(A₁ i)) 𝓕₁ ≃ₗ[T] RestrictedProduct (fun (j : ι₂) => R₂ j) (fun (j : ι₂) => ↑(A₂ j)) 𝓕₂

The linear isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

theorem RingEquiv.restrictedProductCongr_bijOn_structureSubring {ι₁ : Type u_1} {ι₂ : Type u_2} {R₁ : ι₁ → Type u_3} {S₁ : ι₁ → Type u_4} {R₂ : ι₂ → Type u_5} {S₂ : ι₂ → Type u_6} [(i : ι₁) → SetLike (S₁ i) (R₁ i)] [(i : ι₂) → SetLike (S₂ i) (R₂ i)] {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂} [(i : ι₁) → Ring (R₁ i)] [(i : ι₂) → Ring (R₂ i)] [∀ (i : ι₁), SubringClass (S₁ i) (R₁ i)] [∀ (i : ι₂), SubringClass (S₂ i) (R₂ i)] {A₁ : (i : ι₁) → S₁ i} {A₂ : (i : ι₂) → S₂ i} (e : ι₁ ≃ ι₂) (h : 𝓕₁ = Filter.comap (⇑e) 𝓕₂) (φ : (i : ι₁) → R₁ i ≃+* R₂ (e i)) (hφ : ∀ (i : ι₁), Set.BijOn ⇑(φ i) ↑(A₁ i) ↑(A₂ (e i))) : Set.BijOn ⇑(restrictedProductCongr e h φ ⋯) ↑(RestrictedProduct.structureSubring R₁ A₁ 𝓕₁) ↑(RestrictedProduct.structureSubring R₂ A₂ 𝓕₂)

def Equiv.restrictedProductProd {ι : Type u_1} {ℱ : Filter ι} {A : ι → Type u_2} {B : ι → Type u_3} {C : (i : ι) → Set (A i)} {D : (i : ι) → Set (B i)} : RestrictedProduct (fun (i : ι) => A i × B i) (fun (i : ι) => C i ×ˢ D i) ℱ ≃ RestrictedProduct (fun (i : ι) => A i) (fun (i : ι) => C i) ℱ × RestrictedProduct (fun (i : ι) => B i) (fun (i : ι) => D i) ℱ

The bijection between a restricted product of binary products, and the binary product of the restricted products.

@[simp]

theorem Equiv.restrictedProductProd_symm_apply_coe {ι : Type u_1} {ℱ : Filter ι} {A : ι → Type u_2} {B : ι → Type u_3} {C : (i : ι) → Set (A i)} {D : (i : ι) → Set (B i)} (yz : RestrictedProduct (fun (i : ι) => A i) (fun (i : ι) => C i) ℱ × RestrictedProduct (fun (i : ι) => B i) (fun (i : ι) => D i) ℱ) (i : ι) : ↑(restrictedProductProd.symm yz) i = (yz.1 i, yz.2 i)

@[simp]

theorem Equiv.restrictedProductProd_apply {ι : Type u_1} {ℱ : Filter ι} {A : ι → Type u_2} {B : ι → Type u_3} {C : (i : ι) → Set (A i)} {D : (i : ι) → Set (B i)} (x : RestrictedProduct (fun (i : ι) => A i × B i) (fun (i : ι) => C i ×ˢ D i) ℱ) : restrictedProductProd x = (RestrictedProduct.map (fun (i : ι) (t : A i × B i) => t.1) ⋯ x, RestrictedProduct.map (fun (i : ι) (t : A i × B i) => t.2) ⋯ x)

theorem Equiv.restrictedProductProd_symm_comp_inclusion {ι : Type u_1} {A : ι → Type u_2} {B : ι → Type u_3} {C : (i : ι) → Set (A i)} {D : (i : ι) → Set (B i)} {ℱ₁ ℱ₂ : Filter ι} (hℱ : ℱ₁ ≤ ℱ₂) : ⇑restrictedProductProd.symm ∘ Prod.map (RestrictedProduct.inclusion A C hℱ) (RestrictedProduct.inclusion B D hℱ) = RestrictedProduct.inclusion (fun (i : ι) => A i × B i) (fun (i : ι) => C i ×ˢ D i) hℱ ∘ ⇑restrictedProductProd.symm

def Equiv.restrictedProductPi {ι : Type u_1} {ℱ : Filter ι} {n : Type u_2} [Fintype n] {A : n → ι → Type u_3} {C : (j : n) → (i : ι) → Set (A j i)} : RestrictedProduct (fun (i : ι) => (j : n) → A j i) (fun (i : ι) => {f : (fun (i : ι) => (j : n) → A j i) i | ∀ (j : n), f j ∈ C j i}) ℱ ≃ ((j : n) → RestrictedProduct (fun (i : ι) => A j i) (fun (i : ι) => C j i) ℱ)

The bijection between a restricted product of finite products, and a finite product of restricted products.

theorem Equiv.restrictedProductPi_symm_comp_inclusion {ι : Type u_1} {n : Type u_2} [Fintype n] {A : n → ι → Type u_3} {C : (j : n) → (i : ι) → Set (A j i)} {ℱ₁ ℱ₂ : Filter ι} (hℱ : ℱ₁ ≤ ℱ₂) : (⇑restrictedProductPi.symm ∘ Pi.map fun (i : n) => RestrictedProduct.inclusion (A i) (C i) hℱ) = RestrictedProduct.inclusion (fun (i : ι) => (j : n) → A j i) (fun (i : ι) => {f : (j : n) → A j i | ∀ (j : n), f j ∈ C j i}) hℱ ∘ ⇑restrictedProductPi.symm

def Equiv.restrictedProductMatrix {ι : Type u_4} {m : Type u_5} {n : Type u_6} [Fintype m] [Fintype n] {A : ι → Type u_7} {C : (i : ι) → Set (A i)} : RestrictedProduct (fun (i : ι) => Matrix m n (A i)) (fun (i : ι) => {f : (fun (i : ι) => Matrix m n (A i)) i | ∀ (a : m) (b : n), f a b ∈ C i}) Filter.cofinite ≃ Matrix m n (RestrictedProduct (fun (i : ι) => A i) (fun (i : ι) => C i) Filter.cofinite)

The bijection between a restricted product of m x n matrices, and m x n matrices of restricted products.

def RestrictedProduct.flatten {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {𝒢 : Filter ι₂} {f : ι → ι₂} (hf : Filter.Tendsto f ℱ 𝒢) : RestrictedProduct (fun (j : ι₂) => (i : ↑(f ⁻¹' {j})) → G ↑i) (fun (j : ι₂) => Set.univ.pi fun (i : ↑(f ⁻¹' {j})) => C ↑i) 𝒢 → RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) ℱ

The canonical map from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set.

@[simp]

theorem RestrictedProduct.flatten_apply {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {𝒢 : Filter ι₂} {f : ι → ι₂} (hf : Filter.Tendsto f ℱ 𝒢) (x : RestrictedProduct (fun (j : ι₂) => (i : ↑(f ⁻¹' {j})) → G ↑i) (fun (j : ι₂) => Set.univ.pi fun (i : ↑(f ⁻¹' {j})) => C ↑i) 𝒢) (i : ι) : (flatten C hf x) i = x (f i) ⟨i, ⋯⟩

def RestrictedProduct.flatten_equiv {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {𝒢 : Filter ι₂} {f : ι → ι₂} (hf : Filter.comap f 𝒢 = ℱ) : RestrictedProduct (fun (j : ι₂) => (i : ↑(f ⁻¹' {j})) → G ↑i) (fun (j : ι₂) => Set.univ.pi fun (i : ↑(f ⁻¹' {j})) => C ↑i) 𝒢 ≃ RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) ℱ

The canonical bijection from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set.

@[simp]

theorem RestrictedProduct.flatten_equiv_apply {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {𝒢 : Filter ι₂} {f : ι → ι₂} (hf : Filter.comap f 𝒢 = ℱ) (x : RestrictedProduct (fun (j : ι₂) => (i : ↑(f ⁻¹' {j})) → G ↑i) (fun (j : ι₂) => Set.univ.pi fun (i : ↑(f ⁻¹' {j})) => C ↑i) 𝒢) (i : ι) : ((flatten_equiv C hf) x) i = x (f i) ⟨i, ⋯⟩

@[simp]

theorem RestrictedProduct.flatten_equiv_symm_apply {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {𝒢 : Filter ι₂} {f : ι → ι₂} (hf : Filter.comap f 𝒢 = ℱ) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) ℱ) (i : ι₂) (j : ↑(f ⁻¹' {i})) : ((flatten_equiv C hf).symm x) i j = x ↑j

def RestrictedProduct.flatten_equiv' {ι : Type u_1} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {f : ι → ι₂} (hf : Filter.Tendsto f Filter.cofinite Filter.cofinite) : RestrictedProduct (fun (j : ι₂) => (i : ↑(f ⁻¹' {j})) → G ↑i) (fun (j : ι₂) => Set.univ.pi fun (i : ↑(f ⁻¹' {j})) => C ↑i) Filter.cofinite ≃ RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) Filter.cofinite

The equivalence given by flatten when both restricted products are over the cofinite filter.

@[simp]

theorem RestrictedProduct.flatten_equiv'_apply {ι : Type u_1} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {f : ι → ι₂} (hf : Filter.Tendsto f Filter.cofinite Filter.cofinite) (x : RestrictedProduct (fun (j : ι₂) => (i : ↑(f ⁻¹' {j})) → G ↑i) (fun (j : ι₂) => Set.univ.pi fun (i : ↑(f ⁻¹' {j})) => C ↑i) Filter.cofinite) (i : ι) : ((flatten_equiv' C hf) x) i = x (f i) ⟨i, ⋯⟩

@[simp]

theorem RestrictedProduct.flatten_equiv'_symm_apply {ι : Type u_1} {G : ι → Type u_2} (C : (i : ι) → Set (G i)) {ι₂ : Type u_4} {f : ι → ι₂} (hf : Filter.Tendsto f Filter.cofinite Filter.cofinite) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => C i) Filter.cofinite) (i : ι₂) (j : ↑(f ⁻¹' {i})) : ((flatten_equiv' C hf).symm x) i j = x ↑j

Principal filters

A restricted product over a principal filter is isomorphic to a product.

def RestrictedProduct.principalEquivProd {ι : Type u_1} (R : ι → Type u_2) (S : Set ι) [(i : ι) → Decidable (i ∈ S)] (A : (i : ι) → Set (R i)) : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => A i) (Filter.principal S) ≃ ((i : ↑S) → ↑(A ↑i)) × ((i : ↑Sᶜ) → R ↑i)

The canonical isomorphism between Πʳ i, [R i, A i]_[𝓟 S] and (Π i ∈ S, R i) × (Π i ∉ S, A i)

def RestrictedProduct.principalMulEquivProd {ι : Type u_1} (R : ι → Type u_2) (S : Set ι) [(i : ι) → Decidable (i ∈ S)] {T : ι → Type u_3} [(i : ι) → SetLike (T i) (R i)] {A : (i : ι) → T i} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (T i) (R i)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(A i)) (Filter.principal S) ≃* ((i : ↑S) → ↥(A ↑i)) × ((i : ↑Sᶜ) → R ↑i)

Monoid equivalence version of principalEquivProd.

def RestrictedProduct.principalAddEquivSum {ι : Type u_1} (R : ι → Type u_2) (S : Set ι) [(i : ι) → Decidable (i ∈ S)] {T : ι → Type u_3} [(i : ι) → SetLike (T i) (R i)] {A : (i : ι) → T i} [(i : ι) → AddMonoid (R i)] [∀ (i : ι), AddSubmonoidClass (T i) (R i)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(A i)) (Filter.principal S) ≃+ ((i : ↑S) → ↥(A ↑i)) × ((i : ↑Sᶜ) → R ↑i)

Additive monoid equivalence of principalEquivProd.

noncomputable def RestrictedProduct.principalLinearEquivProd {ι : Type u_4} (R : ι → Type u_5) (A : Type u_6) [CommRing A] [(i : ι) → AddCommGroup (R i)] [(i : ι) → Module A (R i)] {C : (i : ι) → Submodule A (R i)} (S : Set ι) [(i : ι) → Decidable (i ∈ S)] : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(C i)) (Filter.principal S) ≃ₗ[A] ((i : ↑S) → ↥(C ↑i)) × ((i : ↑Sᶜ) → R ↑i)

Module equivalence version of principalEquivProd.