NYLL
Module

MappedIdeal.lean

Nyll.EtaleFundamentalGroups.Completions.Adic.MappedIdeal
46 declarations indexed from sourceView source ↗

Module documentation

Module completion and completion at the mapped ideal

For an R-algebra S and an ideal I of R, the module completion used by AdicCompletion.ofTensorProduct is built from the quotients S / I^n S. The ring completion of S at the mapped ideal is built from the same quotients, viewed as quotients by ideals of S. This file constructs the canonical comparison directly at every finite level and passes it to the inverse limits.

Imports5
  • Mathlib.Algebra.Ring.TransferInstance
  • Mathlib.Algebra.Ring.MinimalAxioms
  • Mathlib.LinearAlgebra.FreeModule.Finite.Basic
  • Mathlib.RingTheory.AdicCompletion.AsTensorProduct
  • Mathlib.RingTheory.Ideal.Quotient.Operations
Imported by4

Declarations

theorem

pow_smul_top_eq_restrictScalars_map_pow

L35 ↗
EtaleFundamentalGroups.pow_smul_top_eq_restrictScalars_map_pow
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem pow_smul_top_eq_restrictScalars_map_pow
    (I : Ideal R) (n : ℕ) :
    (I ^ n • ⊤ : Submodule R S) =
      ((I.map (algebraMap R S)) ^ n : Ideal S).restrictScalars R
def

mappedIdealQuotientEquiv

L44 ↗
EtaleFundamentalGroups.mappedIdealQuotientEquiv
Documentation

The finite-level linear equivalence between the quotient used in the module completion and the quotient used in the mapped-ideal ring completion.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
def mappedIdealQuotientEquiv
    (I : Ideal R) (n : ℕ) :
    (S ⧸ (I ^ n • ⊤ : Submodule R S)) ≃ₗ[R]
      S ⧸ (((I.map (algebraMap R S)) ^ n : Ideal S) • ⊤ : Submodule S S)
theorem

mappedIdealQuotientEquiv_mk

L55 ↗
EtaleFundamentalGroups.mappedIdealQuotientEquiv_mk
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem mappedIdealQuotientEquiv_mk
    (I : Ideal R) (n : ℕ) (x : S) :
    mappedIdealQuotientEquiv I n
        (Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R S)) x) =
      Submodule.Quotient.mk
        (p := (((I.map (algebraMap R S)) ^ n : Ideal S) • ⊤ : Submodule S S)) x
theorem

mappedIdealQuotientEquiv_transitionMap

L63 ↗
EtaleFundamentalGroups.mappedIdealQuotientEquiv_transitionMap
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem mappedIdealQuotientEquiv_transitionMap
    (I : Ideal R) {m n : ℕ} (hmn : m ≤ n)
    (x : S ⧸ (I ^ n • ⊤ : Submodule R S)) :
    AdicCompletion.transitionMap (I.map (algebraMap R S)) S hmn
        (mappedIdealQuotientEquiv I n x) =
      mappedIdealQuotientEquiv I m
        (AdicCompletion.transitionMap I S hmn x)
theorem

mappedIdealQuotientEquiv_symm_transitionMap

L73 ↗
EtaleFundamentalGroups.mappedIdealQuotientEquiv_symm_transitionMap
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem mappedIdealQuotientEquiv_symm_transitionMap
    (I : Ideal R) {m n : ℕ} (hmn : m ≤ n)
    (x : S ⧸ (((I.map (algebraMap R S)) ^ n : Ideal S) • ⊤ : Submodule S S)) :
    AdicCompletion.transitionMap I S hmn
        ((mappedIdealQuotientEquiv I n).symm x) =
      (mappedIdealQuotientEquiv I m).symm
        (AdicCompletion.transitionMap (I.map (algebraMap R S)) S hmn x)
def

mappedIdealCompletionLinearEquiv

L87 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquiv
Documentation

