Extend the map (x,y) ↦ q(x/y) from D(y) to the affine plane. Pulling this extension back by (x,y) ↦ (xy,y) agrees with q(x) on D(y), hence everywhere by separatedness. Restriction to y = 0 proves constancy.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]abbrev PlaneSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]abbrev ChartSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]def scaling : Plane k →+* Plane kSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scaling_X : scaling k Polynomial.X = Polynomial.XSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scaling_C (p : k[X]) : scaling k (Polynomial.C p) =
Polynomial.eval₂RingHom (algebraMap k (Plane k))
(Polynomial.C Polynomial.X * Polynomial.X) pSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scaling_C_C (a : k) :
scaling k (Polynomial.C (Polynomial.C a)) = Polynomial.C (Polynomial.C a)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]def scalingChart : Chart k →+* Chart kSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scalingChart_comp :
(scalingChart k).comp (algebraMap (Plane k) (Chart k)) =
(algebraMap (Plane k) (Chart k)).comp (scaling k)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scalingChart_apply (p : Plane k) :
scalingChart k (algebraMap (Plane k) (Chart k) p) =
algebraMap (Plane k) (Chart k) (scaling k p)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scalingChart_invSelf :
scalingChart k (IsLocalization.Away.invSelf (Polynomial.X : Plane k)) =
IsLocalization.Away.invSelf (Polynomial.X : Plane k)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]def ratio : k[X] →+* Chart kSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma ratio_C (a : k) : ratio k (Polynomial.C a) = algebraMap k (Chart k) aSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scalingChart_ratio :
(scalingChart k).comp (ratio k) =
(algebraMap (Plane k) (Chart k)).comp Polynomial.CSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma scaling_comp_base :
(scaling k).comp (algebraMap k (Plane k)) = algebraMap k (Plane k)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma ratio_comp_base :
(ratio k).comp (algebraMap k k[X]) = algebraMap k (Chart k)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]def zeroLine : Plane k →+* k[X]Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]def origin : Plane k →+* kSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma zeroLine_comp_scaling :
(zeroLine k).comp (scaling k) =
(algebraMap k k[X]).comp (origin k)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma zeroLine_comp_C : (zeroLine k).comp Polynomial.C = RingHom.id k[X]Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
namespace AffineLineConstancy
variable (k : Type u) [Field k]lemma origin_comp_base :
(origin k).comp (algebraMap k (Plane k)) = RingHom.id kEvery morphism over a field from the affine line to an abelian variety is constant.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Polynomial
namespace GoodReductionJacobian
open AffineLineConstancy intheorem exists_eq_const_of_affineLine
(k : Type u) [Field k] {A : Scheme.{u}} {fA : A ⟶ Spec (CommRingCat.of k)}
(hA : AbelianSchemePropertyBundle k fA)
(q : Spec (CommRingCat.of k[X]) ⟶ A)
(hq : q ≫ fA = Spec.map (CommRingCat.ofHom (algebraMap k k[X]))) :
∃ a : Spec (CommRingCat.of k) ⟶ A,
a ≫ fA = 𝟙 _ ∧ q = Spec.map (CommRingCat.ofHom (algebraMap k k[X])) ≫ a