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' := ⋯ }

Instances For

source

@[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) :

(reduceModIdeal I f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)

source

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) :

transitionMap I N hmn ∘ₗ ↑R (LinearMap.reduceModIdeal (I ^ n) f) = ↑R (LinearMap.reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn

source

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) :

AdicCauchySequence I M →ₗ[R] 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' := ⋯ }

Instances For

source

@[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 : AdicCauchySequence I M) (n : ℕ) :

↑((map I f) a) n = f (↑a n)

source

@[simp]

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

map I LinearMap.id = LinearMap.id

source

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) :

map I g ∘ₗ map I f = map I (g ∘ₗ f)

source

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 : AdicCauchySequence I M) :

(map I g) ((map I f) a) = (map I (g ∘ₗ f)) a

source

@[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] :

map I 0 = 0

source

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' := ⋯ }

Instances For

source

@[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) :

↑((map I f) x) n = (LinearMap.reduceModIdeal (I ^ n) f) (↑x n)

source

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 g : AdicCompletion I M → N} (h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)) :

f = g

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

source

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 g : AdicCompletion I M →ₗ[AdicCompletion I R] T} (h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)) :

f = g

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

source

theorem AdicCompletion.map_ext'_iff {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 g : AdicCompletion I M →ₗ[AdicCompletion I R] T} :

f = g ↔ ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)

source

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 g : AdicCompletion I M →ₗ[R] N} (h : f ∘ₗ mk I M = g ∘ₗ mk I M) :

f = g

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

source

theorem AdicCompletion.map_ext''_iff {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 g : AdicCompletion I M →ₗ[R] N} :

f = g ↔ f ∘ₗ mk I M = g ∘ₗ mk I M

source

@[simp]

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

map I LinearMap.id = LinearMap.id

source

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) :

map I g ∘ₗ map I f = map I (g ∘ₗ f)

source

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) :

(map I g) ((map I f) x) = (map I (g ∘ₗ f)) x

source

@[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 : AdicCauchySequence I M) :

(map I f) ((mk I M) a) = (mk I N) ((AdicCauchySequence.map I f) a)

source

@[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] :

map I 0 = 0

source

theorem AdicCompletion.map_of {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) :

(map I f) ((of I M) x) = (of I N) (f x)

source

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) ⋯ ⋯

Instances For

source

@[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) :

(congr I f) x = (map I ↑f) x

source

@[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) :

(congr I f).symm x = (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

AdicCompletion 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.

source

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)

Instances For

source

@[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 : ℕ) :

↑((pi I M) c i) n = (LinearMap.reduceModIdeal (I ^ n) (LinearMap.proj i)) (↑c n)

source

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)

Instances For

source

@[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)) :

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

source

@[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)) :

(sum I M) ((DirectSum.of (fun (i : ι) => AdicCompletion I (M i)) j) x) = (map I (DirectSum.lof R ι M j)) x

source

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.

Instances For

source

@[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) ((sumInv I M) x) = (map I (DirectSum.component R ι M j)) x

source

@[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 : ι) :

((sumInv I M) x) j = (map I (DirectSum.component R ι M j)) x

source

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 ι] :

sumInv I M ∘ₗ sum I M = LinearMap.id

source

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 ι] :

sum I M ∘ₗ sumInv I M = LinearMap.id

source

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) ⋯ ⋯

Instances For

source

@[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)) :

(sumEquivOfFintype I M) x = (sum I M) x

source

@[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)) :

(sumEquivOfFintype I M).symm x = (sumInv I M) x

source

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.

Instances For

source

@[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)) :

(piEquivOfFintype I M) x = (pi I M) x

source

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

Instances For

source

@[simp]

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

(piEquivFin I n) x = (pi I fun (x : Fin n) => R) x

source

theorem AdicCompletion.exists_smodEq_pow_add_one_smul {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} (h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)) {y : N} {n : ℕ} (hy : y ∈ I ^ n • ⊤) :

∃ x ∈ I ^ n • ⊤, f x ≡ y [SMOD I ^ (n + 1) • ⊤]

source

theorem AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top {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} (h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)) {x : M} {y : N} {n : ℕ} (hxy : f x ≡ y [SMOD I ^ n • ⊤]) :

∃ (x' : M), x ≡ x' [SMOD I ^ n • ⊤] ∧ f x' ≡ y [SMOD I ^ (n + 1) • ⊤]

source

theorem AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq {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} (h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)) {x : M} {n : ℕ} {y : N ⧸ I ^ n • ⊤} {y' : N ⧸ I ^ (n + 1) • ⊤} (hyy' : (Submodule.factor ⋯) y' = y) (hxy : (I ^ n • ⊤).mkQ (f x) = y) :

∃ (x' : M), x ≡ x' [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f x') = y'

source

theorem AdicCompletion.map_surjective_of_mkQ_comp_surjective {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} (h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)) :

Function.Surjective ⇑(map I f)

source

theorem surjective_of_mkQ_comp_surjective {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] [IsPrecomplete I M] [IsHausdorff I N] {f : M →ₗ[R] N} (h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)) :

Function.Surjective ⇑f

source

theorem surjective_of_mk_map_comp_surjective {R : Type u_1} [CommRing R] {I : Ideal R} {S : Type u_6} [CommRing S] (f : R →+* S) [IsPrecomplete I R] [haus : IsHausdorff (Ideal.map f I) S] (h : Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map f I)).comp f)) :

Function.Surjective ⇑f

Documentation

Mathlib.RingTheory.AdicCompletion.Functoriality

Functoriality of adic completions #

Main definitions #

Main results #

Adic completion in families #