Module

GenericTensorSplit.lean

Nyll.SchemeTheory.RingTheory.GenericTensorSplit

6 declarations indexed from sourceView source ↗

Module documentation

A split generic tensor in the original scalar-extension orientation

Mathlib's pushout cancellation identifies (K ⊗[R] S) ⊗[K] B with S ⊗[R] B as S-algebras, using the canonical S action on the right factor of K ⊗[R] S. A supplied splitting then gives an actual splitting into copies of S ⊗[R] K, with explicit formulas for both directions.

Imports4

Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Algebra.Pi
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.IsTensorProduct

Imported by2

def

genericTensorCancelRingEquiv

L36 ↗

SchemeTheory.genericTensorCancelRingEquiv

Documentation

Cancel the actual K-base change, preserving its literal ring maps.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v
variable (R K S B : Type u)
  [CommRing R] [CommRing K] [CommRing S] [CommRing B]
  [Algebra R K] [Algebra R S] [Algebra R B] [Algebra K B]
  [IsScalarTower R K B]

Lean source · statement

def genericTensorCancelRingEquiv :
    ((K ⊗[R] S) ⊗[K] B) ≃+* (S ⊗[R] B)

theorem

genericTensorCancelRingEquiv_tmul

L42 ↗

SchemeTheory.genericTensorCancelRingEquiv_tmul

Documentation

The cancellation comparison on a double pure tensor.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v
variable (R K S B : Type u)
  [CommRing R] [CommRing K] [CommRing S] [CommRing B]
  [Algebra R K] [Algebra R S] [Algebra R B] [Algebra K B]
  [IsScalarTower R K B]

Lean source · statement

theorem genericTensorCancelRingEquiv_tmul (k : K) (s : S) (b : B) :
    genericTensorCancelRingEquiv R K S B ((k ⊗ₜ[R] s) ⊗ₜ[K] b) =
      s ⊗ₜ[R] (k • b)

theorem

genericTensorCancelRingEquiv_symm_tmul

L54 ↗

SchemeTheory.genericTensorCancelRingEquiv_symm_tmul

Documentation

The inverse comparison retains both original factors.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v
variable (R K S B : Type u)
  [CommRing R] [CommRing K] [CommRing S] [CommRing B]
  [Algebra R K] [Algebra R S] [Algebra R B] [Algebra K B]
  [IsScalarTower R K B]

Lean source · statement

theorem genericTensorCancelRingEquiv_symm_tmul (s : S) (b : B) :
    (genericTensorCancelRingEquiv R K S B).symm (s ⊗ₜ[R] b) =
      ((1 : K) ⊗ₜ[R] s) ⊗ₜ[K] b

def

genericTensorSplitEquiv

L62 ↗

SchemeTheory.genericTensorSplitEquiv

Documentation

Transport an actual splitting over the left generic fiber into the original scalar-extension orientation used by integral-closure descent.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v
variable (R K S B : Type u)
  [CommRing R] [CommRing K] [CommRing S] [CommRing B]
  [Algebra R K] [Algebra R S] [Algebra R B] [Algebra K B]
  [IsScalarTower R K B]

Lean source · statement

def genericTensorSplitEquiv (ι : Type v)
    (e : ((K ⊗[R] S) ⊗[K] B) ≃ₐ[K ⊗[R] S] (ι → K ⊗[R] S)) :
    (S ⊗[R] B) ≃ₐ[S] (ι → S ⊗[R] K)

theorem

genericTensorSplitEquiv_tmul

L73 ↗

SchemeTheory.genericTensorSplitEquiv_tmul

Documentation

The transported forward map is the supplied splitting, followed by the literal commutation of each generic-fiber factor.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v
variable (R K S B : Type u)
  [CommRing R] [CommRing K] [CommRing S] [CommRing B]
  [Algebra R K] [Algebra R S] [Algebra R B] [Algebra K B]
  [IsScalarTower R K B]

Lean source · statement

theorem genericTensorSplitEquiv_tmul (ι : Type v)
    (e : ((K ⊗[R] S) ⊗[K] B) ≃ₐ[K ⊗[R] S] (ι → K ⊗[R] S))
    (s : S) (b : B) (i : ι) :
    genericTensorSplitEquiv R K S B ι e (s ⊗ₜ[R] b) i =
      Algebra.TensorProduct.comm R K S (e (((1 : K) ⊗ₜ[R] s) ⊗ₜ[K] b) i)

theorem

genericTensorSplitEquiv_symm_apply

L84 ↗

SchemeTheory.genericTensorSplitEquiv_symm_apply

Documentation

The transported inverse applies the supplied inverse to the literal commuted coordinates, then applies the constructed cancellation map.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u v
variable (R K S B : Type u)
  [CommRing R] [CommRing K] [CommRing S] [CommRing B]
  [Algebra R K] [Algebra R S] [Algebra R B] [Algebra K B]
  [IsScalarTower R K B]

Lean source · full declaration

theorem genericTensorSplitEquiv_symm_apply (ι : Type v)
    (e : ((K ⊗[R] S) ⊗[K] B) ≃ₐ[K ⊗[R] S] (ι → K ⊗[R] S))
    (y : ι → S ⊗[R] K) :
    (genericTensorSplitEquiv R K S B ι e).symm y =
      genericTensorCancelRingEquiv R K S B
        (e.symm (fun i => Algebra.TensorProduct.comm R S K (y i))) := by
  rfl

Module documentation

A split generic tensor in the original scalar-extension orientation

Declarations

genericTensorCancelRingEquiv

genericTensorCancelRingEquiv_tmul

genericTensorCancelRingEquiv_symm_tmul

genericTensorSplitEquiv

genericTensorSplitEquiv_tmul

genericTensorSplitEquiv_symm_apply