Inverse limit of algebras

Let R be a commutative semiring, I be an index set with ≤ defined, A be a family of R-algebras indexed by I, f be a family of algebra homomorphisms, consisting of a map from A j to A i whenever i ≤ j (i.e. map from larger index to smaller index). One can define the inverse limit Algebra.InverseLimit with respect to these maps f.

noncomputable def Algebra.InverseLimit.toSubalgebra {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) : Subalgebra R ((i : I) → A i)

The inverse limit of algebras as a subalgebra of products of A i.

Equations

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

theorem Algebra.InverseLimit.mem_toSubalgebra {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {x : (i : I) → A i} : x ∈ toSubalgebra f ↔ ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h) (x i') = x i

@[reducible, inline]

abbrev Algebra.InverseLimit {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) : Type (max u_2 u_3)

The inverse limit of algebras as a Type.

Equations

• Algebra.InverseLimit f = ↥(Algebra.InverseLimit.toSubalgebra f)

noncomputable def Algebra.InverseLimit.mk {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] {f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i} (x : (i : I) → A i) (hx : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h) (x i') = x i) : InverseLimit f

Construct an element of the inverse limit of algebras from a compatible family of elements.

Equations

• Algebra.InverseLimit.mk x hx = ⟨x, hx⟩

@[simp]

theorem Algebra.InverseLimit.mk_coe {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] {f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i} (x : (i : I) → A i) (hx : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h) (x i') = x i) : ↑(mk x hx) = x

noncomputable def Algebra.InverseLimit.proj {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) (i : I) : InverseLimit f →ₐ[R] A i

The proj is the natural map from the inverse limit of A to A i for i : I.

Equations

• Algebra.InverseLimit.proj f i = (Pi.evalAlgHom R A i).comp (have this := (Algebra.InverseLimit.toSubalgebra f).val; this)

@[simp]

theorem Algebra.InverseLimit.proj_apply {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) (i : I) (x : InverseLimit f) : (proj f i) x = ↑x i

@[simp]

theorem Algebra.InverseLimit.algHom_comp_proj {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {i i' : I} (h : i ≤ i') : (f h).comp (proj f i') = proj f i

theorem Algebra.InverseLimit.eq_of_proj_comp_eq {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {a b : B →ₐ[R] InverseLimit f} (hab : ∀ (i : I), (proj f i).comp a = (proj f i).comp b) : a = b

noncomputable def Algebra.InverseLimit.lift {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] (φ : (i : I) → B →ₐ[R] A i) (hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp (φ i') = φ i) : B →ₐ[R] InverseLimit f

If a family of algebra maps B → A i for i : I satisfy compatibility conditions, then they lift to a map $B\to\varprojlim_i A_i$.

Equations

• Algebra.InverseLimit.lift f φ hφ = { toFun := fun (x : B) => ⟨fun (i : I) => (φ i) x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Algebra.InverseLimit.lift_apply_coe {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp (φ i') = φ i} (x : B) (i : I) : ↑((lift f φ hφ) x) i = (φ i) x

theorem Algebra.InverseLimit.proj_comp_lift {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp (φ i') = φ i} (i : I) : (proj f i).comp (lift f φ hφ) = φ i

theorem Algebra.InverseLimit.eq_lift_of_proj_comp_eq {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp (φ i') = φ i} (g : B →ₐ[R] InverseLimit f) (hg : ∀ (i : I), (proj f i).comp g = φ i) : g = lift f φ hφ

The lift map $B\to\varprojlim_i A_i$ is unique.

theorem Algebra.InverseLimit.ker_lift_eq_iInf {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp (φ i') = φ i} : RingHom.ker (lift f φ hφ) = ⨅ (i : I), RingHom.ker (φ i)

noncomputable def Algebra.InverseLimit.lift₂' {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(j : J) → Semiring (B j)] [(j : J) → Algebra R (B j)] [LE J] (g : ⦃j j' : J⦄ → j ≤ j' → B j' →ₐ[R] B j) {ij : I → J} (φ : (i : I) → B (ij i) →ₐ[R] A i) (hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), ∃ (h' : ij i ≤ ij i'), (f h).comp (φ i') = (φ i).comp (g h')) : InverseLimit g →ₐ[R] InverseLimit f

If a map ij : I → J, and for each i : I, an algebra map B (ij i) → A i is given, satisfying compatibility conditions, then they lift to a map $\varprojlim_j B_j\to\varprojlim_i A_i$.

This is the primed version since its definition involves a choice of i ↦ j' i. An unprimed version will be defined later with assumptions on index sets.

Equations

• Algebra.InverseLimit.lift₂' f g φ hφ = Algebra.InverseLimit.lift f (fun (i : I) => (φ i).comp (Algebra.InverseLimit.proj g (ij i))) ⋯

@[simp]

theorem Algebra.InverseLimit.lift₂'_apply_coe {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(j : J) → Semiring (B j)] [(j : J) → Algebra R (B j)] [LE J] (g : ⦃j j' : J⦄ → j ≤ j' → B j' →ₐ[R] B j) {ij : I → J} {φ : (i : I) → B (ij i) →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), ∃ (h' : ij i ≤ ij i'), (f h).comp (φ i') = (φ i).comp (g h')} (x : InverseLimit g) (i : I) : ↑((lift₂' f g φ hφ) x) i = (φ i) (↑x (ij i))

theorem Algebra.InverseLimit.proj_comp_lift₂' {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(j : J) → Semiring (B j)] [(j : J) → Algebra R (B j)] [LE J] (g : ⦃j j' : J⦄ → j ≤ j' → B j' →ₐ[R] B j) {ij : I → J} {φ : (i : I) → B (ij i) →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), ∃ (h' : ij i ≤ ij i'), (f h).comp (φ i') = (φ i).comp (g h')} (i : I) : (proj f i).comp (lift₂' f g φ hφ) = (φ i).comp (proj g (ij i))

theorem Algebra.InverseLimit.eq_lift₂'_of_proj_comp_eq {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(j : J) → Semiring (B j)] [(j : J) → Algebra R (B j)] [LE J] (g : ⦃j j' : J⦄ → j ≤ j' → B j' →ₐ[R] B j) {ij : I → J} {φ : (i : I) → B (ij i) →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), ∃ (h' : ij i ≤ ij i'), (f h).comp (φ i') = (φ i).comp (g h')} (h : InverseLimit g →ₐ[R] InverseLimit f) (hh : ∀ (i : I), (proj f i).comp h = (φ i).comp (proj g (ij i))) : h = lift₂' f g φ hφ

The lift map $\varprojlim_j B_j\to\varprojlim_i A_i$ is unique.

@[simp]

theorem Algebra.InverseLimit.lift₂'_id {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) : lift₂' f f (fun (i : I) => AlgHom.id R (A i)) ⋯ = AlgHom.id R (InverseLimit f)

@[simp]

theorem Algebra.InverseLimit.lift₂'_comp_lift₂' {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(j : J) → Semiring (B j)] [(j : J) → Algebra R (B j)] [LE J] (g : ⦃j j' : J⦄ → j ≤ j' → B j' →ₐ[R] B j) {ij : I → J} {φ : (i : I) → B (ij i) →ₐ[R] A i} {hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), ∃ (h' : ij i ≤ ij i'), (f h).comp (φ i') = (φ i).comp (g h')} {K : Type u_6} {C : K → Type u_7} [(k : K) → Semiring (C k)] [(k : K) → Algebra R (C k)] [LE K] (h : ⦃k k' : K⦄ → k ≤ k' → C k' →ₐ[R] C k) {jk : J → K} {ψ : (j : J) → C (jk j) →ₐ[R] B j} {hψ : ∀ ⦃j j' : J⦄ (h' : j ≤ j'), ∃ (h'' : jk j ≤ jk j'), (g h').comp (ψ j') = (ψ j).comp (h h'')} : (lift₂' f g φ hφ).comp (lift₂' g h ψ hψ) = lift₂' f h (fun (i : I) => (φ i).comp (ψ (ij i))) ⋯

noncomputable def Algebra.InverseLimit.congr {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {B : I → Type u_4} [(i : I) → Semiring (B i)] [(i : I) → Algebra R (B i)] (g : ⦃i i' : I⦄ → i ≤ i' → B i' →ₐ[R] B i) (φ : (i : I) → B i ≃ₐ[R] A i) (hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp ↑(φ i') = (↑(φ i)).comp (g h)) : InverseLimit g ≃ₐ[R] InverseLimit f

If A i and B i defined over the same index set are isomorphic, then their inverse limits are also isomorphic.

Equations

• Algebra.InverseLimit.congr f g φ hφ = AlgEquiv.ofAlgHom (Algebra.InverseLimit.lift₂' f g (fun (i : I) => ↑(φ i)) ⋯) (Algebra.InverseLimit.lift₂' g f (fun (i : I) => ↑(φ i).symm) ⋯) ⋯ ⋯

noncomputable def Algebra.InverseLimit.congr₂ {R : Type u_1} [CommSemiring R] {I : Type u_2} {A : I → Type u_3} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] [LE I] (f : ⦃i i' : I⦄ → i ≤ i' → A i' →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(j : J) → Semiring (B j)] [(j : J) → Algebra R (B j)] [Preorder J] (g : ⦃j j' : J⦄ → j ≤ j' → B j' →ₐ[R] B j) (hgcomp : ∀ ⦃j j' j'' : J⦄ (h1 : j ≤ j') (h2 : j' ≤ j''), (g h1).comp (g h2) = g ⋯) (e : I ≃o J) (φ : (i : I) → B (e i) ≃ₐ[R] A i) (hφ : ∀ ⦃i i' : I⦄ (h : i ≤ i'), (f h).comp ↑(φ i') = (↑(φ i)).comp (g ⋯)) : InverseLimit g ≃ₐ[R] InverseLimit f

If A i and B j defined over two isomorphic index sets I and J are isomorphic, such that J is a Preorder (which implies that I is also), and such that the algebra maps on B are functorial, then their inverse limits are also isomorphic.

Equations

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