Module

FaithfullyFlatModuleEqualizer.lean

Nyll.SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleEqualizer

18 declarations indexed from sourceView source ↗

Module documentation

The module equalizer for faithfully flat base change

This file develops the degree-zero part of faithfully flat descent for modules. The first step is the split case: if an algebra admits an algebra section, then the usual Amitsur pair remains exact after tensoring with an arbitrary module.

Imports1

Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Imported by4

def

tensorProductCounitOfSection

L34 ↗

EtaleFundamentalGroups.tensorProductCounitOfSection

Documentation

The contraction of S ⊗[R] M induced by an algebra section S →ₐ[R] R.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductCounitOfSection (g : S →ₐ[R] R) :
    S ⊗[R] M →ₗ[R] M

theorem

tensorProductCounitOfSection_tmul

L40 ↗

EtaleFundamentalGroups.tensorProductCounitOfSection_tmul

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductCounitOfSection_tmul
    (g : S →ₐ[R] R) (s : S) (m : M) :
    tensorProductCounitOfSection g (s ⊗ₜ[R] m) = g s • m

def

tensorProductFirstCounitOfSection

L47 ↗

EtaleFundamentalGroups.tensorProductFirstCounitOfSection

Documentation

Apply an algebra section to the first algebra factor of (S ⊗[R] S) ⊗[R] M.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductFirstCounitOfSection (g : S →ₐ[R] R) :
    (S ⊗[R] S) ⊗[R] M →ₗ[R] S ⊗[R] M

theorem

tensorProductFirstCounitOfSection_tmul

L53 ↗

EtaleFundamentalGroups.tensorProductFirstCounitOfSection_tmul

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductFirstCounitOfSection_tmul
    (g : S →ₐ[R] R) (s t : S) (m : M) :
    tensorProductFirstCounitOfSection g ((s ⊗ₜ[R] t) ⊗ₜ[R] m) =
      (g s • t) ⊗ₜ[R] m

theorem

tensorProduct_exact_of_section

L64 ↗

EtaleFundamentalGroups.tensorProduct_exact_of_section

Documentation

If S admits an R-algebra section, then the module-valued Amitsur pair is exact for every R-module M.

No flatness assumption on M is needed. This split calculation is the contracting-homotopy input used in faithfully flat descent.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProduct_exact_of_section (g : S →ₐ[R] R) :
    Function.Exact
      (TensorProduct.mk R S M 1)
      ((Algebra.TensorProduct.includeLeftSubRight R S).rTensor M)

def

tensorProductBaseChangeCounit

L96 ↗

EtaleFundamentalGroups.tensorProductBaseChangeCounit

Documentation

Multiplication of the two algebra factors after base change.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductBaseChangeCounit :
    S ⊗[R] (S ⊗[R] M) →ₗ[R] S ⊗[R] M

theorem

tensorProductBaseChangeCounit_tmul

L102 ↗

EtaleFundamentalGroups.tensorProductBaseChangeCounit_tmul

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductBaseChangeCounit_tmul
    (a s : S) (m : M) :
    tensorProductBaseChangeCounit (a ⊗ₜ[R] (s ⊗ₜ[R] m)) =
      (a * s) ⊗ₜ[R] m

def

tensorProductBaseChangeFirstMultiplication

L110 ↗

EtaleFundamentalGroups.tensorProductBaseChangeFirstMultiplication

Documentation

Multiply the first two algebra factors in S ⊗ ((S ⊗ S) ⊗ M), leaving the third algebra factor untouched.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductBaseChangeFirstMultiplication :
    S ⊗[R] ((S ⊗[R] S) ⊗[R] M) →ₗ[R] S ⊗[R] (S ⊗[R] M)

theorem

tensorProductBaseChangeFirstMultiplication_tmul

L118 ↗

EtaleFundamentalGroups.tensorProductBaseChangeFirstMultiplication_tmul

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductBaseChangeFirstMultiplication_tmul
    (a s t : S) (m : M) :
    tensorProductBaseChangeFirstMultiplication
        (a ⊗ₜ[R] ((s ⊗ₜ[R] t) ⊗ₜ[R] m)) =
      (a * s) ⊗ₜ[R] (t ⊗ₜ[R] m)

