Module

Pic0_torsion_bijective_of_injective.lean

Nyll.JacobianVarieties.Pic0.Pic0_torsion_bijective_of_injective

5 declarations indexed from sourceView source ↗

Module documentation

An injective map from Picard torsion to its character group is bijective under the finite-cardinality and roots-of-unity hypotheses.

Imports4

Nyll.JacobianVarieties.Autoduality.Cohomology
Mathlib.GroupTheory.FiniteAbelian.Duality
Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Mathlib.SetTheory.Cardinal.Finite

Imported by3

def

monoidHomUnitsEquiv

L37 ↗

JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective.AlgebraicCurve.WC6Sol.monoidHomUnitsEquiv

Documentation

A homomorphism from a group to a monoid factors uniquely through its units.

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC6Sol

Lean source · full declaration

def monoidHomUnitsEquiv (G M : Type*) [Group G] [Monoid M] :
    (G →* M) ≃ (G →* Mˣ) where
  toFun := MonoidHom.toHomUnits
  invFun φ := (Units.coeHom M).comp φ
  left_inv _ := MonoidHom.ext fun _ => rfl
  right_inv _ := MonoidHom.ext fun _ => Units.ext rfl

theorem

card_addChar_eq_of_exponent

L44 ↗

JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective.AlgebraicCurve.WC6Sol.card_addChar_eq_of_exponent

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC6Sol

Lean source · statement

theorem card_addChar_eq_of_exponent {A K : Type*} [AddCommGroup A] [Field K]
    [Finite A] [HasEnoughRootsOfUnity K (Monoid.exponent (Multiplicative A))] :
    Nat.card (AddChar A K) = Nat.card A

theorem

card_addChar_eq

L51 ↗

JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective.AlgebraicCurve.WC6Sol.card_addChar_eq

Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC6Sol

Lean source · statement

theorem card_addChar_eq {A K : Type*} [AddCommGroup A] [Field K] [Finite A]
    {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] (hn : ∀ a : A, n • a = 0) :
    Nat.card (AddChar A K) = Nat.card A

theorem

card_homPic0Gm_eq

L63 ↗

JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective.AlgebraicCurve.WC6Sol.card_homPic0Gm_eq

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace WC6Sol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem card_homPic0Gm_eq {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n]
    [Finite (Pic0.torsion K F n)] :
    Nat.card (HomPic0Gm K F n) = Nat.card (Pic0.torsion K F n)

theorem

bijective_of_injective

L74 ↗

AlgebraicCurve.Pic0.torsion.bijective_of_injective

Source context 4 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_torsion_bijective_of_injective
noncomputable section
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Pic0.torsion.bijective_of_injective {K F : Type*} [Field K] [Field F]
    [Algebra K F] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] [Finite (Pic0.torsion K F n)]
    (f : Pic0.torsion K F n →+ Additive (HomPic0Gm K F n)) (hf : Function.Injective f) :
    Function.Bijective f

Module documentation

Declarations

monoidHomUnitsEquiv

card_addChar_eq_of_exponent

card_addChar_eq

card_homPic0Gm_eq

bijective_of_injective