EtaleFundamentalGroups.StrictHenselian.geometricStalkGenericTensorEquiv
Compare the actual generic tensor over the original fraction field with the tensor over the original ring, retaining the actual stalk's scalars.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [IsLocalRing R]
[Field Ω] [IsSepClosed Ω] (φ : R →+* Ω) [IsLocalHom φ]Lean source · full declaration
def geometricStalkGenericTensorEquiv
(B : Type u) [CommRing B] [Algebra R B] [Algebra (FractionRing R) B]
[IsScalarTower R (FractionRing R) B] :
letI : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
(geometricStalkStructureMap φ).toAlgebra
letI : Algebra (FractionRing R)
(FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) :=
(geometricStalkFractionFieldMap φ).toAlgebra
(geometricStalk (Spec.map (CommRingCat.ofHom φ)) ⊗[R] B) ≃ₐ[
geometricStalk (Spec.map (CommRingCat.ofHom φ))]
(FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))) ⊗[FractionRing R] B) := by
let A := geometricStalk (Spec.map (CommRingCat.ofHom φ))
let K := FractionRing R
let F := FractionRing A
letI : Algebra R A := (geometricStalkStructureMap φ).toAlgebra
letI : Algebra K F := (geometricStalkFractionFieldMap φ).toAlgebra
let e : (A ⊗[R] K) ≃ₐ[A] F := geometricStalkFractionTensorEquiv φ
letI : Algebra K (A ⊗[R] K) := Algebra.TensorProduct.rightAlgebra
have hmap : e.toRingHom.comp
(Algebra.TensorProduct.includeRight : K →ₐ[R] (A ⊗[R] K)).toRingHom =
geometricStalkFractionFieldMap φ := by
apply IsFractionRing.ringHom_ext (A := R)
intro r
change e ((Algebra.TensorProduct.includeRight : K →ₐ[R] (A ⊗[R] K))
(algebraMap R K r)) = geometricStalkFractionFieldMap φ (algebraMap R K r)
rw [AlgHom.commutes]
change e (algebraMap A (A ⊗[R] K) (geometricStalkStructureMap φ r)) = _
rw [e.commutes]
exact (geometricStalkFractionFieldMap_algebraMap φ r).symm
let eK : (A ⊗[R] K) ≃ₐ[K] F :=
{ __ := e.toRingEquiv
commutes' k := RingHom.congr_fun hmap k }
let et : ((A ⊗[R] K) ⊗[K] B) ≃ₐ[K] (F ⊗[K] B) :=
Algebra.TensorProduct.congr eK (AlgEquiv.refl : B ≃ₐ[K] B)
let etA : ((A ⊗[R] K) ⊗[K] B) ≃ₐ[A] (F ⊗[K] B) :=
{ __ := et.toRingEquiv
commutes' a := by
change e (algebraMap A (A ⊗[R] K) a) ⊗ₜ[K] (1 : B) =
algebraMap A F a ⊗ₜ[K] (1 : B)
exact congrArg (fun x : F => x ⊗ₜ[K] (1 : B)) (e.commutes a) }
exact (SchemeTheory.localizationTensorTowerEquiv R K A B R⁰).symm.trans etA