Module

MaximalAdicCompletionMixedHomDescent.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionMixedHomDescent

12 declarations indexed from sourceView source ↗

Module documentation

Hom descent for mixed completion/localization data

The mixed module equalizer upgrades to full faithfulness on morphisms. A compatible tuple consists of a map after maximal-adic completion and one map on every distinguished principal localization. Compatibility is checked on the canonical generators, and the mixed equalizer of the target descends their images uniquely.

Imports2

Imported by2

abbrev

MaximalAdicCompletionRing

L30 ↗

EtaleFundamentalGroups.MaximalAdicCompletionRing

Documentation

The maximal-adic completion used by mixed formal gluing.

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

Lean source · statement

abbrev MaximalAdicCompletionRing
    (R : Type u) [CommRing R] [IsLocalRing R]

abbrev

MaximalAdicCompletionMixedGeneratorIndex

L35 ↗

EtaleFundamentalGroups.MaximalAdicCompletionMixedGeneratorIndex

Documentation

The canonical finite generator index for the maximal ideal.

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

Lean source · statement

abbrev MaximalAdicCompletionMixedGeneratorIndex
    (R : Type u) [CommRing R] [IsLocalRing R]

abbrev

maximalAdicCompletionMixedGenerator

L41 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedGenerator

Documentation

The maximal-ideal generator indexed by MaximalAdicCompletionMixedGeneratorIndex.

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

Lean source · statement

abbrev maximalAdicCompletionMixedGenerator
    (R : Type u) [CommRing R] [IsLocalRing R]
    (i : MaximalAdicCompletionMixedGeneratorIndex R) : R

abbrev

MaximalAdicCompletionMixedLinearMaps

L48 ↗

EtaleFundamentalGroups.MaximalAdicCompletionMixedLinearMaps

Documentation

A completion component and one localized component for every generator of the maximal ideal.

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

Lean source · statement

abbrev MaximalAdicCompletionMixedLinearMaps
    (R : Type u) [CommRing R] [IsLocalRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N]

def

maximalAdicCompletionMixedCompatibleLinearMaps

L61 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedCompatibleLinearMaps

Documentation

Mixed component maps are compatible when the images of every canonical generator form an element of the target mixed equalizer.

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

Lean source · full declaration

def maximalAdicCompletionMixedCompatibleLinearMaps
    (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] :
    Submodule R (MaximalAdicCompletionMixedLinearMaps R M N) where
  carrier := {F | ∀ m : M,
    maximalAdicCompletionMixedLeft R N
        (F.1 (1 ⊗ₜ[R] m),
          fun i ↦ F.2 i (LocalizedModule.mk m 1)) =
      maximalAdicCompletionMixedRight R N
        (F.1 (1 ⊗ₜ[R] m),
          fun i ↦ F.2 i (LocalizedModule.mk m 1))}
  zero_mem' := by
    intro m
    change maximalAdicCompletionMixedLeft R N
        (0 : MaximalAdicCompletionMixedSource R N) =
      maximalAdicCompletionMixedRight R N 0
    simp
  add_mem' := by
    intro F G hF hG m
    change maximalAdicCompletionMixedLeft R N
        ((F.1 (1 ⊗ₜ[R] m), fun i ↦ F.2 i (LocalizedModule.mk m 1)) +
          (G.1 (1 ⊗ₜ[R] m), fun i ↦ G.2 i (LocalizedModule.mk m 1))) =
      maximalAdicCompletionMixedRight R N
        ((F.1 (1 ⊗ₜ[R] m), fun i ↦ F.2 i (LocalizedModule.mk m 1)) +
          (G.1 (1 ⊗ₜ[R] m), fun i ↦ G.2 i (LocalizedModule.mk m 1)))
    rw [map_add, map_add, hF m, hG m]
  smul_mem' := by
    intro r F hF m
    change maximalAdicCompletionMixedLeft R N
        (r • (F.1 (1 ⊗ₜ[R] m),
          fun i ↦ F.2 i (LocalizedModule.mk m 1))) =
      maximalAdicCompletionMixedRight R N
        (r • (F.1 (1 ⊗ₜ[R] m),
          fun i ↦ F.2 i (LocalizedModule.mk m 1)))
    rw [map_smul, map_smul, hF m]

def

linearMapToMaximalAdicCompletionMixedCompatible

L100 ↗

EtaleFundamentalGroups.linearMapToMaximalAdicCompletionMixedCompatible

Documentation

Base change and localization of a global map give compatible mixed component maps.

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

Lean source · full declaration