The canonical R-linear equivalence from the module completion of S along I to the ring completion of S along the mapped ideal I S.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · full declaration
def mappedIdealCompletionLinearEquiv
    (I : Ideal R) :
    AdicCompletion I S ≃ₗ[R]
      AdicCompletion (I.map (algebraMap R S)) S where
  toFun x :=
    ⟨fun n => mappedIdealQuotientEquiv I n (x.val n), fun {m n} hmn => by
      rw [mappedIdealQuotientEquiv_transitionMap I hmn, x.property hmn]⟩
  invFun x :=
    ⟨fun n => (mappedIdealQuotientEquiv I n).symm (x.val n), fun {m n} hmn => by
      rw [mappedIdealQuotientEquiv_symm_transitionMap I hmn, x.property hmn]⟩
  left_inv x := by
    apply AdicCompletion.ext
    intro n
    exact (mappedIdealQuotientEquiv I n).symm_apply_apply (x.val n)
  right_inv x := by
    apply AdicCompletion.ext
    intro n
    exact (mappedIdealQuotientEquiv I n).apply_symm_apply (x.val n)
  map_add' x y := by
    apply AdicCompletion.ext
    intro n
    exact (mappedIdealQuotientEquiv I n).map_add (x.val n) (y.val n)
  map_smul' r x := by
    apply AdicCompletion.ext
    intro n
    exact (mappedIdealQuotientEquiv I n).map_smul r (x.val n)
theorem

mappedIdealCompletionLinearEquiv_apply_val

L115 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquiv_apply_val
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem mappedIdealCompletionLinearEquiv_apply_val
    (I : Ideal R) (x : AdicCompletion I S) (n : ℕ) :
    (mappedIdealCompletionLinearEquiv I x).val n =
      mappedIdealQuotientEquiv I n (x.val n)
def

completedBaseToMappedIdealCompletion

L123 ↗
EtaleFundamentalGroups.completedBaseToMappedIdealCompletion
Documentation

The canonical map from the completed base ring to the completion of S at the mapped ideal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · full declaration
def completedBaseToMappedIdealCompletion
    (I : Ideal R) :
    AdicCompletion I R →+*
      AdicCompletion (I.map (algebraMap R S)) S where
  toFun x := mappedIdealCompletionLinearEquiv I
    (AdicCompletion.map I (Algebra.linearMap R S) x)
  map_zero' := by simp
  map_add' x y := by simp
  map_one' := by
    apply AdicCompletion.ext
    intro n
    change mappedIdealQuotientEquiv I n
        ((Algebra.linearMap R S).reduceModIdeal (I ^ n)
          ((1 : AdicCompletion I R).val n)) = 1
    rw [AdicCompletion.val_one]
    change mappedIdealQuotientEquiv I n
        ((Algebra.linearMap R S).reduceModIdeal (I ^ n)
          (Submodule.Quotient.mk
            (p := (I ^ n • ⊤ : Submodule R R)) 1)) =
      Submodule.Quotient.mk
        (p := (((I.map (algebraMap R S)) ^ n : Ideal S) • ⊤ : Submodule S S)) 1
    rw [LinearMap.reduceModIdeal_apply, mappedIdealQuotientEquiv_mk]
    simp
  map_mul' x y := by
    apply AdicCompletion.ext
    intro n
    change mappedIdealQuotientEquiv I n
        ((Algebra.linearMap R S).reduceModIdeal (I ^ n) ((x * y).val n)) =
      mappedIdealQuotientEquiv I n
          ((Algebra.linearMap R S).reduceModIdeal (I ^ n) (x.val n)) *
        mappedIdealQuotientEquiv I n
          ((Algebra.linearMap R S).reduceModIdeal (I ^ n) (y.val n))
    rw [AdicCompletion.val_mul]
    induction x.val n, y.val n using Quotient.inductionOn₂' with
    | _ x y =>
      change mappedIdealQuotientEquiv I n
          ((Algebra.linearMap R S).reduceModIdeal (I ^ n)
            (Submodule.Quotient.mk
              (p := (I ^ n • ⊤ : Submodule R R)) (x * y))) =
        mappedIdealQuotientEquiv I n
            ((Algebra.linearMap R S).reduceModIdeal (I ^ n)
              (Submodule.Quotient.mk
                (p := (I ^ n • ⊤ : Submodule R R)) x)) *
          mappedIdealQuotientEquiv I n
            ((Algebra.linearMap R S).reduceModIdeal (I ^ n)
              (Submodule.Quotient.mk
                (p := (I ^ n • ⊤ : Submodule R R)) y))
      rw [LinearMap.reduceModIdeal_apply, LinearMap.reduceModIdeal_apply,
        LinearMap.reduceModIdeal_apply, mappedIdealQuotientEquiv_mk,
        mappedIdealQuotientEquiv_mk, mappedIdealQuotientEquiv_mk]
      simp
