Module

Semilinear.lean

Nyll.AlgebraicCurves.Divisors.Semilinear

49 declarations indexed from sourceView source ↗

Module documentation

Algebra, divisors, and base change

Semilinear automorphisms act compatibly on valuation rings, residue fields, and degree-zero divisor classes.

Imports3

Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.Algebra.Ring.Action.End
Mathlib.LinearAlgebra.Dimension.Finrank

Imported by47

def

SemilinearAut

L33 ↗

AlgebraicCurve.SemilinearAut

Documentation

Pairs of field automorphisms compatible with the base-field algebra map.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def SemilinearAut : Subgroup (RingAut F × RingAut K) where
  carrier := {p | ∀ a : K, p.1 (algebraMap K F a) = algebraMap K F (p.2 a)}
  one_mem' _ := rfl
  mul_mem' := fun {p q} hp hq a => by
    change p.1 (q.1 (algebraMap K F a)) = algebraMap K F (p.2 (q.2 a))
    rw [hq a, hp (q.2 a)]
  inv_mem' := fun {p} hp a => by
    change p.1.symm (algebraMap K F a) = algebraMap K F (p.2.symm a)
    apply p.1.injective
    rw [RingEquiv.apply_symm_apply, hp (p.2.symm a), RingEquiv.apply_symm_apply]

theorem

mem_iff

L48 ↗

AlgebraicCurve.SemilinearAut.mem_iff

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem mem_iff {p : RingAut F × RingAut K} :
    p ∈ SemilinearAut K F ↔ ∀ a : K, p.1 (algebraMap K F a) = algebraMap K F (p.2 a)

def

toRingAut

L53 ↗

AlgebraicCurve.SemilinearAut.toRingAut

Documentation

The function-field automorphism of a semilinear automorphism.

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

def toRingAut (g : SemilinearAut K F) : F ≃+* F

def

baseAut

L56 ↗

AlgebraicCurve.SemilinearAut.baseAut

Documentation

The base-field automorphism of a semilinear automorphism.

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

def baseAut (g : SemilinearAut K F) : K ≃+* K

theorem

commutes

L58 ↗

AlgebraicCurve.SemilinearAut.commutes

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem commutes (g : SemilinearAut K F) (a : K) :
    toRingAut g (algebraMap K F a) = algebraMap K F (baseAut g a)

theorem

toRingAut_one

L62 ↗

AlgebraicCurve.SemilinearAut.toRingAut_one

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem toRingAut_one : toRingAut (1 : SemilinearAut K F) = 1

theorem

baseAut_one

L64 ↗

AlgebraicCurve.SemilinearAut.baseAut_one

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem baseAut_one : baseAut (1 : SemilinearAut K F) = 1

theorem

toRingAut_mul

L66 ↗

AlgebraicCurve.SemilinearAut.toRingAut_mul

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem toRingAut_mul (g h : SemilinearAut K F) :
    toRingAut (g * h) = toRingAut g * toRingAut h

theorem

baseAut_mul

L69 ↗

AlgebraicCurve.SemilinearAut.baseAut_mul

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem baseAut_mul (g h : SemilinearAut K F) :
    baseAut (g * h) = baseAut g * baseAut h

theorem

toRingAut_inv

L72 ↗

AlgebraicCurve.SemilinearAut.toRingAut_inv

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem toRingAut_inv (g : SemilinearAut K F) :
    toRingAut g⁻¹ = (toRingAut g).symm

theorem

baseAut_inv

L75 ↗

AlgebraicCurve.SemilinearAut.baseAut_inv

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem baseAut_inv (g : SemilinearAut K F) :
    baseAut g⁻¹ = (baseAut g).symm

instance

(anonymous instance)

L78 ↗

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · full declaration

instance : MulSemiringAction (SemilinearAut K F) F where
  smul g x := toRingAut g x
  one_smul _ := rfl
  mul_smul _ _ _ := rfl
  smul_zero g := map_zero (toRingAut g)
  smul_add g := map_add (toRingAut g)
  smul_one g := map_one (toRingAut g)
  smul_mul g := map_mul (toRingAut g)

theorem

smul_def

L87 ↗

AlgebraicCurve.SemilinearAut.smul_def

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem smul_def (g : SemilinearAut K F) (x : F) : g • x = toRingAut g x

theorem

inv_smul_def

L89 ↗

AlgebraicCurve.SemilinearAut.inv_smul_def

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem inv_smul_def (g : SemilinearAut K F) (x : F) : g⁻¹ • x = (toRingAut g).symm x

theorem

smul_algebraMap

L91 ↗

