Module

Basic.lean

Nyll.SchemeTheory.Affine.WeilRestriction.Basic

33 declarations indexed from sourceView source ↗

Module documentation

Affine Weil restriction along a finite free algebra

For a finite free commutative R-algebra A and a finitely presented commutative R-algebra B, this file constructs explicitly an R-algebra representing C ↦ Hom_R(B, C ⊗[R] A).

This is the affine algebra input for the finite étale relative internal Hom of Stacks Project, Tag 0BL7. The presentation-dependent construction is kept private; the public theorem is independent of all choices.

Imports4

Mathlib.RingTheory.Extension.Presentation.Basic
Mathlib.RingTheory.TensorProduct.Free
Mathlib.Algebra.Category.CommAlgCat.Monoidal
Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Imported by2

abbrev

BasisIndex

L47 ↗

CommAlgCat.BasisIndex

Source context 10 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

abbrev BasisIndex (R A : Type u) [CommRing R] [CommRing A] [Algebra R A]
    [Module.Free R A]

abbrev

chosenBasis

L50 ↗

CommAlgCat.chosenBasis

Source context 10 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]

Lean source · statement

abbrev chosenBasis (R A : Type u) [CommRing R] [CommRing A] [Algebra R A]
    [Module.Free R A] : Module.Basis (BasisIndex R A) R A

def

genericImage

L57 ↗

CommAlgCat.genericImage

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def genericImage (i : ι) :
    MvPolynomial (ι × BasisIndex R A) R ⊗[R] A

lemma

genericImage_coeff

L61 ↗

CommAlgCat.genericImage_coeff

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

lemma genericImage_coeff (i : ι) (j : BasisIndex R A) :
    (Algebra.TensorProduct.basis (MvPolynomial (ι × BasisIndex R A) R)
      (chosenBasis R A)).repr (genericImage (R := R) (A := A) i) j =
      MvPolynomial.X (i, j)

def

relationCoeff

L74 ↗

CommAlgCat.relationCoeff

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def relationCoeff (s : σ) (j : BasisIndex R A) :
    MvPolynomial (ι × BasisIndex R A) R

def

relationsIdeal

L80 ↗

CommAlgCat.relationsIdeal

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def relationsIdeal : Ideal (MvPolynomial (ι × BasisIndex R A) R)

abbrev

HomRing

L84 ↗

CommAlgCat.HomRing

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

abbrev HomRing

lemma

basis_repr_map

L88 ↗

CommAlgCat.basis_repr_map

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
omit [Module.Finite R A] in

Lean source · statement

lemma basis_repr_map
    {C D : Type u} [CommRing C] [CommRing D] [Algebra R C] [Algebra R D]
    (f : C →ₐ[R] D) (x : C ⊗[R] A) (j : BasisIndex R A) :
    (Algebra.TensorProduct.basis D (chosenBasis R A)).repr
        (Algebra.TensorProduct.map f (AlgHom.id R A) x) j =
      f ((Algebra.TensorProduct.basis C (chosenBasis R A)).repr x j)

lemma

basis_repr_aeval_map

L102 ↗

CommAlgCat.basis_repr_aeval_map

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
omit [Module.Finite R A] in

Lean source · full declaration

lemma basis_repr_aeval_map
    {C D : Type u} [CommRing C] [CommRing D] [Algebra R C] [Algebra R D]
    {κ : Type u} (f : C →ₐ[R] D) (x : κ → C ⊗[R] A)
    (p : MvPolynomial κ R) (j : BasisIndex R A) :
    (Algebra.TensorProduct.basis D (chosenBasis R A)).repr
        (MvPolynomial.aeval
          (fun i => Algebra.TensorProduct.map f (AlgHom.id R A) (x i)) p) j =
      f ((Algebra.TensorProduct.basis C (chosenBasis R A)).repr
        (MvPolynomial.aeval x p) j) := by
  let tf := Algebra.TensorProduct.map f (AlgHom.id R A)
  calc
    (Algebra.TensorProduct.basis D (chosenBasis R A)).repr
        (MvPolynomial.aeval (fun i => tf (x i)) p) j =
      (Algebra.TensorProduct.basis D (chosenBasis R A)).repr
        (tf (MvPolynomial.aeval x p)) j :=
      congrArg (fun z =>
        (Algebra.TensorProduct.basis D (chosenBasis R A)).repr z j)
        (MvPolynomial.comp_aeval_apply x tf p).symm
    _ = f ((Algebra.TensorProduct.basis C (chosenBasis R A)).repr
        (MvPolynomial.aeval x p) j) := basis_repr_map f _ j

def

quotientImage

L123 ↗

