Theorems · Definition · general topology

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} →
                [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)] →
                  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] →
                    {B₁ : (i : ι₁) → S₁ i} →
                      {B₂ : (j : ι₂) → S₂ j} →
                        (f : ι₂ → ι₁) →
                          Filter.Tendsto f 𝓕₂ 𝓕₁ →
                            [inst_2 : (i : ι₁) → Ring (R₁ i)] →
                              [inst_3 : (i : ι₂) → Ring (R₂ i)] →
                                [inst_4 : ∀ (i : ι₁), SubringClass (S₁ i) (R₁ i)] →
                                  [inst_5 : ∀ (i : ι₂), SubringClass (S₂ i) (R₂ i)] →
                                    (φ : (j : ι₂) → R₁ (f j) →+* R₂ j) →
                                      (∀ᶠ (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.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

1 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

SetLikeSetLikeRingRingSubringClassSubringClass