NYLL
Module

FaithfullyFlatModuleHomDescent.lean

Nyll.SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleHomDescent
6 declarations indexed from sourceView source ↗

Module documentation

Descent of module homomorphisms along a faithfully flat algebra

The usual Amitsur equalizer for a target module also gives the Hom-level full-faithfulness statement. An S-linear map between two extended modules comes from the base precisely when its values on the canonical generators belong to the target equalizer.

Imports2
Imported by2

Declarations

def

tensorProductDescentCompatibleLinearMaps

L34 ↗
EtaleFundamentalGroups.tensorProductDescentCompatibleLinearMaps
Documentation

The submodule of maps between extended modules whose values on the canonical generators satisfy the Amitsur equalizer relation.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w 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]
variable {N : Type w'} [AddCommGroup N] [Module R N]
Lean source · full declaration
def tensorProductDescentCompatibleLinearMaps :
    Submodule R ((S ⊗[R] M) →ₗ[S] (S ⊗[R] N)) where
  carrier := {F | ∀ m : M,
    tensorProductDescentLeft (R := R) (S := S) (M := N)
        (F (1 ⊗ₜ[R] m)) =
      tensorProductDescentRight (R := R) (S := S) (M := N)
        (F (1 ⊗ₜ[R] m))}
  zero_mem' := by simp
  add_mem' := by
    intro F G hF hG m
    simp only [LinearMap.add_apply, map_add]
    rw [hF m, hG m]
  smul_mem' := by
    intro r F hF m
    simp only [LinearMap.smul_apply, map_smul]
    rw [hF m]
def

tensorProductLinearMapToDescentCompatible

L53 ↗
EtaleFundamentalGroups.tensorProductLinearMapToDescentCompatible
Documentation

Base change sends every R-linear map to a descent-compatible map between the extended modules.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w 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]
variable {N : Type w'} [AddCommGroup N] [Module R N]
Lean source · full declaration
def tensorProductLinearMapToDescentCompatible :
    (M →ₗ[R] N) →ₗ[R]
      tensorProductDescentCompatibleLinearMaps
        (R := R) (S := S) (M := M) (N := N) where
  toFun f := ⟨f.baseChange S, by
    intro m
    simp [tensorProductDescentLeft, tensorProductDescentRight]⟩
  map_add' f g := by
    apply Subtype.ext
    exact LinearMap.baseChange_add f g
  map_smul' r f := by
    apply Subtype.ext
    exact LinearMap.baseChange_smul r f
theorem

tensorProductLinearMapToDescentCompatible_coe

L68 ↗
EtaleFundamentalGroups.tensorProductLinearMapToDescentCompatible_coe
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w 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]
variable {N : Type w'} [AddCommGroup N] [Module R N]
Lean source · statement
theorem tensorProductLinearMapToDescentCompatible_coe
    (f : M →ₗ[R] N) :
    (tensorProductLinearMapToDescentCompatible
      (R := R) (S := S) (M := M) (N := N) f :
        (S ⊗[R] M) →ₗ[S] (S ⊗[R] N)) =
      f.baseChange S
def

tensorProductLinearMapDescentEquiv

L78 ↗
EtaleFundamentalGroups.tensorProductLinearMapDescentEquiv
Documentation

Faithfully flat base change is fully faithful after equipping extended modules with their canonical Amitsur descent relation.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w 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]
variable {N : Type w'} [AddCommGroup N] [Module R N]
Lean source · statement
def tensorProductLinearMapDescentEquiv
    [Module.FaithfullyFlat R S] :
    (M →ₗ[R] N) ≃ₗ[R]
      tensorProductDescentCompatibleLinearMaps
        (R := R) (S := S) (M := M) (N := N)
theorem

tensorProductLinearMapDescentEquiv_apply

L112 ↗
EtaleFundamentalGroups.tensorProductLinearMapDescentEquiv_apply
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w 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]
variable {N : Type w'} [AddCommGroup N] [Module R N]
Lean source · statement
theorem tensorProductLinearMapDescentEquiv_apply
    [Module.FaithfullyFlat R S] (f : M →ₗ[R] N) :
    ((tensorProductLinearMapDescentEquiv
      (R := R) (S := S) (M := M) (N := N)) f :
        (S ⊗[R] M) →ₗ[S] (S ⊗[R] N)) =
      f.baseChange S
theorem

tensorProductLinearMapDescentEquiv_symm_baseChange

L121 ↗
EtaleFundamentalGroups.tensorProductLinearMapDescentEquiv_symm_baseChange
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v w 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]
variable {N : Type w'} [AddCommGroup N] [Module R N]
Lean source · statement
theorem tensorProductLinearMapDescentEquiv_symm_baseChange
    [Module.FaithfullyFlat R S]
    (F : tensorProductDescentCompatibleLinearMaps
      (R := R) (S := S) (M := M) (N := N)) :
    ((tensorProductLinearMapDescentEquiv
      (R := R) (S := S) (M := M) (N := N)).symm F).baseChange S =
      (F : (S ⊗[R] M) →ₗ[S] (S ⊗[R] N))

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