CommAlgCat.quotientImage

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def quotientImage (i : ι) : HomRing (R := R) (A := A) (B := B) P ⊗[R] A

lemma

aeval_relation_quotientImage

L129 ↗

CommAlgCat.aeval_relation_quotientImage

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

lemma aeval_relation_quotientImage (s : σ) :
    MvPolynomial.aeval (quotientImage (R := R) (A := A) (B := B) P)
      (P.relation s) = 0

def

presentationMap

L157 ↗

CommAlgCat.presentationMap

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def presentationMap : P.Ring →ₐ[R] HomRing (R := R) (A := A) (B := B) P ⊗[R] A

lemma

presentationMap_relation

L160 ↗

CommAlgCat.presentationMap_relation

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

lemma presentationMap_relation (s : σ) :
    presentationMap (R := R) (A := A) (B := B) P (P.relation s) = 0

lemma

presentation_ker_le

L164 ↗

CommAlgCat.presentation_ker_le

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

lemma presentation_ker_le :
    P.ker ≤ RingHom.ker (presentationMap (R := R) (A := A) (B := B) P).toRingHom

def

presentationLift

L171 ↗

CommAlgCat.presentationLift

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def presentationLift : P.Quotient →ₐ[R]
    HomRing (R := R) (A := A) (B := B) P ⊗[R] A

def

universal

L177 ↗

CommAlgCat.universal

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

def universal : B →ₐ[R] HomRing (R := R) (A := A) (B := B) P ⊗[R] A

lemma

universal_val

L181 ↗

CommAlgCat.universal_val

Source context 11 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)

Lean source · statement

lemma universal_val (i : ι) :
    universal (R := R) (A := A) (B := B) P (P.val i) =
      quotientImage (R := R) (A := A) (B := B) P i

def

coeffAssignment

L200 ↗

CommAlgCat.coeffAssignment

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

def coeffAssignment (g : B →ₐ[R] C ⊗[R] A) (x : ι × BasisIndex R A) : C

lemma

map_genericImage_coeffAssignment

L203 ↗

CommAlgCat.map_genericImage_coeffAssignment

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma map_genericImage_coeffAssignment (g : B →ₐ[R] C ⊗[R] A) (i : ι) :
    Algebra.TensorProduct.map (MvPolynomial.aeval (coeffAssignment (P := P) g)) (AlgHom.id R A)
        (genericImage (R := R) (A := A) i) =
      g (P.val i)

lemma

aeval_relationCoeff_coeffAssignment

L222 ↗

CommAlgCat.aeval_relationCoeff_coeffAssignment

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma aeval_relationCoeff_coeffAssignment (g : B →ₐ[R] C ⊗[R] A)
    (s : σ) (j : BasisIndex R A) :
    MvPolynomial.aeval (coeffAssignment (P := P) g)
      (relationCoeff (P := P) s j) = 0

lemma

relationsIdeal_le_ker_coeffAssignment

L233 ↗

CommAlgCat.relationsIdeal_le_ker_coeffAssignment

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma relationsIdeal_le_ker_coeffAssignment (g : B →ₐ[R] C ⊗[R] A) :
    relationsIdeal (P := P) ≤
      RingHom.ker (MvPolynomial.aeval (coeffAssignment (P := P) g)).toRingHom

def

liftCoefficients

L242 ↗

CommAlgCat.liftCoefficients

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

def liftCoefficients (g : B →ₐ[R] C ⊗[R] A) :
    HomRing (R := R) (A := A) (B := B) P →ₐ[R] C

def

homForward

L249 ↗

CommAlgCat.homForward

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

def homForward (h : HomRing (R := R) (A := A) (B := B) P →ₐ[R] C) :
    B →ₐ[R] C ⊗[R] A

lemma

homForward_liftCoefficients

L254 ↗

CommAlgCat.homForward_liftCoefficients

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma homForward_liftCoefficients (g : B →ₐ[R] C ⊗[R] A) :
    homForward (P := P) (liftCoefficients (P := P) g) = g

lemma

coeffAssignment_homForward

L282 ↗

CommAlgCat.coeffAssignment_homForward

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma coeffAssignment_homForward
    (h : HomRing (R := R) (A := A) (B := B) P →ₐ[R] C)
    (i : ι) (j : BasisIndex R A) :
    coeffAssignment (P := P) (homForward (P := P) h) (i, j) =
      h (Ideal.Quotient.mkₐ R (relationsIdeal (R := R) (A := A) (B := B) P)
        (MvPolynomial.X (i, j)))

lemma

liftCoefficients_homForward

L293 ↗

