Documentation

Atlas.ArithmeticGeometry.code.PicardGroup

source
noncomputable def Theorem19_14.divMap (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] :
Fˣ → CurveDivisor C
Instances For
    source
    noncomputable def Theorem19_14.toPicMap (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] :
    CurveDivisor C →+ CurveDivisor C ⧸ CurveWithOrd.principalDivisors
    Instances For
      source
      theorem Theorem19_14.exact_at_functionField_mathlib (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] :
      Function.Exact (⇑CurveWithConstants.constantsEmb) (divMap C k F)
      source
      theorem Theorem19_14.exact_at_DivGroup_mathlib (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] :
      Function.Exact (divMap C k F) ⇑(toPicMap C k F)
      source
      theorem Theorem19_14.toPicMap_surjective (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] :
      Function.Surjective ⇑(toPicMap C k F)
      source
      theorem Theorem19_14.picard_exact_sequence (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] :
      Function.Injective ⇑CurveWithConstants.constantsEmb ∧ Function.Exact (⇑CurveWithConstants.constantsEmb) (divMap C k F) ∧ Function.Exact (divMap C k F) ⇑(toPicMap C k F) ∧ Function.Surjective ⇑(toPicMap C k F)