AlgebraicCurve.SemilinearAut.smul_algebraMap

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem smul_algebraMap (g : SemilinearAut K F) (a : K) :
    g • algebraMap K F a = algebraMap K F (baseAut g a)

def

ofAlgAut

L96 ↗

AlgebraicCurve.SemilinearAut.ofAlgAut

Documentation

An algebra automorphism viewed as a semilinear automorphism with identity base action.

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · full declaration

def ofAlgAut : (F ≃ₐ[K] F) →* SemilinearAut K F where
  toFun σ := ⟨((σ : F ≃+* F), 1), fun a => by simp⟩
  map_one' := Subtype.ext (by ext <;> rfl)
  map_mul' σ τ := Subtype.ext (by ext <;> rfl)

theorem

toRingAut_ofAlgAut

L101 ↗

AlgebraicCurve.SemilinearAut.toRingAut_ofAlgAut

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem toRingAut_ofAlgAut (σ : F ≃ₐ[K] F) : toRingAut (ofAlgAut σ) = (σ : F ≃+* F)

theorem

baseAut_ofAlgAut

L103 ↗

AlgebraicCurve.SemilinearAut.baseAut_ofAlgAut

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem baseAut_ofAlgAut (σ : F ≃ₐ[K] F) : baseAut (ofAlgAut σ) = 1

theorem

ofAlgAut_smul

L105 ↗

AlgebraicCurve.SemilinearAut.ofAlgAut_smul

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
variable {K F}

Lean source · statement

theorem ofAlgAut_smul (σ : F ≃ₐ[K] F) (x : F) : ofAlgAut σ • x = σ x

theorem

pointwise_smul_top

L116 ↗

AlgebraicCurve.SemilinearAut.pointwise_smul_top

Source context 8 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)

Lean source · statement

theorem pointwise_smul_top : g • (⊤ : ValuationSubring F) = ⊤

def

smulValuationSubringEquiv

L122 ↗

AlgebraicCurve.SemilinearAut.smulValuationSubringEquiv

Documentation

The valuation-ring equivalence induced by the semilinear action.

Source context 8 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)

Lean source · full declaration

def smulValuationSubringEquiv (A : ValuationSubring F) :
    A ≃+* (g • A : ValuationSubring F) where
  toFun x := ⟨g • (x : F), ValuationSubring.smul_mem_pointwise_smul g (x : F) A x.2⟩
  invFun y := ⟨g⁻¹ • (y : F),
    (ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem (g := g) (S := A)
      (x := (y : F))).mp y.2⟩
  left_inv x := by ext; simp
  right_inv y := by ext; simp
  map_mul' x y := by ext; simp
  map_add' x y := by ext; simp

theorem

coe_smulValuationSubringEquiv_apply

L133 ↗

AlgebraicCurve.SemilinearAut.coe_smulValuationSubringEquiv_apply

Source context 8 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)

Lean source · statement

theorem coe_smulValuationSubringEquiv_apply (A : ValuationSubring F) (x : A) :
    ((smulValuationSubringEquiv g A x : (g • A : ValuationSubring F)) : F) = g • (x : F)

instance

(anonymous instance)

L137 ↗

Source context 8 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)

Lean source · full declaration

instance : SMul (SemilinearAut K F) (Place K F) where
  smul g v :=
    { toValuationSubring := g • v.toValuationSubring
      algebraMap_mem' := fun a => by
        have h := ValuationSubring.smul_mem_pointwise_smul g
          (algebraMap K F ((baseAut g).symm a)) v.toValuationSubring
          (v.algebraMap_mem' ((baseAut g).symm a))
        rwa [smul_algebraMap, RingEquiv.apply_symm_apply] at h
      ne_top' := fun h => v.ne_top' <| by
        have h2 := congrArg (g⁻¹ • ·) h
        simpa [pointwise_smul_top] using h2
      isPrincipalIdealRing' :=
        IsPrincipalIdealRing.of_surjective
          (smulValuationSubringEquiv g v.toValuationSubring : _ ≃+* _)
          (smulValuationSubringEquiv g v.toValuationSubring).surjective }

theorem

smul_toValuationSubring

L156 ↗

AlgebraicCurve.SemilinearAut.smul_toValuationSubring

Source context 9 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)
variable (v : Place K F)

Lean source · statement

theorem smul_toValuationSubring : (g • v).toValuationSubring = g • v.toValuationSubring

instance

(anonymous instance)

L159 ↗

Source context 9 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)
variable (v : Place K F)

Lean source · full declaration

