NYLL
Module

FiniteEtale.lean

Nyll.SchemeTheory.Affine.WeilRestriction.FiniteEtale
39 declarations indexed from sourceView source ↗

Module documentation

Finite étale affine Weil restriction

This file proves that the affine corepresenter constructed in SchemeTheory.Affine.WeilRestriction.Basic is compatible with arbitrary base change and is finite étale when both input algebras are finite étale.

These are the affine algebra ingredients for Stacks Project, Tag 0BL7.

Imports6
Imported by3

Declarations

def

tensorPower

L43 ↗
CommAlgCat.tensorPower
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
def tensorPower (B : CommAlgCat.{u} R) : ℕ → CommAlgCat.{u} R
  | 0 => of R R
  | n + 1 => B ⊗ tensorPower B n
def

binaryHomEquiv

L47 ↗
CommAlgCat.binaryHomEquiv
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
def binaryHomEquiv (X Y Z : CommAlgCat.{u} R) :
    (X ⊗ Y ⟶ Z) ≃ ((X ⟶ Z) × (Y ⟶ Z)) where
  toFun f := ((binaryCofan X Y).inl ≫ f, (binaryCofan X Y).inr ≫ f)
  invFun p := (binaryCofanIsColimit X Y).desc (BinaryCofan.mk p.1 p.2)
  left_inv f := by
    apply (binaryCofanIsColimit X Y).hom_ext
    intro j
    rw [(binaryCofanIsColimit X Y).fac
      (BinaryCofan.mk ((binaryCofan X Y).inl ≫ f) ((binaryCofan X Y).inr ≫ f)) j]
    rcases j with ⟨j⟩
    cases j <;> rfl
  right_inv p := by
    apply Prod.ext
    · exact (binaryCofanIsColimit X Y).fac (BinaryCofan.mk p.1 p.2) ⟨WalkingPair.left⟩
    · exact (binaryCofanIsColimit X Y).fac (BinaryCofan.mk p.1 p.2) ⟨WalkingPair.right⟩
def

tensorPowerHomEquiv

L63 ↗
CommAlgCat.tensorPowerHomEquiv
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
def tensorPowerHomEquiv (B C : CommAlgCat.{u} R) :
    (n : ℕ) → (tensorPower B n ⟶ C) ≃ (Fin n → (B ⟶ C))
  | 0 =>
      { toFun := fun _ i => Fin.elim0 i
        invFun := fun _ => isInitialSelf.to C
        left_inv := fun _ => isInitialSelf.hom_ext _ _
        right_inv := fun _ => funext fun i => Fin.elim0 i }
  | n + 1 =>
      (binaryHomEquiv B (tensorPower B n) C).trans <|
        ((Equiv.refl (B ⟶ C)).prodCongr (tensorPowerHomEquiv B C n)).trans <|
          Fin.consEquiv (fun _ : Fin (n + 1) => B ⟶ C)
lemma

tensorPowerHomEquiv_comp

L75 ↗
CommAlgCat.tensorPowerHomEquiv_comp
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
lemma tensorPowerHomEquiv_comp (B : CommAlgCat.{u} R) {C D : CommAlgCat.{u} R}
    (n : ℕ) (f : tensorPower B n ⟶ C) (g : C ⟶ D) :
    tensorPowerHomEquiv B D n (f ≫ g) =
      fun i => tensorPowerHomEquiv B C n f i ≫ g := by
  induction n with
  | zero =>
      funext i
      exact Fin.elim0 i
  | succ n ih =>
      funext i
      refine Fin.cases ?_ (fun j => ?_) i
      · change ((binaryCofan B (tensorPower B n)).inl ≫ f) ≫ g =
          (binaryCofan B (tensorPower B n)).inl ≫ (f ≫ g)
        exact Category.assoc _ _ _
      · change tensorPowerHomEquiv B D n
            (((binaryCofan B (tensorPower B n)).inr ≫ f) ≫ g) j =
          tensorPowerHomEquiv B C n
              ((binaryCofan B (tensorPower B n)).inr ≫ f) j ≫ g
        exact congrFun (ih ((binaryCofan B (tensorPower B n)).inr ≫ f)) j
def

tensorPiAlgEquiv

L95 ↗
CommAlgCat.tensorPiAlgEquiv
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
def tensorPiAlgEquiv (C : CommAlgCat.{u} R) (n : ℕ) :
    C ⊗[R] (Fin n → R) ≃ₐ[R] (Fin n → C)
