NYLL
Module

GradedBaseChange.lean

Nyll.SchemeTheory.RingTheory.Descent.GradedBaseChange
14 declarations indexed from sourceView source ↗

Module documentation

Scalar extension assembled from homogeneous pieces

The inverse is defined on each homogeneous component and extended through the direct sum.

Imports3
  • Mathlib.RingTheory.GradedAlgebra.Basic
  • Mathlib.RingTheory.IsTensorProduct
  • Mathlib.RingTheory.TensorProduct.Basic
Imported by1

Declarations

abbrev

piece

L39 ↗
SchemeTheory.GradedBaseChange.piece
Source context 4 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
Lean source · statement
abbrev piece (n : ℕ) : 𝓐 n →ₗ[S] (𝓑 n).restrictScalars S
abbrev

φ

L42 ↗
SchemeTheory.GradedBaseChange.φ
Source context 4 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
Lean source · statement
abbrev φ : A ⊗[S] T →ₐ[S] B
theorem

φ_tmul

L45 ↗
SchemeTheory.GradedBaseChange.φ_tmul
Source context 4 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
Lean source · statement
theorem φ_tmul (a : A) (t : T) : φ T A B ϑ (a ⊗ₜ[S] t) = t • ϑ a
def

incl

L48 ↗
SchemeTheory.GradedBaseChange.incl
Source context 4 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
Lean source · statement
def incl (n : ℕ) : T ⊗[S] ↥(𝓐 n) →ₗ[S] A ⊗[S] T
theorem

incl_tmul

L52 ↗
SchemeTheory.GradedBaseChange.incl_tmul
Source context 5 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
omit [GradedAlgebra 𝓐] in
Lean source · statement
theorem incl_tmul (n : ℕ) (t : T) (a : 𝓐 n) :
    incl T A 𝓐 n (t ⊗ₜ[S] a) = (a : A) ⊗ₜ[S] t
theorem

φ_incl_smul

L58 ↗
SchemeTheory.GradedBaseChange.φ_incl_smul
Source context 5 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
omit [GradedAlgebra 𝓐] in
Lean source · statement
theorem φ_incl_smul (n : ℕ) (t : T) (z : T ⊗[S] ↥(𝓐 n)) :
    φ T A B ϑ (incl T A 𝓐 n (t • z)) = t • φ T A B ϑ (incl T A 𝓐 n z)
def

ψn

L67 ↗
SchemeTheory.GradedBaseChange.ψn
Source context 5 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
Lean source · statement
def ψn (n : ℕ) : ↥(𝓑 n) →ₗ[S] A ⊗[S] T
def

ψ

L72 ↗
SchemeTheory.GradedBaseChange.ψ
Source context 5 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
Lean source · statement
def ψ : B →ₗ[S] A ⊗[S] T
theorem

ψ_of_mem

L77 ↗
SchemeTheory.GradedBaseChange.ψ_of_mem
Source context 6 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
omit [GradedAlgebra 𝓐] in
Lean source · statement
theorem ψ_of_mem {b : B} {n : ℕ} (hb : b ∈ 𝓑 n) :
    ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc b = ψn T A 𝓐 B 𝓑 ϑ hϑdeg hbc n ⟨b, hb⟩
theorem

φ_ψn

L84 ↗
SchemeTheory.GradedBaseChange.φ_ψn
Source context 6 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
omit [GradedAlgebra 𝓐] [GradedAlgebra 𝓑] in
Lean source · statement
theorem φ_ψn (n : ℕ) (x : ↥((𝓑 n).restrictScalars S)) :
    φ T A B ϑ (incl T A 𝓐 n ((hbc n).equiv.symm x)) = (x : B)
theorem

φ_ψ

L98 ↗
SchemeTheory.GradedBaseChange.φ_ψ
Source context 6 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
omit [GradedAlgebra 𝓐] in
Lean source · statement
theorem φ_ψ (b : B) : φ T A B ϑ (ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc b) = b
theorem

ψ_φ_tmul_of_mem

L108 ↗
SchemeTheory.GradedBaseChange.ψ_φ_tmul_of_mem
Source context 6 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
omit [GradedAlgebra 𝓐] in
Lean source · statement
theorem ψ_φ_tmul_of_mem {a : A} {n : ℕ} (ha : a ∈ 𝓐 n) (t : T) :
    ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc (φ T A B ϑ (a ⊗ₜ[S] t)) = a ⊗ₜ[S] t
theorem

ψ_φ

L121 ↗
SchemeTheory.GradedBaseChange.ψ_φ
Source context 5 commands

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

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedBaseChange
variable {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
  (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
  (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
  (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
  (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
variable (hbc : ∀ n, IsBaseChange T (piece T A 𝓐 B 𝓑 ϑ hϑdeg n))
Lean source · statement
theorem ψ_φ (z : A ⊗[S] T) : ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc (φ T A B ϑ z) = z
theorem

bijective_tensorProduct_lift_of_forall_isBaseChange

L137 ↗
GradedAlgebra.bijective_tensorProduct_lift_of_forall_isBaseChange
Documentation

Degreewise base-change equivalences assemble to a bijective scalar-extension map on the whole graded algebra.

Source context 3 commands

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

open TensorProduct DirectSum
universe u
open SchemeTheory.GradedBaseChange in
Lean source · full declaration
theorem GradedAlgebra.bijective_tensorProduct_lift_of_forall_isBaseChange
    {S : Type u} [CommRing S] (T : Type u) [CommRing T] [Algebra S T]
    (A : Type u) [CommRing A] [Algebra S A] (𝓐 : ℕ → Submodule S A) [GradedAlgebra 𝓐]
    (B : Type u) [CommRing B] [Algebra T B] [Algebra S B] [IsScalarTower S T B]
    (𝓑 : ℕ → Submodule T B) [GradedAlgebra 𝓑]
    (ϑ : A →ₐ[S] B) (hϑdeg : ∀ n, ∀ x ∈ 𝓐 n, ϑ x ∈ 𝓑 n)
    (hbc : ∀ n, IsBaseChange T ((ϑ.toLinearMap.restrict (p := 𝓐 n)
      (q := (𝓑 n).restrictScalars S) (hϑdeg n))
      : 𝓐 n →ₗ[S] (𝓑 n).restrictScalars S)) :
    Function.Bijective
      (Algebra.TensorProduct.lift ϑ (IsScalarTower.toAlgHom S T B) (fun _ _ => Commute.all _ _) :
        A ⊗[S] T →ₐ[S] B) := by
  refine ⟨fun x y hxy => ?_, fun b => ⟨ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc b, φ_ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc b⟩⟩
  have := congrArg (ψ T A 𝓐 B 𝓑 ϑ hϑdeg hbc) hxy
  rwa [ψ_φ, ψ_φ] at this

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