theorem
L30 ↗baseChange
AlgebraicGeometry.RelPicard.IsAlgEquivZero.baseChange
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.S_AlgebraicGeometry_RelPicard_IsAlgEquivZero_baseChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfraLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.IsAlgEquivZero.baseChange
{k : Type u} [Field k] (K : Type u) [Field K] [Algebra k K]
{A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k)) {L : A.Modules} (hL : IsAlgEquivZero a L) :
IsAlgEquivZero (pullback.snd a (Spec.map (CommRingCat.ofHom (algebraMap k K))))
((Scheme.Modules.pullback
(pullback.fst a (Spec.map (CommRingCat.ofHom (algebraMap k K))))).obj L)