NYLL
Module

FaithfullyFlatModuleDatum.lean

Nyll.SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
11 declarations indexed from sourceView source ↗

Module documentation

Effective faithfully flat descent for a module datum

The invariant submodule of an arbitrary compatible tensor descent datum base-changes back to the given module. This differs from the canonical Amitsur equalizer of an already descended module. Public assumptions and conclusions are those of the pinned upstream theorem; implementation-only coaction helpers are private.

Imports5
  • Mathlib.RingTheory.Flat.Equalizer
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
  • Mathlib.RingTheory.TensorProduct.Basic
  • Mathlib.RingTheory.IsTensorProduct
  • Mathlib.Tactic.Convert
Imported by2

Declarations

def

δ

L46 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.δ
Source context 6 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
Lean source · statement
def δ : N →ₗ[A] B ⊗[A] N
def

ι

L50 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.ι
Source context 7 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
Lean source · statement
def ι : N →ₗ[A] B ⊗[A] N
def

Msub

L52 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.Msub
Source context 7 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
Lean source · statement
def Msub : Submodule A N
theorem

δ_apply

L55 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.δ_apply
Source context 8 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
omit [Module B N] [IsScalarTower A B N] in
Lean source · statement
theorem δ_apply (n : N) : δ φ n = φ (n ⊗ₜ 1)
theorem

mem_Msub

L58 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.mem_Msub
Source context 8 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
omit [Module B N] [IsScalarTower A B N] in
Lean source · statement
theorem mem_Msub {n : N} : n ∈ Msub φ ↔ φ (n ⊗ₜ 1) = 1 ⊗ₜ n
theorem

δ_smul_of_mem

L60 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.δ_smul_of_mem
Source context 7 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
Lean source · statement
theorem δ_smul_of_mem (hφ₁ : ∀ (b : B) (x : N ⊗[A] B), φ (b • x) = b • φ x)
    {m : N} (hm : m ∈ Msub φ) (b : B) : δ φ (b • m) = b ⊗ₜ m
theorem

lTensor_δ_δ

L67 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.lTensor_δ_δ
Source context 8 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
omit [Module B N] [IsScalarTower A B N] in
Lean source · statement
theorem lTensor_δ_δ
    (hcoc : (φ : N ⊗[A] B →ₗ[A] B ⊗[A] N).lTensor B ∘ₗ (TensorProduct.assoc A B N B).toLinearMap ∘ₗ
        (φ : N ⊗[A] B →ₗ[A] B ⊗[A] N).rTensor B =
      (TensorProduct.comm A N B).toLinearMap.lTensor B ∘ₗ
        (TensorProduct.assoc A B N B).toLinearMap ∘ₗ
        (φ : N ⊗[A] B →ₗ[A] B ⊗[A] N).rTensor B ∘ₗ (TensorProduct.assoc A N B B).symm.toLinearMap ∘ₗ
        (TensorProduct.comm A B B).toLinearMap.lTensor N ∘ₗ
          (TensorProduct.assoc A N B B).toLinearMap)
    (n : N) : (δ φ).lTensor B (δ φ n) = (ι A B N).lTensor B (δ φ n)
theorem

tmul_one_injective