lemma

tensorPiAlgEquiv_map

L100 ↗
CommAlgCat.tensorPiAlgEquiv_map
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
lemma tensorPiAlgEquiv_map {C D : CommAlgCat.{u} R} (n : ℕ) (g : C ⟶ D)
    (z : C ⊗[R] (Fin n → R)) (i : Fin n) :
    tensorPiAlgEquiv D n
        (Algebra.TensorProduct.map g.hom (AlgHom.id R (Fin n → R)) z) i =
      g.hom (tensorPiAlgEquiv C n z i)
def

homTensorPiEquiv

L109 ↗
CommAlgCat.homTensorPiEquiv
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
def homTensorPiEquiv (B C : CommAlgCat.{u} R) (n : ℕ) :
    (B ⟶ (MonoidalCategory.tensorRight (of R (Fin n → R))).obj C) ≃
      (Fin n → (B ⟶ C)) where
  toFun f i := ofHom <| (Pi.evalAlgHom R (fun _ : Fin n => C) i).comp <|
    (tensorPiAlgEquiv C n).toAlgHom.comp f.hom
  invFun f := ofHom <| (tensorPiAlgEquiv C n).symm.toAlgHom.comp <| AlgHom.pi fun i => (f i).hom
  left_inv f := by
    apply hom_ext
    ext x
    change (tensorPiAlgEquiv C n).symm (fun i => tensorPiAlgEquiv C n (f.hom x) i) = f.hom x
    rw [show (fun i => tensorPiAlgEquiv C n (f.hom x) i) =
      tensorPiAlgEquiv C n (f.hom x) by rfl]
    exact (tensorPiAlgEquiv C n).symm_apply_apply (f.hom x)
  right_inv f := by
    funext i
    apply hom_ext
    ext x
    change tensorPiAlgEquiv C n
      ((tensorPiAlgEquiv C n).symm (fun i => (f i).hom x)) i = (f i).hom x
    rw [(tensorPiAlgEquiv C n).apply_symm_apply]
lemma

homTensorPiEquiv_map

L130 ↗
CommAlgCat.homTensorPiEquiv_map
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
lemma homTensorPiEquiv_map (B : CommAlgCat.{u} R) {C D : CommAlgCat.{u} R}
    (n : ℕ) (f : B ⟶ (MonoidalCategory.tensorRight (of R (Fin n → R))).obj C)
    (g : C ⟶ D) :
    homTensorPiEquiv B D n
        (f ≫ (MonoidalCategory.tensorRight (of R (Fin n → R))).map g) =
      fun i => homTensorPiEquiv B C n f i ≫ g := by
  funext i
  apply hom_ext
  ext x
  exact tensorPiAlgEquiv_map n g (f.hom x) i
def

splitCorepresentableBy