theorem

tensorProduct_exact_of_faithfullyFlat

L132 ↗

EtaleFundamentalGroups.tensorProduct_exact_of_faithfullyFlat

Documentation

Faithfully flat module descent in degree zero: for any faithfully flat R-algebra S and any R-module M, the canonical Amitsur pair

M → S ⊗[R] M → (S ⊗[R] S) ⊗[R] M

is exact. In particular, M is the equalizer of the two pullbacks of S ⊗[R] M to S ⊗[R] S.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProduct_exact_of_faithfullyFlat
    [Module.FaithfullyFlat R S] :
    Function.Exact
      (TensorProduct.mk R S M 1)
      ((Algebra.TensorProduct.includeLeftSubRight R S).rTensor M)

def

tensorProductDescentLeft

L175 ↗

EtaleFundamentalGroups.tensorProductDescentLeft

Documentation

Pull an extended module back along the left projection S ⇉ S ⊗[R] S.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductDescentLeft :
    S ⊗[R] M →ₗ[R] (S ⊗[R] S) ⊗[R] M

def

tensorProductDescentRight

L181 ↗

EtaleFundamentalGroups.tensorProductDescentRight

Documentation

Pull an extended module back along the right projection S ⇉ S ⊗[R] S.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductDescentRight :
    S ⊗[R] M →ₗ[R] (S ⊗[R] S) ⊗[R] M

theorem

tensorProductDescentLeft_tmul

L186 ↗

EtaleFundamentalGroups.tensorProductDescentLeft_tmul

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductDescentLeft_tmul (s : S) (m : M) :
    tensorProductDescentLeft (s ⊗ₜ[R] m) =
      (s ⊗ₜ[R] 1) ⊗ₜ[R] m

theorem

tensorProductDescentRight_tmul

L192 ↗

EtaleFundamentalGroups.tensorProductDescentRight_tmul

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductDescentRight_tmul (s : S) (m : M) :
    tensorProductDescentRight (s ⊗ₜ[R] m) =
      (1 ⊗ₜ[R] s) ⊗ₜ[R] m

def

tensorProductEqualizerMap

L199 ↗

EtaleFundamentalGroups.tensorProductEqualizerMap

Documentation

The canonical map from an R-module to the equalizer of its two pullbacks from S to S ⊗[R] S.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductEqualizerMap :
    M →ₗ[R] LinearMap.eqLocus
      (tensorProductDescentLeft (R := R) (S := S) (M := M))
      (tensorProductDescentRight (R := R) (S := S) (M := M))

theorem

tensorProductEqualizerMap_coe

L208 ↗

EtaleFundamentalGroups.tensorProductEqualizerMap_coe

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductEqualizerMap_coe (m : M) :
    (tensorProductEqualizerMap (R := R) (S := S) (M := M) m : S ⊗[R] M) =
      1 ⊗ₜ[R] m

def

tensorProductEqualizerEquiv

L216 ↗

EtaleFundamentalGroups.tensorProductEqualizerEquiv

Documentation

Faithfully flat descent identifies an R-module with the equalizer of the two canonical pullback maps from S ⊗[R] M to (S ⊗[R] S) ⊗[R] M.

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

def tensorProductEqualizerEquiv
    [Module.FaithfullyFlat R S] :
    M ≃ₗ[R] LinearMap.eqLocus
      (tensorProductDescentLeft (R := R) (S := S) (M := M))
      (tensorProductDescentRight (R := R) (S := S) (M := M))

theorem

tensorProductEqualizerEquiv_apply

L237 ↗

EtaleFundamentalGroups.tensorProductEqualizerEquiv_apply

Source context 7 commands

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

@[expose] public noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w
variable {R : Type u} [CommRing R]
variable {S : Type v} [CommRing S] [Algebra R S]
variable {M : Type w} [AddCommGroup M] [Module R M]

Lean source · statement

theorem tensorProductEqualizerEquiv_apply
    [Module.FaithfullyFlat R S] (m : M) :
    (tensorProductEqualizerEquiv (R := R) (S := S) (M := M) m : S ⊗[R] M) =
      1 ⊗ₜ[R] m

Module documentation

The module equalizer for faithfully flat base change

Declarations