CommAlgCat.liftCoefficients_homForward

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma liftCoefficients_homForward
    (h : HomRing (R := R) (A := A) (B := B) P →ₐ[R] C) :
    liftCoefficients (P := P) (homForward (P := P) h) = h

def

weilHomEquiv

L304 ↗

CommAlgCat.weilHomEquiv

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · full declaration

def weilHomEquiv :
    (HomRing (R := R) (A := A) (B := B) P →ₐ[R] C) ≃
      (B →ₐ[R] C ⊗[R] A) where
  toFun := homForward (P := P)
  invFun := liftCoefficients (P := P)
  left_inv := liftCoefficients_homForward (P := P)
  right_inv := homForward_liftCoefficients (P := P)

lemma

homForward_comp

L312 ↗

CommAlgCat.homForward_comp

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma homForward_comp
    {D : Type u} [CommRing D] [Algebra R D]
    (h : HomRing (R := R) (A := A) (B := B) P →ₐ[R] C)
    (k : C →ₐ[R] D) :
    homForward (P := P) (k.comp h) =
      (Algebra.TensorProduct.map k (AlgHom.id R A)).comp
        (homForward (P := P) h)

def

categoryWeilHomEquiv

L323 ↗

CommAlgCat.categoryWeilHomEquiv

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · full declaration

def categoryWeilHomEquiv (S : CommAlgCat.{u} R) :
    (CommAlgCat.of R (HomRing (R := R) (A := A) (B := B) P) ⟶ S) ≃
      (CommAlgCat.of R B ⟶
        (MonoidalCategory.tensorRight (CommAlgCat.of R A)).obj S) where
  toFun f := CommAlgCat.ofHom (homForward (P := P) f.hom)
  invFun g := CommAlgCat.ofHom (liftCoefficients (P := P) g.hom)
  left_inv f := by
    apply CommAlgCat.hom_ext
    exact liftCoefficients_homForward (P := P) f.hom
  right_inv g := by
    apply CommAlgCat.hom_ext
    exact homForward_liftCoefficients (P := P) g.hom

lemma

categoryWeilHomEquiv_comp

L336 ↗

CommAlgCat.categoryWeilHomEquiv_comp

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma categoryWeilHomEquiv_comp {S T : CommAlgCat.{u} R}
    (f : CommAlgCat.of R (HomRing (R := R) (A := A) (B := B) P) ⟶ S)
    (g : S ⟶ T) :
    categoryWeilHomEquiv (P := P) T (f ≫ g) =
      categoryWeilHomEquiv (P := P) S f ≫
        (MonoidalCategory.tensorRight (CommAlgCat.of R A)).map g

def

corepresentableBy

L348 ↗

CommAlgCat.corepresentableBy

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · full declaration

def corepresentableBy :
    ((MonoidalCategory.tensorRight (CommAlgCat.of R A)) ⋙
      coyoneda.obj (Opposite.op (CommAlgCat.of R B))).CorepresentableBy
        (CommAlgCat.of R (HomRing (R := R) (A := A) (B := B) P)) where
  homEquiv {Y} := categoryWeilHomEquiv (P := P) Y
  homEquiv_comp g f := categoryWeilHomEquiv_comp (P := P) f g

lemma

leftAdjointObjIsDefined

L355 ↗

CommAlgCat.leftAdjointObjIsDefined

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

lemma leftAdjointObjIsDefined (P : Algebra.Presentation R B ι σ) :
    (MonoidalCategory.tensorRight (CommAlgCat.of R A)).leftAdjointObjIsDefined
      (CommAlgCat.of R B)

theorem

tensorRight_leftAdjointObjIsDefined

L369 ↗

CommAlgCat.tensorRight_leftAdjointObjIsDefined

Documentation

If A is finite free over R and B is finitely presented over R, then tensoring commutative R-algebras with A has a left-adjoint object at B. Equivalently, the functor C ↦ Hom_R(B, C ⊗[R] A) is corepresentable.

This is the affine source lemma for the relative internal Hom in Stacks Project, Tag 0BL7.

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct BigOperators
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open TensorProduct
open Module
universe u
namespace CommAlgCat
variable {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R B]
variable [Module.Free R A] [Module.Finite R A]
  {ι σ : Type u} (P : Algebra.Presentation R B ι σ)
variable {C : Type u} [CommRing C] [Algebra R C]

Lean source · statement

theorem tensorRight_leftAdjointObjIsDefined
    [Algebra.FinitePresentation R B] :
    (MonoidalCategory.tensorRight (CommAlgCat.of R A)).leftAdjointObjIsDefined
      (CommAlgCat.of R B)

Module documentation

Affine Weil restriction along a finite free algebra

Declarations