theorem

completedBaseToMappedIdealCompletion_apply_val

L176 ↗
EtaleFundamentalGroups.completedBaseToMappedIdealCompletion_apply_val
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem completedBaseToMappedIdealCompletion_apply_val
    (I : Ideal R) (x : AdicCompletion I R) (n : ℕ) :
    (completedBaseToMappedIdealCompletion (S := S) I x).val n =
      mappedIdealQuotientEquiv I n
        ((Algebra.linearMap R S).reduceModIdeal (I ^ n) (x.val n))
theorem

completedBaseToMappedIdealCompletion_algebraMap

L184 ↗
EtaleFundamentalGroups.completedBaseToMappedIdealCompletion_algebraMap
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
theorem completedBaseToMappedIdealCompletion_algebraMap
    (I : Ideal R) (r : R) :
    completedBaseToMappedIdealCompletion (S := S) I
        (algebraMap R (AdicCompletion I R) r) =
      algebraMap R (AdicCompletion (I.map (algebraMap R S)) S) r
def

mappedIdealCompletionAlgebraOverCompletedBase

L209 ↗
EtaleFundamentalGroups.mappedIdealCompletionAlgebraOverCompletedBase
Documentation

The canonical algebra structure of the mapped-ideal completion over the completed base ring.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
def mappedIdealCompletionAlgebraOverCompletedBase
    (I : Ideal R) :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S)
instance

completedBaseComparisonAlgebra

L221 ↗
EtaleFundamentalGroups.completedBaseComparisonAlgebra
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
Lean source · statement
instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S)
theorem

mappedIdealCompletionIsScalarTower

L228 ↗
EtaleFundamentalGroups.mappedIdealCompletionIsScalarTower
Documentation

The canonical completed-base algebra structure restricts to the native R-algebra structure on the mapped-ideal completion.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
Lean source · statement
theorem mappedIdealCompletionIsScalarTower
    :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S)
instance

completedBaseComparisonIsScalarTower

L236 ↗
EtaleFundamentalGroups.completedBaseComparisonIsScalarTower
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
Lean source · statement
instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S)
theorem

mappedIdealCompletionLinearEquiv_smul

L244 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquiv_smul
Documentation

The finite-level comparison intertwines the existing completed-base scalar action on the module completion with multiplication by the canonical completed-base map on the mapped-ideal completion.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem mappedIdealCompletionLinearEquiv_smul
    (r : AdicCompletion I R) (x : AdicCompletion I S) :
    mappedIdealCompletionLinearEquiv I (r • x) =
      r • mappedIdealCompletionLinearEquiv I x
def

mappedIdealCompletionLinearEquivOverCompletedBase

L273 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquivOverCompletedBase
Documentation

The canonical comparison as a linear equivalence over the completed base ring.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def mappedIdealCompletionLinearEquivOverCompletedBase
    :
    AdicCompletion I S ≃ₗ[AdicCompletion I R]
      AdicCompletion (I.map (algebraMap R S)) S
theorem

mappedIdealCompletionLinearEquiv_of

L289 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquiv_of
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem mappedIdealCompletionLinearEquiv_of
    (s : S) :
    mappedIdealCompletionLinearEquiv I (AdicCompletion.of I S s) =
      algebraMap S (AdicCompletion (I.map (algebraMap R S)) S) s
