Units of restricted products

This file contains results about the units of a restricted product. The restricted product Πʳ i : ι, [R i, B i]_[𝓕] of a family of types R with respect to a family of subsets B along a filter 𝓕 is defined in Mathlib.Topology.Algebra.RestrictedProduct.Basic. Here, we give conditions that characterize when an element of the restricted product is a unit, and provide an isomorphism between the units of the restricted product and the restricted product of the units.

Main definitions

• RestrictedProduct.unitsEquiv: the (monoid) isomorphism between (Πʳ i, [R i, B i]_[𝓕])ˣ and Πʳ i, [(R i)ˣ, (B i).units]_[𝓕].

Tags

restricted product, adeles, ideles

theorem RestrictedProduct.isUnit_of_eventually_isUnit {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕} (hx : ∀ (i : ι), IsUnit (x i)) (hxr : ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩) : IsUnit x

theorem RestrictedProduct.eventualy_isUnit_of_isUnit {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕} (hx : IsUnit x) : (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩

theorem RestrictedProduct.isUnit_iff {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} {x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕} : IsUnit x ↔ (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩

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

The homomorphism from the units of a restricted product to the regular product of unit.

Equations

• RestrictedProduct.coeUnits = MulEquiv.piUnits.toMonoidHom.comp (Units.map RestrictedProduct.coeMonoidHom)

def RestrictedProduct.mkUnit {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} (x : (i : ι) → (R i)ˣ) (hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units) : (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕)ˣ

Constructs a unit in a restricted product Πʳ i, [R i, B i]_[𝓕] given an element x of the usual product and the condition that x is eventually in the units of B i along 𝓕.

Equations

• RestrictedProduct.mkUnit x hx = { val := ⟨fun (i : ι) => ↑(x i), ⋯⟩, inv := ⟨fun (i : ι) => ↑(x i)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }

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

The ring isomorphism between the units of a restricted product Πʳ i, [R i, B i]_[𝓕] and the restricted product of (R i)ˣ with respect to (B i)ˣ.

Equations

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

@[simp]

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

@[simp]

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