Module

ScalarExtension.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.ScalarExtension

8 declarations indexed from sourceView source ↗

Module documentation

Scalar extension of tensor equivalences with literal compatibility

The tensor universal property extends a map along an actual coefficient algebra homomorphism. The same construction on its inverse produces the extended equivalence. Both compatibility squares with a later coefficient algebra are retained. No additional algebra structure between the two coefficient rings is installed.

Imports3

Mathlib.Algebra.Algebra.Equiv
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

theorem

tensorAlgHom_tmul

L30 ↗

EtaleFundamentalGroups.tensorAlgHom_tmul

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem tensorAlgHom_tmul
    {K E B X : Type u} [CommRing K] [CommRing E] [CommRing B] [CommRing X]
    [Algebra K E] [Algebra K B] [Algebra E X]
    (f : (E ⊗[K] B) →ₐ[E] X) (e : E) (b : B) :
    f (e ⊗ₜ[K] b) = e • f ((1 : E) ⊗ₜ[K] b)

theorem

tensorMap_smul

L40 ↗

EtaleFundamentalGroups.tensorMap_smul

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem tensorMap_smul
    {K E T B : Type u} [CommRing K] [CommRing E] [CommRing T] [CommRing B]
    [Algebra K E] [Algebra K T] [Algebra K B]
    (η : E →ₐ[K] T) (e : E) (x : E ⊗[K] B) :
    Algebra.TensorProduct.map η (AlgHom.id K B) (e • x) =
      η e • Algebra.TensorProduct.map η (AlgHom.id K B) x

def

tensorScalarExtendAlgHom

L58 ↗

EtaleFundamentalGroups.tensorScalarExtendAlgHom

Documentation

Extend a tensor-algebra morphism along the specified coefficient map, using the actual tensor universal property.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
variable {K E T B D : Type u}
  [CommRing K] [CommRing E] [CommRing T] [CommRing B] [CommRing D]
  [Algebra K E] [Algebra K T] [Algebra K B] [Algebra K D]

Lean source · statement

def tensorScalarExtendAlgHom (η : E →ₐ[K] T)
    (f : (E ⊗[K] B) →ₐ[E] (E ⊗[K] D)) :
    (T ⊗[K] B) →ₐ[T] (T ⊗[K] D)

theorem

tensorScalarExtendAlgHom_tmul

L66 ↗

EtaleFundamentalGroups.tensorScalarExtendAlgHom_tmul

Documentation

The extended map has its specified value on every pure tensor.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
variable {K E T B D : Type u}
  [CommRing K] [CommRing E] [CommRing T] [CommRing B] [CommRing D]
  [Algebra K E] [Algebra K T] [Algebra K B] [Algebra K D]

Lean source · statement

theorem tensorScalarExtendAlgHom_tmul (η : E →ₐ[K] T)
    (f : (E ⊗[K] B) →ₐ[E] (E ⊗[K] D)) (t : T) (b : B) :
    tensorScalarExtendAlgHom η f (t ⊗ₜ[K] b) =
      t • Algebra.TensorProduct.map η (AlgHom.id K D) (f ((1 : E) ⊗ₜ[K] b))

theorem

tensorScalarExtendAlgHom_map

L73 ↗

EtaleFundamentalGroups.tensorScalarExtendAlgHom_map

Documentation

Extension commutes with the original coefficient inclusion on all elements.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
variable {K E T B D : Type u}
  [CommRing K] [CommRing E] [CommRing T] [CommRing B] [CommRing D]
  [Algebra K E] [Algebra K T] [Algebra K B] [Algebra K D]

Lean source · statement

theorem tensorScalarExtendAlgHom_map (η : E →ₐ[K] T)
    (f : (E ⊗[K] B) →ₐ[E] (E ⊗[K] D)) (x : E ⊗[K] B) :
    tensorScalarExtendAlgHom η f (Algebra.TensorProduct.map η (AlgHom.id K B) x) =
      Algebra.TensorProduct.map η (AlgHom.id K D) (f x)

def

tensorScalarExtendAlgEquiv

L86 ↗

EtaleFundamentalGroups.tensorScalarExtendAlgEquiv

Documentation

