Module

FGSubalgebraTensorStage.lean

Nyll.AlgebraicCurves.Geometry.Schemes.FGSubalgebraTensorStage

9 declarations indexed from sourceView source ↗

Module documentation

Tensor products at finitely generated subalgebra stages and their directed-limit maps.

Imports4

Mathlib.RingTheory.TensorProduct.DirectLimitFG
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.Order.DirectedInverseSystem
Nyll.SchemeTheory.Descent.FGSubalgebra

Imported by3

abbrev

tensorStage

L32 ↗

AlgebraicGeometry.FGSubalgebra.tensorStage

Documentation

The tensor product with the given finitely generated subalgebra.

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

abbrev tensorStage (D : FGSubalgebra k A) : Type u

abbrev

tensorStageMap

L35 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageMap

Documentation

The transition algebra map induced by inclusion of finitely generated subalgebras.

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

abbrev tensorStageMap (D D' : FGSubalgebra k A) (h : D ≤ D') :
    tensorStage k A Γ D →ₐ[Γ] tensorStage k A Γ D'

abbrev

tensorStageToColimit

L40 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageToColimit

Documentation

The algebra map from a tensor stage to the tensor product with the ambient algebra.

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

abbrev tensorStageToColimit (D : FGSubalgebra k A) : tensorStage k A Γ D →ₐ[Γ] Γ
    ⊗[k] A

instance

tensorStage_directedSystem

L44 ↗

AlgebraicGeometry.FGSubalgebra.tensorStage_directedSystem

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · full declaration

instance tensorStage_directedSystem : DirectedSystem (tensorStage k A Γ) (fun i j h =>
    tensorStageMap k A Γ i j h) where
  map_self := fun i x => by
    induction x using TensorProduct.inductionOn with
    | tmul γ d => rw [Algebra.TensorProduct.map_tmul]; rfl
    | add x y hx hy => rw [map_add, hx, hy]
  map_map := fun i j l hij hjl x => by
    induction x using TensorProduct.inductionOn with
    | tmul γ d => rw [Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.map_tmul]; rfl
    | add x y hx hy => simp only [map_add, hx, hy]

theorem

tensorStageToColimit_comp

L55 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageToColimit_comp

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

theorem tensorStageToColimit_comp (i j : FGSubalgebra k A) (h : i ≤ j) :
    (tensorStageToColimit k A Γ j).comp (tensorStageMap k A Γ i j h) = tensorStageToColimit k A
      Γ i

theorem

tensorStageToColimit_comm

L63 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageToColimit_comm

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

theorem tensorStageToColimit_comm (D : FGSubalgebra k A) (u : ↥D.1 ⊗[k] Γ) :
    tensorStageToColimit k A Γ D (TensorProduct.comm k _ _ u) = TensorProduct.comm k _ _
      (D.1.val.toLinearMap.rTensor Γ u)

theorem

tensorStageMap_comm

L70 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageMap_comm

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · full declaration

theorem tensorStageMap_comm (D D' : FGSubalgebra k A) (h : D ≤ D') (u : ↥D.1 ⊗[k] Γ) :
    tensorStageMap k A Γ D D' h (TensorProduct.comm k _ _ u) =
      TensorProduct.comm k _ _ ((Subalgebra.inclusion (show D.1 ≤ D'.1 from
        h)).toLinearMap.rTensor Γ u) := by
  induction u using TensorProduct.inductionOn with
  | tmul d γ => rfl
  | add x y hx hy => simp only [map_add, hx, hy]

theorem

tensorStageToColimit_surj

L78 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageToColimit_surj

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

theorem tensorStageToColimit_surj (b : Γ ⊗[k] A) : ∃ (D : FGSubalgebra k A) (x : tensorStage k A
    Γ D), tensorStageToColimit k A Γ D x = b

theorem

tensorStageToColimit_zero

L84 ↗

AlgebraicGeometry.FGSubalgebra.tensorStageToColimit_zero

Source context 4 commands

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

universe u
open TensorProduct
namespace AlgebraicGeometry.FGSubalgebra
variable (k : Type u) [CommRing k] (A : Type u) [CommRing A] [Algebra k A]
  (Γ : Type u) [CommRing Γ] [Algebra k Γ]

Lean source · statement

theorem tensorStageToColimit_zero (D : FGSubalgebra k A) (x : tensorStage k A Γ D) (hx :
    tensorStageToColimit k A Γ D x = 0) :
    ∃ (D' : FGSubalgebra k A) (h : D ≤ D'), tensorStageMap k A Γ D D' h x = 0

Module documentation

Declarations