Functoriality of adic completions

In this file we establish functorial properties of the adic completion.

Main definitions

• AdicCauchySequence.map I f: the linear map on I-adic cauchy sequences induced by f
• AdicCompletion.map I f: the linear map on I-adic completions induced by f

Main results

• sumEquivOfFintype: adic completion commutes with finite sums
• piEquivOfFintype: adic completion commutes with finite products

noncomputable def LinearMap.reduceModIdeal {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : M ⧸ I • ⊤ →ₗ[R ⧸ I] N ⧸ I • ⊤

The induced linear map on the quotients mod I • ⊤.

Equations

• LinearMap.reduceModIdeal I f = { toFun := ⇑(LinearMap.reduceModIdealAux I f), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.reduceModIdeal_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (x : M) : (LinearMap.reduceModIdeal I f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)

theorem AdicCompletion.transitionMap_comp_reduceModIdeal {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) {m : ℕ} {n : ℕ} (hmn : m ≤ n) : AdicCompletion.transitionMap I N hmn ∘ₗ ↑R (LinearMap.reduceModIdeal (I ^ n) f) = ↑R (LinearMap.reduceModIdeal (I ^ m) f) ∘ₗ AdicCompletion.transitionMap I M hmn

noncomputable def AdicCompletion.AdicCauchySequence.map {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : AdicCompletion.AdicCauchySequence I M →ₗ[R] AdicCompletion.AdicCauchySequence I N

A linear map induces a linear map on adic cauchy sequences.

Equations

• AdicCompletion.AdicCauchySequence.map I f = { toFun := fun (a : AdicCompletion.AdicCauchySequence I M) => ⟨fun (n : ℕ) => f (↑a n), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AdicCompletion.AdicCauchySequence.map_apply_coe {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (a : AdicCompletion.AdicCauchySequence I M) (n : ℕ) : ↑((AdicCompletion.AdicCauchySequence.map I f) a) n = f (↑a n)

@[simp]

theorem AdicCompletion.AdicCauchySequence.map_id {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : AdicCompletion.AdicCauchySequence.map I LinearMap.id = LinearMap.id

theorem AdicCompletion.AdicCauchySequence.map_comp {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {P : Type u_4} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : AdicCompletion.AdicCauchySequence.map I g ∘ₗ AdicCompletion.AdicCauchySequence.map I f = AdicCompletion.AdicCauchySequence.map I (g ∘ₗ f)

theorem AdicCompletion.AdicCauchySequence.map_comp_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {P : Type u_4} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (a : AdicCompletion.AdicCauchySequence I M) : (AdicCompletion.AdicCauchySequence.map I g) ((AdicCompletion.AdicCauchySequence.map I f) a) = (AdicCompletion.AdicCauchySequence.map I (g ∘ₗ f)) a

@[simp]

theorem AdicCompletion.AdicCauchySequence.map_zero {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] : AdicCompletion.AdicCauchySequence.map I 0 = 0

noncomputable def AdicCompletion.map {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I N

A linear map induces a map on adic completions.

Equations

• AdicCompletion.map I f = { toFun := ⇑(AdicCompletion.adicCompletionAux I f), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AdicCompletion.map_val_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) {n : ℕ} (x : AdicCompletion I M) : ↑((AdicCompletion.map I f) x) n = (LinearMap.reduceModIdeal (I ^ n) f) (↑x n)

theorem AdicCompletion.map_ext {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Sort u_6} {f : AdicCompletion I M → N} {g : AdicCompletion I M → N} (h : ∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)) : f = g

Equality of maps out of an adic completion can be checked on Cauchy sequences.

theorem AdicCompletion.map_ext' {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {T : Type u_5} [AddCommGroup T] [Module (AdicCompletion I R) T] {f : AdicCompletion I M →ₗ[AdicCompletion I R] T} {g : AdicCompletion I M →ₗ[AdicCompletion I R] T} (h : ∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)) : f = g

Equality of linear maps out of an adic completion can be checked on Cauchy sequences.

theorem AdicCompletion.map_ext'' {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {f : AdicCompletion I M →ₗ[R] N} {g : AdicCompletion I M →ₗ[R] N} (h : f ∘ₗ AdicCompletion.mk I M = g ∘ₗ AdicCompletion.mk I M) : f = g

Equality of linear maps out of an adic completion can be checked on Cauchy sequences.

@[simp]

theorem AdicCompletion.map_id {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : AdicCompletion.map I LinearMap.id = LinearMap.id

theorem AdicCompletion.map_comp {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {P : Type u_4} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : AdicCompletion.map I g ∘ₗ AdicCompletion.map I f = AdicCompletion.map I (g ∘ₗ f)

theorem AdicCompletion.map_comp_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {P : Type u_4} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : AdicCompletion I M) : (AdicCompletion.map I g) ((AdicCompletion.map I f) x) = (AdicCompletion.map I (g ∘ₗ f)) x

@[simp]

theorem AdicCompletion.map_mk {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (a : AdicCompletion.AdicCauchySequence I M) : (AdicCompletion.map I f) ((AdicCompletion.mk I M) a) = (AdicCompletion.mk I N) ((AdicCompletion.AdicCauchySequence.map I f) a)

@[simp]

theorem AdicCompletion.map_zero {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] : AdicCompletion.map I 0 = 0

noncomputable def AdicCompletion.congr {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M ≃ₗ[R] N) : AdicCompletion I M ≃ₗ[AdicCompletion I R] AdicCompletion I N

A linear equiv induces a linear equiv on adic completions.

Equations

• AdicCompletion.congr I f = LinearEquiv.ofLinear (AdicCompletion.map I ↑f) (AdicCompletion.map I ↑f.symm) ⋯ ⋯

@[simp]

theorem AdicCompletion.congr_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M ≃ₗ[R] N) (x : AdicCompletion I M) : (AdicCompletion.congr I f) x = (AdicCompletion.map I ↑f) x

@[simp]

theorem AdicCompletion.congr_symm_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M ≃ₗ[R] N) (x : AdicCompletion I N) : (AdicCompletion.congr I f).symm x = (AdicCompletion.map I ↑f.symm) x

Adic completion in families

In this section we consider a family M : ι → Type* of R-modules. Purely from the formal properties of adic completions we obtain two canonical maps

• AdicCompleiton I (∀ j, M j) →ₗ[R] ∀ j, AdicCompletion I (M j)
• (⨁ j, (AdicCompletion I (M j))) →ₗ[R] AdicCompletion I (⨁ j, M j)

If ι is finite, both are isomorphisms and, modulo the equivalence ⨁ j, (AdicCompletion I (M j) and ∀ j, AdicCompletion I (M j), inverse to each other.

noncomputable def AdicCompletion.pi {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] : AdicCompletion I ((j : ι) → M j) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I (M j)

The canonical map from the adic completion of the product to the product of the adic completions.

Equations

• AdicCompletion.pi I M = LinearMap.pi fun (j : ι) => AdicCompletion.map I (LinearMap.proj j)

@[simp]

theorem AdicCompletion.pi_apply_coe {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (c : AdicCompletion I ((j : ι) → M j)) (i : ι) (n : ℕ) : ↑((AdicCompletion.pi I M) c i) n = (LinearMap.reduceModIdeal (I ^ n) (LinearMap.proj i)) (↑c n)

noncomputable def AdicCompletion.sum {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] : (DirectSum ι fun (j : ι) => AdicCompletion I (M j)) →ₗ[AdicCompletion I R] AdicCompletion I (DirectSum ι fun (j : ι) => M j)

The canonical map from the sum of the adic completions to the adic completion of the sum.

Equations

• AdicCompletion.sum I M = DirectSum.toModule (AdicCompletion I R) ι (AdicCompletion I (DirectSum ι fun (j : ι) => M j)) fun (j : ι) => AdicCompletion.map I (DirectSum.lof R ι M j)

@[simp]

theorem AdicCompletion.sum_lof {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (j : ι) (x : AdicCompletion I (M j)) : (AdicCompletion.sum I M) ((DirectSum.lof (AdicCompletion I R) ι (fun (i : ι) => AdicCompletion I (M i)) j) x) = (AdicCompletion.map I (DirectSum.lof R ι M j)) x

@[simp]

theorem AdicCompletion.sum_of {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (j : ι) (x : AdicCompletion I (M j)) : (AdicCompletion.sum I M) ((DirectSum.of (fun (i : ι) => AdicCompletion I (M i)) j) x) = (AdicCompletion.map I (DirectSum.lof R ι M j)) x

noncomputable def AdicCompletion.sumInv {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] : AdicCompletion I (DirectSum ι fun (j : ι) => M j) →ₗ[AdicCompletion I R] DirectSum ι fun (j : ι) => AdicCompletion I (M j)

If ι is finite, we use the equivalence of sum and product to obtain an inverse for AdicCompletion.sum from AdicCompletion.pi.

Equations

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

@[simp]

theorem AdicCompletion.component_sumInv {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (x : AdicCompletion I (DirectSum ι fun (j : ι) => M j)) (j : ι) : (DirectSum.component (AdicCompletion I R) ι (fun (i : ι) => AdicCompletion I (M i)) j) ((AdicCompletion.sumInv I M) x) = (AdicCompletion.map I (DirectSum.component R ι M j)) x

@[simp]

theorem AdicCompletion.sumInv_apply {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (x : AdicCompletion I (DirectSum ι fun (j : ι) => M j)) (j : ι) : ((AdicCompletion.sumInv I M) x) j = (AdicCompletion.map I (DirectSum.component R ι M j)) x

theorem AdicCompletion.sumInv_comp_sum {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] : AdicCompletion.sumInv I M ∘ₗ AdicCompletion.sum I M = LinearMap.id

theorem AdicCompletion.sum_comp_sumInv {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] : AdicCompletion.sum I M ∘ₗ AdicCompletion.sumInv I M = LinearMap.id

noncomputable def AdicCompletion.sumEquivOfFintype {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] : (DirectSum ι fun (j : ι) => AdicCompletion I (M j)) ≃ₗ[AdicCompletion I R] AdicCompletion I (DirectSum ι fun (j : ι) => M j)

If ι is finite, sum has sumInv as inverse.

Equations

• AdicCompletion.sumEquivOfFintype I M = LinearEquiv.ofLinear (AdicCompletion.sum I M) (AdicCompletion.sumInv I M) ⋯ ⋯

@[simp]

theorem AdicCompletion.sumEquivOfFintype_apply {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (x : DirectSum ι fun (j : ι) => AdicCompletion I (M j)) : (AdicCompletion.sumEquivOfFintype I M) x = (AdicCompletion.sum I M) x

@[simp]

theorem AdicCompletion.sumEquivOfFintype_symm_apply {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (x : AdicCompletion I (DirectSum ι fun (j : ι) => M j)) : (AdicCompletion.sumEquivOfFintype I M).symm x = (AdicCompletion.sumInv I M) x

noncomputable def AdicCompletion.piEquivOfFintype {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] [Fintype ι] : AdicCompletion I ((j : ι) → M j) ≃ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I (M j)

If ι is finite, pi is a linear equiv.

Equations

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

@[simp]

theorem AdicCompletion.piEquivOfFintype_apply {R : Type u_1} [CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] [Fintype ι] (x : AdicCompletion I ((j : ι) → M j)) : (AdicCompletion.piEquivOfFintype I M) x = (AdicCompletion.pi I M) x

noncomputable def AdicCompletion.piEquivFin {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : AdicCompletion I (Fin n → R) ≃ₗ[AdicCompletion I R] Fin n → AdicCompletion I R

Adic completion of R^n is (AdicCompletion I R)^n.

Equations

• AdicCompletion.piEquivFin I n = AdicCompletion.piEquivOfFintype I fun (x : Fin n) => R

@[simp]

theorem AdicCompletion.piEquivFin_apply {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCompletion I (Fin n → R)) : (AdicCompletion.piEquivFin I n) x = (AdicCompletion.pi I fun (x : Fin n) => R) x