Extend a genuine tensor-algebra equivalence and its inverse along the specified coefficient map.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
variable {K E T B D : Type u}
  [CommRing K] [CommRing E] [CommRing T] [CommRing B] [CommRing D]
  [Algebra K E] [Algebra K T] [Algebra K B] [Algebra K D]

Lean source · statement

def tensorScalarExtendAlgEquiv (η : E →ₐ[K] T)
    (e : (E ⊗[K] B) ≃ₐ[E] (E ⊗[K] D)) :
    (T ⊗[K] B) ≃ₐ[T] (T ⊗[K] D)

theorem

tensorScalarExtendAlgHom_square

L113 ↗

EtaleFundamentalGroups.tensorScalarExtendAlgHom_square

Documentation

A literal forward compatibility square survives extension of scalars.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
variable {K E T B D : Type u}
  [CommRing K] [CommRing E] [CommRing T] [CommRing B] [CommRing D]
  [Algebra K E] [Algebra K T] [Algebra K B] [Algebra K D]

Lean source · statement

theorem tensorScalarExtendAlgHom_square
    {F : Type u} [CommRing F] [Algebra K F]
    (η : E →ₐ[K] T) (σ : T →ₐ[K] F)
    (f : (E ⊗[K] B) →ₐ[E] (E ⊗[K] D))
    (g : (F ⊗[K] B) →ₐ[F] (F ⊗[K] D))
    (h : (Algebra.TensorProduct.map (σ.comp η) (AlgHom.id K D)).comp
        (f.restrictScalars K) = (g.restrictScalars K).comp
          (Algebra.TensorProduct.map (σ.comp η) (AlgHom.id K B))) :
    (Algebra.TensorProduct.map σ (AlgHom.id K D)).comp
        ((tensorScalarExtendAlgHom η f).restrictScalars K) =
      (g.restrictScalars K).comp (Algebra.TensorProduct.map σ (AlgHom.id K B))

theorem

tensorScalarExtendAlgEquiv_squares

L145 ↗

EtaleFundamentalGroups.tensorScalarExtendAlgEquiv_squares

Documentation

Both literal squares survive extension of a genuine equivalence. The inverse is the extension of the original inverse by construction.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
variable {K E T B D : Type u}
  [CommRing K] [CommRing E] [CommRing T] [CommRing B] [CommRing D]
  [Algebra K E] [Algebra K T] [Algebra K B] [Algebra K D]

Lean source · statement

theorem tensorScalarExtendAlgEquiv_squares
    {F : Type u} [CommRing F] [Algebra K F]
    (η : E →ₐ[K] T) (σ : T →ₐ[K] F)
    (e : (E ⊗[K] B) ≃ₐ[E] (E ⊗[K] D))
    (q : (F ⊗[K] B) ≃ₐ[F] (F ⊗[K] D))
    (hf : (Algebra.TensorProduct.map (σ.comp η) (AlgHom.id K D)).comp
        (e.toAlgHom.restrictScalars K) = (q.toAlgHom.restrictScalars K).comp
          (Algebra.TensorProduct.map (σ.comp η) (AlgHom.id K B)))
    (hi : (Algebra.TensorProduct.map (σ.comp η) (AlgHom.id K B)).comp
        (e.symm.toAlgHom.restrictScalars K) = (q.symm.toAlgHom.restrictScalars K).comp
          (Algebra.TensorProduct.map (σ.comp η) (AlgHom.id K D))) :
    (Algebra.TensorProduct.map σ (AlgHom.id K D)).comp
        ((tensorScalarExtendAlgEquiv η e).toAlgHom.restrictScalars K) =
      (q.toAlgHom.restrictScalars K).comp
        (Algebra.TensorProduct.map σ (AlgHom.id K B)) ∧
    (Algebra.TensorProduct.map σ (AlgHom.id K B)).comp
        ((tensorScalarExtendAlgEquiv η e).symm.toAlgHom.restrictScalars K) =
      (q.symm.toAlgHom.restrictScalars K).comp
        (Algebra.TensorProduct.map σ (AlgHom.id K D))

Module documentation

Scalar extension of tensor equivalences with literal compatibility

Declarations