L141 ↗
CommAlgCat.splitCorepresentableBy
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · full declaration
def splitCorepresentableBy (B : CommAlgCat.{u} R) (n : ℕ) :
    ((MonoidalCategory.tensorRight (of R (Fin n → R))) ⋙
      coyoneda.obj (Opposite.op B)).CorepresentableBy (tensorPower B n) where
  homEquiv {Y} := (tensorPowerHomEquiv B Y n).trans (homTensorPiEquiv B Y n).symm
  homEquiv_comp {Y Y'} g f := by
    apply (homTensorPiEquiv B Y' n).injective
    change homTensorPiEquiv B Y' n
        ((homTensorPiEquiv B Y' n).symm (tensorPowerHomEquiv B Y' n (f ≫ g))) =
      homTensorPiEquiv B Y' n
        ((homTensorPiEquiv B Y n).symm (tensorPowerHomEquiv B Y n f) ≫
          (MonoidalCategory.tensorRight (of R (Fin n → R))).map g)
    rw [Equiv.apply_symm_apply, homTensorPiEquiv_map, Equiv.apply_symm_apply]
    exact tensorPowerHomEquiv_comp B n f g
def

tensorRightIsoOfIso

L155 ↗
CommAlgCat.tensorRightIsoOfIso
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
def tensorRightIsoOfIso {A A' : CommAlgCat.{u} R} (e : A ≅ A') :
    MonoidalCategory.tensorRight A ≅ MonoidalCategory.tensorRight A'
def

splitCorepresentableByOfAlgEquiv

L160 ↗
CommAlgCat.splitCorepresentableByOfAlgEquiv
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
def splitCorepresentableByOfAlgEquiv
    {A : Type u} [CommRing A] [Algebra R A] (B : CommAlgCat.{u} R)
    {n : ℕ} (e : A ≃ₐ[R] (Fin n → R)) :
    ((MonoidalCategory.tensorRight (of R A)) ⋙ coyoneda.obj (Opposite.op B)).CorepresentableBy
      (tensorPower B n)
lemma

tensorPower_finite

L170 ↗
CommAlgCat.tensorPower_finite
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
lemma tensorPower_finite (B : CommAlgCat.{u} R) [Module.Finite R B] (n : ℕ) :
    Module.Finite R (tensorPower B n)
lemma

tensorPower_etale

L178 ↗
CommAlgCat.tensorPower_etale
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
lemma tensorPower_etale (B : CommAlgCat.{u} R) [Algebra.Etale R B] (n : ℕ) :
    Algebra.Etale R (tensorPower B n)
def

affineWeilRestriction

L193 ↗
CommAlgCat.affineWeilRestriction
Documentation

The commutative R-algebra corepresenting homomorphisms from B to tensor products with the finite free R-algebra A.

Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
def affineWeilRestriction
    {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] :
    CommAlgCat.{u} R
def

affineWeilRestrictionCorepresentableBy

L202 ↗
CommAlgCat.affineWeilRestrictionCorepresentableBy
Documentation

The canonical affine Weil restriction corepresents C ↦ Hom_R(B, C ⊗_R A).

Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
def affineWeilRestrictionCorepresentableBy
    {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] :
    ((MonoidalCategory.tensorRight (of R A)) ⋙
      coyoneda.obj (Opposite.op (of R B))).CorepresentableBy
      (affineWeilRestriction (R := R) (A := A) (B := B))
lemma

affineWeilRestriction_finite_etale_of_isFiniteSplit

L212 ↗
CommAlgCat.affineWeilRestriction_finite_etale_of_isFiniteSplit
Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
lemma affineWeilRestriction_finite_etale_of_isFiniteSplit
    {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Algebra.IsFiniteSplit R A]
    [Module.Finite R B] [Algebra.Etale R B] :
    Module.Finite R (affineWeilRestriction (R := R) (A := A) (B := B)) ∧
      Algebra.Etale R (affineWeilRestriction (R := R) (A := A) (B := B))
abbrev

AS

L238 ↗
CommAlgCat.AS
Source context 11 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev AS
abbrev

BS

L239 ↗
CommAlgCat.BS
Source context 11 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
abbrev BS
instance

(anonymous instance)

L241 ↗
Source context 11 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
Lean source · statement
instance : Module.Finite S (S ⊗[R] A)
abbrev

tensorRightR

L245 ↗
CommAlgCat.tensorRightR
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
abbrev tensorRightR
def

sourceR

L248 ↗
CommAlgCat.sourceR
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
def sourceR : tensorRightR (R := R) (A := A).PartialLeftAdjointSource
abbrev

HR

L251 ↗
CommAlgCat.HR
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
abbrev HR
abbrev

baseHR

L255 ↗
CommAlgCat.baseHR
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
abbrev baseHR : CommAlgCat S
abbrev

restrictObj

L258 ↗
CommAlgCat.restrictObj
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
abbrev restrictObj (C : CommAlgCat S) : CommAlgCat R
def

restrictMap

L262 ↗
CommAlgCat.restrictMap
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
def restrictMap {C D : CommAlgCat S} (f : C ⟶ D) :
    restrictObj (R := R) C ⟶ restrictObj (R := R) D
def

baseChangeHomEquiv

L270 ↗
CommAlgCat.baseChangeHomEquiv
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · full declaration
def baseChangeHomEquiv (C : CommAlgCat S) :
    (baseHR (R := R) (S := S) (A := A) (B := B) ⟶ C) ≃
      (HR (R := R) (A := A) (B := B) ⟶ restrictObj (R := R) C) where
  toFun f := by
    let : Algebra R C := Algebra.compHom C (algebraMap R S)
    let : IsScalarTower R S C := .of_algebraMap_eq' rfl
    exact ofHom
      ((Algebra.TensorProduct.liftEquivRight R S
        (HR (R := R) (A := A) (B := B)) C).symm f.hom)
  invFun f := by
    let : Algebra R C := Algebra.compHom C (algebraMap R S)
    let : IsScalarTower R S C := .of_algebraMap_eq' rfl
    exact ofHom
      (Algebra.TensorProduct.liftEquivRight R S
        (HR (R := R) (A := A) (B := B)) C f.hom)
  left_inv f := by
    apply hom_ext
    let : Algebra R C := Algebra.compHom C (algebraMap R S)
    let : IsScalarTower R S C := .of_algebraMap_eq' rfl
    exact Equiv.apply_symm_apply _ f.hom
  right_inv f := by
    apply hom_ext
    let : Algebra R C := Algebra.compHom C (algebraMap R S)
    let : IsScalarTower R S C := .of_algebraMap_eq' rfl
    exact Equiv.symm_apply_apply _ f.hom
lemma

baseChangeHomEquiv_comp

L296 ↗
CommAlgCat.baseChangeHomEquiv_comp
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
lemma baseChangeHomEquiv_comp {C D : CommAlgCat S}
    (f : baseHR (R := R) (S := S) (A := A) (B := B) ⟶ C) (g : C ⟶ D) :
    baseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) D (f ≫ g) =
      baseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) C f ≫
        restrictMap (R := R) g