def

tensorProductToMappedIdealCompletionAlgHom

L299 ↗
EtaleFundamentalGroups.tensorProductToMappedIdealCompletionAlgHom
Documentation

The canonical algebra homomorphism from the base-changed algebra to the mapped-ideal completion.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def tensorProductToMappedIdealCompletionAlgHom
    :
    (AdicCompletion I R ⊗[R] S) →ₐ[AdicCompletion I R]
      AdicCompletion (I.map (algebraMap R S)) S
theorem

tensorProductToMappedIdealCompletionAlgHom_tmul

L309 ↗
EtaleFundamentalGroups.tensorProductToMappedIdealCompletionAlgHom_tmul
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem tensorProductToMappedIdealCompletionAlgHom_tmul
    (r : AdicCompletion I R) (s : S) :
    tensorProductToMappedIdealCompletionAlgHom I (r ⊗ₜ[R] s) =
      r • algebraMap S (AdicCompletion (I.map (algebraMap R S)) S) s
theorem

tensorProductToMappedIdealCompletionAlgHom_apply

L315 ↗
EtaleFundamentalGroups.tensorProductToMappedIdealCompletionAlgHom_apply
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section CompletedBaseComparison
variable (I : Ideal R)
local instance completedBaseComparisonAlgebra :
    Algebra (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance completedBaseComparisonIsScalarTower :
    IsScalarTower R (AdicCompletion I R)
      (AdicCompletion (I.map (algebraMap R S)) S) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem tensorProductToMappedIdealCompletionAlgHom_apply
    (z : (AdicCompletion I R ⊗[R] S)) :
    tensorProductToMappedIdealCompletionAlgHom I z =
      mappedIdealCompletionLinearEquiv I
        (AdicCompletion.ofTensorProduct I S z)
def

mappedIdealCompletionMul

L329 ↗
EtaleFundamentalGroups.mappedIdealCompletionMul
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
def mappedIdealCompletionMul
    (I : Ideal R) : Mul (AdicCompletion I S)
def

mappedIdealCompletionOne

L335 ↗
EtaleFundamentalGroups.mappedIdealCompletionOne
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
Lean source · statement
def mappedIdealCompletionOne
    (I : Ideal R) : One (AdicCompletion I S)
theorem

mappedIdealCompletionLinearEquiv_mul

L341 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquiv_mul
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionRingConstruction
Lean source · full declaration
theorem mappedIdealCompletionLinearEquiv_mul
    (I : Ideal R)
    (x y : AdicCompletion I S) :
    letI : Mul (AdicCompletion I S) := mappedIdealCompletionMul I
    mappedIdealCompletionLinearEquiv I (x * y) =
      mappedIdealCompletionLinearEquiv I x * mappedIdealCompletionLinearEquiv I y := by
  exact (mappedIdealCompletionLinearEquiv I).apply_symm_apply _
theorem

mappedIdealCompletionLinearEquiv_one

L349 ↗
EtaleFundamentalGroups.mappedIdealCompletionLinearEquiv_one
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionRingConstruction
Lean source · full declaration
theorem mappedIdealCompletionLinearEquiv_one
    (I : Ideal R) :
    letI : One (AdicCompletion I S) := mappedIdealCompletionOne I
    mappedIdealCompletionLinearEquiv I (1 : AdicCompletion I S) = 1 := by
  exact (mappedIdealCompletionLinearEquiv I).apply_symm_apply _
def

mappedIdealCompletionCommRing

L359 ↗
EtaleFundamentalGroups.mappedIdealCompletionCommRing
Documentation

The commutative-ring structure on the module completion obtained by using the canonical finite-level quotient rings. Its additive structure is the existing additive structure of the module completion.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionRingConstruction
Lean source · statement
def mappedIdealCompletionCommRing
    (I : Ideal R) : CommRing (AdicCompletion I S)
def

mappedIdealCompletionRingEquiv

L388 ↗
EtaleFundamentalGroups.mappedIdealCompletionRingEquiv
Documentation

The canonical ring equivalence from the module completion along I to the ring completion along the mapped ideal I S.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionTransportedRing
Lean source · full declaration
def mappedIdealCompletionRingEquiv
    (I : Ideal R) :
    letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
    AdicCompletion I S ≃+* AdicCompletion (I.map (algebraMap R S)) S := by
  let e : AdicCompletion I S ≃
      AdicCompletion (I.map (algebraMap R S)) S :=
    (mappedIdealCompletionLinearEquiv I).toEquiv
  letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
  exact
    { toEquiv := e
      map_add' := fun x y ↦ by
        apply AdicCompletion.ext
        intro n
        exact (mappedIdealQuotientEquiv I n).map_add (x.val n) (y.val n)
      map_mul' := mappedIdealCompletionLinearEquiv_mul I }
theorem

mappedIdealCompletionRingEquiv_apply_val

L405 ↗
EtaleFundamentalGroups.mappedIdealCompletionRingEquiv_apply_val
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionTransportedRing
Lean source · full declaration
theorem mappedIdealCompletionRingEquiv_apply_val
    (I : Ideal R) (x : AdicCompletion I S) (n : ℕ) :
    letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
    (mappedIdealCompletionRingEquiv I x).val n =
      mappedIdealQuotientEquiv I n (x.val n) := by
  rfl
def

mappedIdealCompletionAlgebra

L415 ↗
EtaleFundamentalGroups.mappedIdealCompletionAlgebra
Documentation

The R-algebra structure on the module completion obtained from the canonical comparison with the mapped-ideal ring completion.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionTransportedRing
Lean source · full declaration
def mappedIdealCompletionAlgebra
    (I : Ideal R) :
    letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
    Algebra R (AdicCompletion I S) := by
  letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
  let e : AdicCompletion I S ≃+*
      AdicCompletion (I.map (algebraMap R S)) S :=
    mappedIdealCompletionRingEquiv I
  exact (e.symm.toRingHom.comp
    (algebraMap R (AdicCompletion (I.map (algebraMap R S)) S))).toAlgebra
def

mappedIdealCompletionAlgEquiv

L428 ↗
EtaleFundamentalGroups.mappedIdealCompletionAlgEquiv
Documentation

The canonical R-algebra equivalence between the module completion along I and the ring completion along the mapped ideal I S.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionTransportedRing
Lean source · full declaration
def mappedIdealCompletionAlgEquiv
    (I : Ideal R) :
    letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
    letI : Algebra R (AdicCompletion I S) := mappedIdealCompletionAlgebra I
    AdicCompletion I S ≃ₐ[R]
      AdicCompletion (I.map (algebraMap R S)) S := by
  letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
  let e : AdicCompletion I S ≃+*
      AdicCompletion (I.map (algebraMap R S)) S :=
    mappedIdealCompletionRingEquiv I
  letI : Algebra R (AdicCompletion I S) := mappedIdealCompletionAlgebra I
  exact
    { toRingEquiv := e
      commutes' := fun r ↦ e.apply_symm_apply
        (algebraMap R (AdicCompletion (I.map (algebraMap R S)) S) r) }
theorem

mappedIdealCompletionAlgEquiv_apply_val

L445 ↗
EtaleFundamentalGroups.mappedIdealCompletionAlgEquiv_apply_val
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section MappedIdealCompletionTransportedRing
Lean source · full declaration
theorem mappedIdealCompletionAlgEquiv_apply_val
    (I : Ideal R) (x : AdicCompletion I S) (n : ℕ) :
    letI : CommRing (AdicCompletion I S) := mappedIdealCompletionCommRing I
    letI : Algebra R (AdicCompletion I S) := mappedIdealCompletionAlgebra I
    (mappedIdealCompletionAlgEquiv I x).val n =
      mappedIdealQuotientEquiv I n (x.val n) := by
  rfl
instance

tensorProductMappedIdealCompletionAlgebra

L463 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionAlgebra
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductEquivalence
universe u
variable {R₀ S₀ : Type u} [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
Lean source · statement
instance tensorProductMappedIdealCompletionAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀)
instance

tensorProductMappedIdealCompletionIsScalarTower

L468 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionIsScalarTower
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductEquivalence
universe u
variable {R₀ S₀ : Type u} [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
Lean source · statement
instance tensorProductMappedIdealCompletionIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀)
def

tensorProductMappedIdealCompletionLinearEquiv

L476 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionLinearEquiv
Documentation

For a finite algebra over a Noetherian ring, the tensor-product model of completion is canonically linearly equivalent to completion at the mapped ideal.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductEquivalence
universe u
variable {R₀ S₀ : Type u} [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def tensorProductMappedIdealCompletionLinearEquiv
    [IsNoetherianRing R₀] [Module.Finite R₀ S₀] :
    (AdicCompletion I R₀ ⊗[R₀] S₀) ≃ₗ[AdicCompletion I R₀]
      AdicCompletion (I.map (algebraMap R₀ S₀)) S₀
def

tensorProductMappedIdealCompletionAlgEquiv

L485 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionAlgEquiv
Documentation

For a finite algebra over a Noetherian ring, base change to the completed base is canonically the completion at the mapped ideal.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductEquivalence
universe u
variable {R₀ S₀ : Type u} [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def tensorProductMappedIdealCompletionAlgEquiv
    [IsNoetherianRing R₀] [Module.Finite R₀ S₀] :
    (AdicCompletion I R₀ ⊗[R₀] S₀) ≃ₐ[AdicCompletion I R₀]
      AdicCompletion (I.map (algebraMap R₀ S₀)) S₀
def

tensorProductMappedIdealCompletionRingEquiv

L504 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionRingEquiv
Documentation

The ring-equivalence form of tensorProductMappedIdealCompletionAlgEquiv.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductEquivalence
universe u
variable {R₀ S₀ : Type u} [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def tensorProductMappedIdealCompletionRingEquiv
    [IsNoetherianRing R₀] [Module.Finite R₀ S₀] :
    (AdicCompletion I R₀ ⊗[R₀] S₀) ≃+*
      AdicCompletion (I.map (algebraMap R₀ S₀)) S₀
theorem

tensorProductMappedIdealCompletionAlgEquiv_apply

L511 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionAlgEquiv_apply
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductEquivalence
universe u
variable {R₀ S₀ : Type u} [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem tensorProductMappedIdealCompletionAlgEquiv_apply
    [IsNoetherianRing R₀] [Module.Finite R₀ S₀]
    (z : AdicCompletion I R₀ ⊗[R₀] S₀) :
    tensorProductMappedIdealCompletionAlgEquiv I z =
      tensorProductToMappedIdealCompletionAlgHom I z
instance

tensorProductMappedIdealCompletionFreeAlgebra

L527 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionFreeAlgebra
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
Lean source · statement
instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀)
instance

tensorProductMappedIdealCompletionFreeIsScalarTower

L532 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionFreeIsScalarTower
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
Lean source · statement
instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀)
def

ofTensorProductEquivOfFiniteFree

L537 ↗
EtaleFundamentalGroups.ofTensorProductEquivOfFiniteFree
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def ofTensorProductEquivOfFiniteFree
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀] :
    (AdicCompletion I R₀ ⊗[R₀] S₀) ≃ₗ[AdicCompletion I R₀]
      AdicCompletion I S₀
theorem

ofTensorProductEquivOfFiniteFree_apply

L549 ↗
EtaleFundamentalGroups.ofTensorProductEquivOfFiniteFree_apply
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem ofTensorProductEquivOfFiniteFree_apply
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀]
    (z : AdicCompletion I R₀ ⊗[R₀] S₀) :
    ofTensorProductEquivOfFiniteFree I z =
      AdicCompletion.ofTensorProduct I S₀ z
theorem

ofTensorProduct_bijective_of_finite_free

L573 ↗
EtaleFundamentalGroups.ofTensorProduct_bijective_of_finite_free
Documentation

For a finite free module, the canonical tensor-to-completion map is bijective without any universe restriction on the module.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem ofTensorProduct_bijective_of_finite_free
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀] :
    Function.Bijective (AdicCompletion.ofTensorProduct I S₀)
theorem

tensorProductToMappedIdealCompletionAlgHom_bijective_of_finite_free

L587 ↗
EtaleFundamentalGroups.tensorProductToMappedIdealCompletionAlgHom_bijective_of_finite_free
Documentation

For a finite free algebra, the canonical algebra homomorphism from completed base change to mapped-ideal completion is bijective, even when the two rings live in different universes.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem tensorProductToMappedIdealCompletionAlgHom_bijective_of_finite_free
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀] :
    Function.Bijective
      (tensorProductToMappedIdealCompletionAlgHom (S := S₀) I)
