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 j : I⦄ → i ≤ j → A j →ₐ[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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {x : (i : I) → A i} : x ∈ toSubalgebra f ↔ ∀ ⦃i j : I⦄ (h : i ≤ j), (f h) (x j) = 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 j : I⦄ → i ≤ j → A j →ₐ[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 j : I⦄ → i ≤ j → A j →ₐ[R] A i} (x : (i : I) → A i) (hx : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h) (x j) = 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i} (x : (i : I) → A i) (hx : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h) (x j) = 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 j : I⦄ → i ≤ j → A j →ₐ[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 (let_fun 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 j : I⦄ → i ≤ j → A j →ₐ[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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {i j : I} (h : i ≤ j) : (f h).comp (proj f j) = proj f 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] (φ : (i : I) → B →ₐ[R] A i) (hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h).comp (φ j) = φ 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h).comp (φ j) = φ 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h).comp (φ j) = φ 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {B : Type u_4} [Semiring B] [Algebra R B] {φ : (i : I) → B →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h).comp (φ j) = φ 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.

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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(i : J) → Semiring (B i)] [(i : J) → Algebra R (B i)] [LE J] (g : ⦃i j : J⦄ → i ≤ j → B j →ₐ[R] B i) {j' : I → J} (φ : (i : I) → B (j' i) →ₐ[R] A i) (hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), ∃ (h' : j' i ≤ j' j), (f h).comp (φ j) = (φ i).comp (g h')) : InverseLimit g →ₐ[R] InverseLimit f

If for each i : I, an element j' i : J and an algebra map B (j' 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 (j' 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(i : J) → Semiring (B i)] [(i : J) → Algebra R (B i)] [LE J] (g : ⦃i j : J⦄ → i ≤ j → B j →ₐ[R] B i) {j' : I → J} {φ : (i : I) → B (j' i) →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), ∃ (h' : j' i ≤ j' j), (f h).comp (φ j) = (φ i).comp (g h')} (x : InverseLimit g) (i : I) : ↑((lift₂' f g φ hφ) x) i = (φ i) (↑x (j' 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(i : J) → Semiring (B i)] [(i : J) → Algebra R (B i)] [LE J] (g : ⦃i j : J⦄ → i ≤ j → B j →ₐ[R] B i) {j' : I → J} {φ : (i : I) → B (j' i) →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), ∃ (h' : j' i ≤ j' j), (f h).comp (φ j) = (φ i).comp (g h')} (i : I) : (proj f i).comp (lift₂' f g φ hφ) = (φ i).comp (proj g (j' 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(i : J) → Semiring (B i)] [(i : J) → Algebra R (B i)] [LE J] (g : ⦃i j : J⦄ → i ≤ j → B j →ₐ[R] B i) {j' : I → J} {φ : (i : I) → B (j' i) →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), ∃ (h' : j' i ≤ j' j), (f h).comp (φ j) = (φ i).comp (g h')} (h : InverseLimit g →ₐ[R] InverseLimit f) (hh : ∀ (i : I), (proj f i).comp h = (φ i).comp (proj g (j' 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 j : I⦄ → i ≤ j → A j →ₐ[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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(i : J) → Semiring (B i)] [(i : J) → Algebra R (B i)] [LE J] (g : ⦃i j : J⦄ → i ≤ j → B j →ₐ[R] B i) {j' : I → J} {φ : (i : I) → B (j' i) →ₐ[R] A i} {hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), ∃ (h' : j' i ≤ j' j), (f h).comp (φ j) = (φ i).comp (g h')} {K : Type u_6} {C : K → Type u_7} [(i : K) → Semiring (C i)] [(i : K) → Algebra R (C i)] [LE K] (h : ⦃i j : K⦄ → i ≤ j → C j →ₐ[R] C i) {k' : J → K} {ψ : (i : J) → C (k' i) →ₐ[R] B i} {hψ : ∀ ⦃i j : J⦄ (h' : i ≤ j), ∃ (h'' : k' i ≤ k' j), (g h').comp (ψ j) = (ψ i).comp (h h'')} : (lift₂' f g φ hφ).comp (lift₂' g h ψ hψ) = lift₂' f h (fun (i : I) => (φ i).comp (ψ (j' 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {B : I → Type u_4} [(i : I) → Semiring (B i)] [(i : I) → Algebra R (B i)] (g : ⦃i j : I⦄ → i ≤ j → B j →ₐ[R] B i) (φ : (i : I) → B i ≃ₐ[R] A i) (hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h).comp ↑(φ j) = (↑(φ 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 j : I⦄ → i ≤ j → A j →ₐ[R] A i) {J : Type u_4} {B : J → Type u_5} [(i : J) → Semiring (B i)] [(i : J) → Algebra R (B i)] [Preorder J] (g : ⦃i j : J⦄ → i ≤ j → B j →ₐ[R] B i) (hgcomp : ∀ ⦃i j k : J⦄ (hij : i ≤ j) (hjk : j ≤ k), (g hij).comp (g hjk) = g ⋯) (e : I ≃o J) (φ : (i : I) → B (e i) ≃ₐ[R] A i) (hφ : ∀ ⦃i j : I⦄ (h : i ≤ j), (f h).comp ↑(φ j) = (↑(φ 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.