abbrev

tensorRightS

L311 ↗
CommAlgCat.tensorRightS
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
abbrev tensorRightS
def

postcompAlgEquiv

L314 ↗
CommAlgCat.postcompAlgEquiv
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · full declaration
def postcompAlgEquiv {X Y : Type u}
    [CommRing X] [CommRing Y] [Algebra R X] [Algebra R Y]
    (e : X ≃ₐ[R] Y) : (B →ₐ[R] X) ≃ (B →ₐ[R] Y) where
  toFun f := e.toAlgHom.comp f
  invFun f := e.symm.toAlgHom.comp f
  left_inv f := by ext x; simp
  right_inv f := by ext x; simp
def

targetAlgHomEquiv

L322 ↗
CommAlgCat.targetAlgHomEquiv
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
def targetAlgHomEquiv (C : CommAlgCat S) :
    (B →ₐ[R] (tensorRightR (R := R) (A := A)).obj (restrictObj (R := R) C)) ≃
      (BS (R := R) (S := S) (B := B) →ₐ[S]
        (tensorRightS (R := R) (S := S) (A := A)).obj C)
lemma

targetAlgHomEquiv_apply

L336 ↗
CommAlgCat.targetAlgHomEquiv_apply
Source context 13 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
omit [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] in
Lean source · full declaration
lemma targetAlgHomEquiv_apply (C : CommAlgCat S)
    (f : B →ₐ[R]
      (tensorRightR (R := R) (A := A)).obj (restrictObj (R := R) C)) :
    letI : Algebra R C := Algebra.compHom C (algebraMap R S)
    letI : IsScalarTower R S C := .of_algebraMap_eq' rfl
    targetAlgHomEquiv (R := R) (S := S) (A := A) (B := B) C f =
        Algebra.TensorProduct.liftEquivRight R S B
          (C ⊗[S] AS (R := R) (S := S) (A := A))
            (((Algebra.TensorProduct.cancelBaseChange
              R S S C A).symm.restrictScalars R).toAlgHom.comp
              f) := by
  rfl
def

targetBaseChangeHomEquiv

L349 ↗
CommAlgCat.targetBaseChangeHomEquiv
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
def targetBaseChangeHomEquiv (C : CommAlgCat S) :
    (of R B ⟶ (tensorRightR (R := R) (A := A)).obj (restrictObj (R := R) C)) ≃
    (of S (BS (R := R) (S := S) (B := B)) ⟶
      (tensorRightS (R := R) (S := S) (A := A)).obj C)
lemma

cancelBaseChange_symm_map

L363 ↗
CommAlgCat.cancelBaseChange_symm_map
Source context 13 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
omit [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] in
Lean source · statement
lemma cancelBaseChange_symm_map {C D : CommAlgCat S}
    [Algebra R C] [Algebra R D]
    [IsScalarTower R S C] [IsScalarTower R S D]
    (g : C ⟶ D) (x : C ⊗[R] A) :
    (Algebra.TensorProduct.cancelBaseChange R S S D A).symm
        (Algebra.TensorProduct.map (g.hom.restrictScalars R) (AlgHom.id R A) x) =
      Algebra.TensorProduct.map g.hom (AlgHom.id S (S ⊗[R] A))
        ((Algebra.TensorProduct.cancelBaseChange R S S C A).symm x)