def

tensorProductMappedIdealCompletionFreeAlgEquiv

L604 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionFreeAlgEquiv
Documentation

For a finite free algebra, completed base change is canonically the completion at the mapped ideal, with no equality constraint on the universes of the two rings.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def tensorProductMappedIdealCompletionFreeAlgEquiv
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀] :
    (AdicCompletion I R₀ ⊗[R₀] S₀) ≃ₐ[AdicCompletion I R₀]
      AdicCompletion (I.map (algebraMap R₀ S₀)) S₀
def

tensorProductMappedIdealCompletionFreeRingEquiv

L614 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionFreeRingEquiv
Documentation

The cross-universe ring-equivalence form of tensorProductMappedIdealCompletionFreeAlgEquiv.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
def tensorProductMappedIdealCompletionFreeRingEquiv
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀] :
    (AdicCompletion I R₀ ⊗[R₀] S₀) ≃+*
      AdicCompletion (I.map (algebraMap R₀ S₀)) S₀
theorem

tensorProductMappedIdealCompletionFreeAlgEquiv_apply

L621 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionFreeAlgEquiv_apply
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem tensorProductMappedIdealCompletionFreeAlgEquiv_apply
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀]
    (z : AdicCompletion I R₀ ⊗[R₀] S₀) :
    tensorProductMappedIdealCompletionFreeAlgEquiv I z =
      tensorProductToMappedIdealCompletionAlgHom I z