instance : MulAction (SemilinearAut K F) (Place K F) where
  one_smul v := by
    ext1
    rw [smul_toValuationSubring, one_smul]
  mul_smul g h v := by
    ext1
    simp only [smul_toValuationSubring]
    rw [mul_smul]

theorem

ord_smul

L168 ↗

AlgebraicCurve.SemilinearAut.ord_smul

Source context 9 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)
variable (v : Place K F)

Lean source · statement

theorem ord_smul (f : F) : (g • v).ord (g • f) = v.ord f

def

smulResidueRingEquiv

L189 ↗

AlgebraicCurve.SemilinearAut.smulResidueRingEquiv

Documentation

The residue-field equivalence induced by the semilinear action on the place.

Source context 9 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)
variable (v : Place K F)

Lean source · statement

def smulResidueRingEquiv : v.ResidueField ≃+* (g • v).ResidueField

theorem

smulResidueRingEquiv_algebraMap

L192 ↗

AlgebraicCurve.SemilinearAut.smulResidueRingEquiv_algebraMap

Source context 9 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)
variable (v : Place K F)

Lean source · statement

theorem smulResidueRingEquiv_algebraMap (a : K) :
    smulResidueRingEquiv g v (algebraMap K v.ResidueField a)
      = algebraMap K (g • v).ResidueField (baseAut g a)

theorem

deg_smul

L205 ↗

AlgebraicCurve.SemilinearAut.deg_smul

Source context 9 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}
variable (g : SemilinearAut K F)
variable (v : Place K F)

Lean source · statement

theorem deg_smul : (g • v).deg = v.deg

instance

(anonymous instance)

L218 ↗

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

instance : DistribMulAction (SemilinearAut K F) (Divisor K F)

theorem

divisor_smul_def

L221 ↗

AlgebraicCurve.SemilinearAut.divisor_smul_def

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem divisor_smul_def (g : SemilinearAut K F) (D : Divisor K F) :
    g • D = Finsupp.mapDomain (g • ·) D

theorem

smul_single

L224 ↗

AlgebraicCurve.SemilinearAut.smul_single

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_single (g : SemilinearAut K F) (v : Place K F) (n : ℤ) :
    g • Finsupp.single v n = Finsupp.single (g • v) n

theorem

divisor_smul_apply_smul

L228 ↗

AlgebraicCurve.SemilinearAut.divisor_smul_apply_smul

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem divisor_smul_apply_smul (g : SemilinearAut K F) (D : Divisor K F) (v : Place K F) :
    (g • D) (g • v) = D v

theorem

divisor_smul_apply

L233 ↗

AlgebraicCurve.SemilinearAut.divisor_smul_apply

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem divisor_smul_apply (g : SemilinearAut K F) (D : Divisor K F) (w : Place K F) :
    (g • D) w = D (g⁻¹ • w)

theorem

degree_smul

L238 ↗

AlgebraicCurve.SemilinearAut.degree_smul

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem degree_smul (g : SemilinearAut K F) (D : Divisor K F) :
    Divisor.degree (g • D) = Divisor.degree D

theorem

smul_mem_degZero

L246 ↗

AlgebraicCurve.SemilinearAut.smul_mem_degZero

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_mem_degZero (g : SemilinearAut K F) {D : Divisor K F}
    (hD : D ∈ Divisor.degZero (K := K) (F := F)) :
    g • D ∈ Divisor.degZero (K := K) (F := F)

theorem

smul_mem_principal

L251 ↗

AlgebraicCurve.SemilinearAut.smul_mem_principal

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_mem_principal (g : SemilinearAut K F) {D : Divisor K F}
    (hD : D ∈ Divisor.principal (K := K) (F := F)) :
    g • D ∈ Divisor.principal (K := K) (F := F)

def

degZeroSMulHom

L262 ↗

AlgebraicCurve.SemilinearAut.degZeroSMulHom

Documentation

The semilinear action restricted to degree-zero divisors.

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

def degZeroSMulHom (g : SemilinearAut K F) :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K) (F := F)

theorem

coe_degZeroSMulHom

L268 ↗

AlgebraicCurve.SemilinearAut.coe_degZeroSMulHom

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem coe_degZeroSMulHom (g : SemilinearAut K F) (D : Divisor.degZero (K := K) (F := F)) :
    (degZeroSMulHom g D : Divisor K F) = g • (D : Divisor K F)

instance

(anonymous instance)

L271 ↗

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · full declaration

instance : SMul (SemilinearAut K F) (Pic0 K F) where
  smul g := QuotientAddGroup.map _ _ (degZeroSMulHom g) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact smul_mem_principal g hD)

theorem

