Documentation

Mathlib.RingTheory.AdicCompletion.Functoriality

Functoriality of adic completions #

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

Main definitions #

Main results #

source
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
    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
        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
            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
              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
                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

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