theorem

tensorProductMappedIdealCompletionFreeRingEquiv_includeRight_apply

L631 ↗
EtaleFundamentalGroups.tensorProductMappedIdealCompletionFreeRingEquiv_includeRight_apply
Documentation

On the right tensor factor, the cross-universe ring equivalence is the canonical map from the algebra to its mapped-ideal completion.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups
open TensorProduct
universe uR uS
variable {R : Type uR} [CommRing R]
variable {S : Type uS} [CommRing S] [Algebra R S]
section TensorProductFreeEquivalence
variable {R₀ : Type uR} {S₀ : Type uS}
variable [CommRing R₀] [CommRing S₀] [Algebra R₀ S₀]
variable (I : Ideal R₀)
local instance tensorProductMappedIdealCompletionFreeAlgebra :
    Algebra (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionAlgebraOverCompletedBase I
local instance tensorProductMappedIdealCompletionFreeIsScalarTower :
    IsScalarTower R₀ (AdicCompletion I R₀)
      (AdicCompletion (I.map (algebraMap R₀ S₀)) S₀) :=
  mappedIdealCompletionIsScalarTower I
Lean source · statement
theorem tensorProductMappedIdealCompletionFreeRingEquiv_includeRight_apply
    [Module.Free R₀ S₀] [Module.Finite R₀ S₀]
    (x : S₀) :
    tensorProductMappedIdealCompletionFreeRingEquiv I
        (Algebra.TensorProduct.includeRight x) =
      AdicCompletion.of (I.map (algebraMap R₀ S₀)) S₀ x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.