Module

MaximalAdicCompletionMixedBilinearDescent.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionMixedBilinearDescent

8 declarations indexed from sourceView source ↗

Module documentation

Bilinear descent for mixed completion/localization data

Bilinear maps are linearized on the tensor product and then descended by the mixed Hom full-faithfulness theorem. Thus a compatible completion component and compatible principal-localization components determine a unique global bilinear map.

Imports1

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionMixedHomDescent

Imported by1

Nyll.EtaleFundamentalGroups.Purity.Local.All

abbrev

MaximalAdicCompletionMixedCompatibleBilinearMaps

L28 ↗

EtaleFundamentalGroups.MaximalAdicCompletionMixedCompatibleBilinearMaps

Documentation

Tensor-linearized mixed completion/localization data for a bilinear map.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

abbrev MaximalAdicCompletionMixedCompatibleBilinearMaps
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P]

def

bilinearMapToMaximalAdicCompletionMixedCompatible

L37 ↗

EtaleFundamentalGroups.bilinearMapToMaximalAdicCompletionMixedCompatible

Documentation

A global bilinear map gives tensor-linearized maps on the completion and on every distinguished principal localization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

def bilinearMapToMaximalAdicCompletionMixedCompatible
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P] :
    (M →ₗ[R] N →ₗ[R] P) →ₗ[R]
      MaximalAdicCompletionMixedCompatibleBilinearMaps R M N P

theorem

bilinearMapToMaximalAdicCompletionMixedCompatible_completion

L48 ↗

EtaleFundamentalGroups.bilinearMapToMaximalAdicCompletionMixedCompatible_completion

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

theorem bilinearMapToMaximalAdicCompletionMixedCompatible_completion
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P]
    (f : M →ₗ[R] N →ₗ[R] P) :
    (bilinearMapToMaximalAdicCompletionMixedCompatible R M N P f).1.1 =
      (TensorProduct.lift f).baseChange (MaximalAdicCompletionRing R)

theorem

bilinearMapToMaximalAdicCompletionMixedCompatible_localization

L59 ↗

EtaleFundamentalGroups.bilinearMapToMaximalAdicCompletionMixedCompatible_localization

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

theorem bilinearMapToMaximalAdicCompletionMixedCompatible_localization
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P]
    (f : M →ₗ[R] N →ₗ[R] P)
    (i : MaximalAdicCompletionMixedGeneratorIndex R) :
    (bilinearMapToMaximalAdicCompletionMixedCompatible R M N P f).1.2 i =
      LocalizedModule.map
        (Submonoid.powers (maximalAdicCompletionMixedGenerator R i))
        (TensorProduct.lift f)

def

maximalAdicCompletionMixedBilinearMapDescentEquiv

L74 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedBilinearMapDescentEquiv

Documentation

Mixed completion and principal-localization data are fully faithful on bilinear maps, after the canonical tensor-product linearization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

def maximalAdicCompletionMixedBilinearMapDescentEquiv
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P] :
    (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R]
      MaximalAdicCompletionMixedCompatibleBilinearMaps R M N P

theorem

maximalAdicCompletionMixedBilinearMapDescentEquiv_apply

L85 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedBilinearMapDescentEquiv_apply

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

theorem maximalAdicCompletionMixedBilinearMapDescentEquiv_apply
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P]
    (f : M →ₗ[R] N →ₗ[R] P) :
    maximalAdicCompletionMixedBilinearMapDescentEquiv R M N P f =
      bilinearMapToMaximalAdicCompletionMixedCompatible R M N P f

theorem

maximalAdicCompletionMixedBilinearMapDescentEquiv_symm_completion

L96 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedBilinearMapDescentEquiv_symm_completion

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

theorem maximalAdicCompletionMixedBilinearMapDescentEquiv_symm_completion
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P]
    (F : MaximalAdicCompletionMixedCompatibleBilinearMaps R M N P) :
    (TensorProduct.lift
        ((maximalAdicCompletionMixedBilinearMapDescentEquiv R M N P).symm F)).baseChange
          (MaximalAdicCompletionRing R) =
      F.1.1

theorem

maximalAdicCompletionMixedBilinearMapDescentEquiv_symm_localization

L118 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedBilinearMapDescentEquiv_symm_localization

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w x

Lean source · statement

theorem maximalAdicCompletionMixedBilinearMapDescentEquiv_symm_localization
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]
    (P : Type x) [AddCommGroup P] [Module R P]
    (F : MaximalAdicCompletionMixedCompatibleBilinearMaps R M N P)
    (i : MaximalAdicCompletionMixedGeneratorIndex R) :
    LocalizedModule.map
        (Submonoid.powers (maximalAdicCompletionMixedGenerator R i))
        (TensorProduct.lift
          ((maximalAdicCompletionMixedBilinearMapDescentEquiv R M N P).symm F)) =
      F.1.2 i

Module documentation

Bilinear descent for mixed completion/localization data

Declarations