pic0_smul_mk

L277 ↗

AlgebraicCurve.SemilinearAut.pic0_smul_mk

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · statement

theorem pic0_smul_mk (g : SemilinearAut K F) (D : Divisor.degZero (K := K) (F := F)) :
    g • (Pic0.mk D) = Pic0.mk (degZeroSMulHom g D)

instance

(anonymous instance)

L280 ↗

Source context 7 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace SemilinearAut
open scoped Pointwise
variable {K F}

Lean source · full declaration

instance : DistribMulAction (SemilinearAut K F) (Pic0 K F) where
  one_smul x := by
    obtain ⟨D, rfl⟩ := Pic0.mk_surjective x
    rw [pic0_smul_mk]
    exact congrArg Pic0.mk (Subtype.ext (by rw [coe_degZeroSMulHom, one_smul]))
  mul_smul g h x := by
    obtain ⟨D, rfl⟩ := Pic0.mk_surjective x
    rw [pic0_smul_mk, pic0_smul_mk, pic0_smul_mk]
    exact congrArg Pic0.mk (Subtype.ext (by simp only [coe_degZeroSMulHom]; rw [mul_smul]))
  smul_zero g := by
    change g • Pic0.mk 0 = Pic0.mk 0
    rw [pic0_smul_mk]
    exact congrArg Pic0.mk (map_zero _)
  smul_add g x y := by
    obtain ⟨D, rfl⟩ := Pic0.mk_surjective x
    obtain ⟨E, rfl⟩ := Pic0.mk_surjective y
    change g • Pic0.mk (D + E) = Pic0.mk (degZeroSMulHom g D) + Pic0.mk (degZeroSMulHom g E)
    rw [pic0_smul_mk]
    exact congrArg Pic0.mk (map_add _ _ _)

theorem

smul_zsmul

L310 ↗

AlgebraicCurve.SemilinearAut.smul_zsmul

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace SemilinearAut
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem smul_zsmul (g : SemilinearAut K F) (m : ℤ) (x : Pic0 K F) :
    g • (m • x) = m • (g • x)

theorem

smul_mem_torsion

L314 ↗

AlgebraicCurve.SemilinearAut.smul_mem_torsion

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace SemilinearAut
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem smul_mem_torsion (g : SemilinearAut K F) {n : ℕ} {x : Pic0 K F}
    (hx : x ∈ Pic0.torsion K F n) : g • x ∈ Pic0.torsion K F n

instance

instSMulTorsion

L320 ↗

AlgebraicCurve.SemilinearAut.instSMulTorsion

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace SemilinearAut
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

instance instSMulTorsion (n : ℕ) : SMul (SemilinearAut K F) (Pic0.torsion K F n)

theorem

coe_torsion_smul

L323 ↗

AlgebraicCurve.SemilinearAut.coe_torsion_smul

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace SemilinearAut
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_torsion_smul {n : ℕ} (g : SemilinearAut K F) (x : Pic0.torsion K F n) :
    ((g • x : Pic0.torsion K F n) : Pic0 K F) = g • (x : Pic0 K F)

instance

instDistribMulActionTorsion

L326 ↗

AlgebraicCurve.SemilinearAut.instDistribMulActionTorsion

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace SemilinearAut
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

instance instDistribMulActionTorsion (n : ℕ) : DistribMulAction (SemilinearAut K F)
  (Pic0.torsion K F n) where
  one_smul x := Subtype.ext <| one_smul _ (x : Pic0 K F)
  mul_smul g h x := Subtype.ext <| mul_smul g h (x : Pic0 K F)
  smul_zero g := Subtype.ext <| smul_zero (A := Pic0 K F) g
  smul_add g x y := Subtype.ext <| smul_add g (x : Pic0 K F) (y : Pic0 K F)

instance

instModuleZModTorsion

L339 ↗

AlgebraicCurve.Pic0.instModuleZModTorsion

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace Pic0
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

instance instModuleZModTorsion (n : ℕ) : Module (ZMod n) (torsion K F n)

instance

instSMulCommClassZModTorsion

L352 ↗

AlgebraicCurve.SemilinearAut.instSMulCommClassZModTorsion

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
namespace SemilinearAut
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

instance instSMulCommClassZModTorsion (n : ℕ) :
    SMulCommClass (SemilinearAut K F) (ZMod n) (Pic0.torsion K F n) where
  smul_comm g c x :=
    ZMod.map_smul (DistribSMul.toAddMonoidHom (Pic0.torsion K F n) g) c x

Module documentation

Algebra, divisors, and base change

Declarations