def linearMapToMaximalAdicCompletionMixedCompatible
    (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] :
    (M →ₗ[R] N) →ₗ[R]
      maximalAdicCompletionMixedCompatibleLinearMaps R M N where
  toFun f := ⟨
    (f.baseChange (MaximalAdicCompletionRing R),
      fun i ↦ LocalizedModule.map
        (Submonoid.powers (maximalAdicCompletionMixedGenerator R i)) f), by
      intro m
      let y : MaximalAdicCompletionMixedSource R N :=
        (f.baseChange (MaximalAdicCompletionRing R) (1 ⊗ₜ[R] m),
          fun i ↦ LocalizedModule.map
            (Submonoid.powers (maximalAdicCompletionMixedGenerator R i)) f
              (LocalizedModule.mk m 1))
      have hy : y =
          (maximalAdicCompletionMixedEqualizerMap R N (f m)).1 := by
        apply Prod.ext
        · simp [y]
        · funext i
          simp [y]
      change maximalAdicCompletionMixedLeft R N y =
        maximalAdicCompletionMixedRight R N y
      rw [hy]
      exact (maximalAdicCompletionMixedEqualizerMap R N (f m)).2⟩
  map_add' f g := by
    apply Subtype.ext
    apply Prod.ext
    · exact LinearMap.baseChange_add f g
    · funext i
      exact (LocalizedModule.map
        (Submonoid.powers (maximalAdicCompletionMixedGenerator R i))).map_add f g
  map_smul' r f := by
    apply Subtype.ext
    apply Prod.ext
    · exact LinearMap.baseChange_smul r f
    · funext i
      exact (LocalizedModule.map
        (Submonoid.powers (maximalAdicCompletionMixedGenerator R i))).map_smul r f

theorem

linearMapToMaximalAdicCompletionMixedCompatible_completion

L142 ↗

EtaleFundamentalGroups.linearMapToMaximalAdicCompletionMixedCompatible_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

Lean source · statement

theorem linearMapToMaximalAdicCompletionMixedCompatible_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]
    (f : M →ₗ[R] N) :
    (linearMapToMaximalAdicCompletionMixedCompatible R M N f).1.1 =
      f.baseChange (MaximalAdicCompletionRing R)

theorem

linearMapToMaximalAdicCompletionMixedCompatible_localization

L152 ↗

EtaleFundamentalGroups.linearMapToMaximalAdicCompletionMixedCompatible_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

Lean source · statement

theorem linearMapToMaximalAdicCompletionMixedCompatible_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]
    (f : M →ₗ[R] N) (i : MaximalAdicCompletionMixedGeneratorIndex R) :
    (linearMapToMaximalAdicCompletionMixedCompatible R M N f).1.2 i =
      LocalizedModule.map (Submonoid.powers (maximalAdicCompletionMixedGenerator R i)) f

def

maximalAdicCompletionMixedLinearMapDescentEquiv

L163 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedLinearMapDescentEquiv

Documentation

Mixed maximal-completion and principal-localization data are fully faithful on module homomorphisms.

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

Lean source · statement

def maximalAdicCompletionMixedLinearMapDescentEquiv
    (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] :
    (M →ₗ[R] N) ≃ₗ[R]
      maximalAdicCompletionMixedCompatibleLinearMaps R M N

theorem

maximalAdicCompletionMixedLinearMapDescentEquiv_apply

L238 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedLinearMapDescentEquiv_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

Lean source · statement

theorem maximalAdicCompletionMixedLinearMapDescentEquiv_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]
    (f : M →ₗ[R] N) :
    maximalAdicCompletionMixedLinearMapDescentEquiv R M N f =
      linearMapToMaximalAdicCompletionMixedCompatible R M N f

theorem

maximalAdicCompletionMixedLinearMapDescentEquiv_symm_completion

L248 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedLinearMapDescentEquiv_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

Lean source · statement

theorem maximalAdicCompletionMixedLinearMapDescentEquiv_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]
    (F : maximalAdicCompletionMixedCompatibleLinearMaps R M N) :
    ((maximalAdicCompletionMixedLinearMapDescentEquiv R M N).symm F).baseChange
        (MaximalAdicCompletionRing R) =
      F.1.1

theorem

maximalAdicCompletionMixedLinearMapDescentEquiv_symm_localization

L264 ↗

EtaleFundamentalGroups.maximalAdicCompletionMixedLinearMapDescentEquiv_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

Lean source · statement

theorem maximalAdicCompletionMixedLinearMapDescentEquiv_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]
    (F : maximalAdicCompletionMixedCompatibleLinearMaps R M N)
    (i : MaximalAdicCompletionMixedGeneratorIndex R) :
    LocalizedModule.map (Submonoid.powers (maximalAdicCompletionMixedGenerator R i))
        ((maximalAdicCompletionMixedLinearMapDescentEquiv R M N).symm F) =
      F.1.2 i

Module documentation

Hom descent for mixed completion/localization data

Declarations