L95 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.tmul_one_injective
Source context 7 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Defs
variable {A : Type u} [CommRing A] {B : Type v} [CommRing B] [Algebra A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
variable (A B N) in
Lean source · full declaration
theorem tmul_one_injective :
    Function.Injective (fun n : N => n ⊗ₜ[A] (1 : B)) := by
  intro m n h
  apply Algebra.TensorProduct.mk_one_injective_of_isScalarTower (R := A) (S := B) N
  simpa only [TensorProduct.mk_apply, TensorProduct.comm_tmul] using
    congrArg (TensorProduct.comm A N B) h
theorem

isBaseChange_Msub

L111 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.isBaseChange_Msub
Source context 6 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Main
variable {A : Type u} [CommRing A] (B : Type v) [CommRing B]
  [Algebra A B] [Module.FaithfullyFlat A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
Lean source · statement
theorem isBaseChange_Msub (hφ₁ : ∀ (b : B) (x : N ⊗[A] B), φ (b • x) = b • φ x)
    (hcoc : (φ : N ⊗[A] B →ₗ[A] B ⊗[A] N).lTensor B ∘ₗ (TensorProduct.assoc A B N B).toLinearMap ∘ₗ
        (φ : N ⊗[A] B →ₗ[A] B ⊗[A] N).rTensor B =
      (TensorProduct.comm A N B).toLinearMap.lTensor B ∘ₗ
        (TensorProduct.assoc A B N B).toLinearMap ∘ₗ
        (φ : N ⊗[A] B →ₗ[A] B ⊗[A] N).rTensor B ∘ₗ (TensorProduct.assoc A N B B).symm.toLinearMap ∘ₗ
        (TensorProduct.comm A B B).toLinearMap.lTensor N ∘ₗ
          (TensorProduct.assoc A N B B).toLinearMap) :
    IsBaseChange B (Msub φ).subtype
theorem

φ_tmul_of_mem

L154 ↗
SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum.Invariants.φ_tmul_of_mem
Source context 7 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
namespace Invariants
universe u v w
section Main
variable {A : Type u} [CommRing A] (B : Type v) [CommRing B]
  [Algebra A B] [Module.FaithfullyFlat A B]
  {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ : N ⊗[A] B ≃ₗ[A] B ⊗[A] N)
omit [Module.FaithfullyFlat A B] in
Lean source · statement
theorem φ_tmul_of_mem (hφ₁ : ∀ (b : B) (x : N ⊗[A] B), φ (b • x) = b • φ x)
    (hφ₂ : ∀ (b : B) (x : N ⊗[A] B),
      φ ((LinearMap.mulLeft A b).lTensor N x) = (DistribSMul.toLinearMap A N b).lTensor B (φ x))
    (b b' : B) (m : N) (hm : φ (m ⊗ₜ 1) = 1 ⊗ₜ m) :
    φ ((b • m) ⊗ₜ[A] b') = b ⊗ₜ[A] (b' • m)
theorem

isBaseChange_eqLocus_of_descentDatum

L170 ↗
Module.FaithfullyFlat.isBaseChange_eqLocus_of_descentDatum
Source context 3 commands

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

namespace SchemeTheory.RingTheory.Descent.FaithfullyFlatModuleDatum
open TensorProduct
universe u v w
Lean source · statement
theorem _root_.Module.FaithfullyFlat.isBaseChange_eqLocus_of_descentDatum
    {A : Type u} [CommRing A] (B : Type v) [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B]
    {N : Type w} [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
    (φ : TensorProduct A N B ≃ₗ[A] TensorProduct A B N)
    (hφ₁ : ∀ (b : B) (x : TensorProduct A N B), φ (b • x) = b • φ x)
    (hφ₂ : ∀ (b : B) (x : TensorProduct A N B),
      φ ((LinearMap.mulLeft A b).lTensor N x) = (DistribSMul.toLinearMap A N b).lTensor B (φ x))
    (hcocycle :
      (φ : TensorProduct A N B →ₗ[A] TensorProduct A B N).lTensor B ∘ₗ
          (TensorProduct.assoc A B N B).toLinearMap ∘ₗ
          (φ : TensorProduct A N B →ₗ[A] TensorProduct A B N).rTensor B =
        (TensorProduct.comm A N B).toLinearMap.lTensor B ∘ₗ
          (TensorProduct.assoc A B N B).toLinearMap ∘ₗ
          (φ : TensorProduct A N B →ₗ[A] TensorProduct A B N).rTensor B ∘ₗ
          (TensorProduct.assoc A N B B).symm.toLinearMap ∘ₗ
          (TensorProduct.comm A B B).toLinearMap.lTensor N ∘ₗ
          (TensorProduct.assoc A N B B).toLinearMap) :
    IsBaseChange B (LinearMap.eqLocus
        ((φ : TensorProduct A N B →ₗ[A] TensorProduct A B N) ∘ₗ (TensorProduct.mk A N B).flip 1)
        (TensorProduct.mk A B N 1)).subtype ∧
      ∀ (b b' : B) (m : N), φ (m ⊗ₜ[A] 1) = 1 ⊗ₜ[A] m →
        φ ((b • m) ⊗ₜ[A] b') = b ⊗ₜ[A] (b' • m)

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