lemma

targetBaseChangeHomEquiv_comp

L376 ↗
CommAlgCat.targetBaseChangeHomEquiv_comp
Source context 13 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
omit [Module.Free R A] [Module.Finite R A] [Algebra.FinitePresentation R B] in
Lean source · statement
lemma targetBaseChangeHomEquiv_comp {C D : CommAlgCat S}
    (f : of R B ⟶
      (tensorRightR (R := R) (A := A)).obj (restrictObj (R := R) C))
    (g : C ⟶ D) :
    targetBaseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) D
        (f ≫ (tensorRightR (R := R) (A := A)).map (restrictMap (R := R) g)) =
      targetBaseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) C f ≫
        (tensorRightS (R := R) (S := S) (A := A)).map g
def

sourceS

L410 ↗
CommAlgCat.sourceS
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
def sourceS :
    tensorRightS (R := R) (S := S) (A := A).PartialLeftAdjointSource
abbrev

HS

L414 ↗
CommAlgCat.HS
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
abbrev HS
def

baseChangeCorepresentableBy

L419 ↗
CommAlgCat.baseChangeCorepresentableBy
Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · full declaration
def baseChangeCorepresentableBy :
    ((tensorRightS (R := R) (S := S) (A := A)) ⋙
      coyoneda.obj (Opposite.op (of S (BS (R := R) (S := S) (B := B))))).CorepresentableBy
        (baseHR (R := R) (S := S) (A := A) (B := B)) where
  homEquiv {Y} :=
    (baseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) Y).trans <|
      ((tensorRightR (R := R) (A := A)).partialLeftAdjointHomEquiv
        (X := sourceR (R := R) (A := A) (B := B))).trans <|
          targetBaseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) Y
  homEquiv_comp {Y Y'} g f := by
    change
      targetBaseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) Y'
          ((tensorRightR (R := R) (A := A)).partialLeftAdjointHomEquiv
            (baseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) Y' (f ≫ g))) =
        targetBaseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) Y
            ((tensorRightR (R := R) (A := A)).partialLeftAdjointHomEquiv
              (baseChangeHomEquiv (R := R) (S := S) (A := A) (B := B) Y f)) ≫
          (tensorRightS (R := R) (S := S) (A := A)).map g
    rw [baseChangeHomEquiv_comp, Functor.partialLeftAdjointHomEquiv_comp]
    exact targetBaseChangeHomEquiv_comp (R := R) (S := S) (A := A) (B := B) _ _
opaque

affineWeilRestrictionBaseChangeIso

L441 ↗
CommAlgCat.affineWeilRestrictionBaseChangeIso
Documentation

Affine Weil restriction commutes with arbitrary base change.

Source context 12 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
section BaseChange
variable {S A B : Type u}
  [CommRing S] [CommRing A] [CommRing B]
  [Algebra R S] [Algebra R A] [Algebra R B]
  [Module.Free R A] [Module.Finite R A]
  [Algebra.FinitePresentation R B]
local instance : Module.Finite S (S ⊗[R] A) :=
  Module.Finite.of_basis
    (Algebra.TensorProduct.basis S (Module.Free.chooseBasis R A))
Lean source · statement
opaque affineWeilRestrictionBaseChangeIso :
    of S (S ⊗[R] affineWeilRestriction (R := R) (A := A) (B := B)) ≅
      affineWeilRestriction
        (R := S) (A := S ⊗[R] A) (B := S ⊗[R] B)
theorem

affineWeilRestriction_finiteEtale

L456 ↗
CommAlgCat.affineWeilRestriction_finiteEtale
Documentation

If A and B are finite étale over R, then their affine Weil restriction corepresenter is finite étale over R.

Source context 9 commands

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

@[expose] public section
open scoped TensorProduct
noncomputable section
open CategoryTheory
open CategoryTheory.Limits
open CategoryTheory.MonoidalCategory
universe u
namespace CommAlgCat
variable {R : Type u} [CommRing R]
Lean source · statement
theorem affineWeilRestriction_finiteEtale
    {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Free R A] [Module.Finite R A] [Algebra.Etale R A]
    [Module.Finite R B] [Algebra.Etale R B] :
    finiteEtale R (affineWeilRestriction (R := R) (A := A) (B := B))

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