Module

GenusFF_eq_and_nonempty_pic0_addEquiv_of_algebraMap_eq_comp.lean

Nyll.JacobianVarieties.Pic0.GenusFF_eq_and_nonempty_pic0_addEquiv_of_algebraMap_eq_comp

31 declarations indexed from sourceView source ↗

Module documentation

Genus and Picard groups under a change of constant-field names

A ring equivalence between the constant fields transports places, divisors, and repartitions. The resulting quotient equivalences preserve genus and the Picard group.

Imports2

Imported by1

Nyll.JacobianVarieties.Pic0.All

theorem

trAlgebraMap

L33 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trAlgebraMap

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trAlgebraMap (e : k ≃+* K) (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (a : k) :
    algebraMap k F a = algebraMap K F (e a)

theorem

trFinrankEq

L38 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trFinrankEq

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trFinrankEq (e : k ≃+* K) {M M' : Type*} [AddCommGroup M] [Module k M]
    [AddCommGroup M']
    [Module K M'] (j : M ≃+ M') (hj : ∀ (c : k) (m : M), j (c • m) = e c • j m) :
    Module.finrank k M = Module.finrank K M'

def

trPlaceEquiv

L46 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPlaceEquiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · full declaration

def trPlaceEquiv (e : k ≃+* K) (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    Place k F ≃ Place K F where
  toFun v :=
    { toValuationSubring := v.toValuationSubring
      algebraMap_mem' := fun b => by
        have h : algebraMap K F b = algebraMap k F (e.symm b) := by
          rw [trAlgebraMap e he, RingEquiv.apply_symm_apply]
        rw [h]
        exact v.algebraMap_mem' _
      ne_top' := v.ne_top'
      isPrincipalIdealRing' := v.isPrincipalIdealRing' }
  invFun w :=
    { toValuationSubring := w.toValuationSubring
      algebraMap_mem' := fun a => by
        rw [trAlgebraMap e he]
        exact w.algebraMap_mem' _
      ne_top' := w.ne_top'
      isPrincipalIdealRing' := w.isPrincipalIdealRing' }
  left_inv _ := Place.ext rfl
  right_inv _ := Place.ext rfl

theorem

trPlaceEquiv_ord

L67 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPlaceEquiv_ord

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPlaceEquiv_ord (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (v : Place k F) (f : F) : (trPlaceEquiv e he v).ord f = v.ord f

theorem

trPlaceEquiv_symm_ord

L71 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPlaceEquiv_symm_ord

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPlaceEquiv_symm_ord (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (w : Place K F) (f : F) : ((trPlaceEquiv e he).symm w).ord f = w.ord f

theorem

trPlaceEquiv_symm_adicValuation

L75 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPlaceEquiv_symm_adicValuation

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPlaceEquiv_symm_adicValuation (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) (w : Place K F) (f : F) :
    ((trPlaceEquiv e he).symm w).adicValuation f = w.adicValuation f

theorem

trPlaceEquiv_adicValuation

L79 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPlaceEquiv_adicValuation

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPlaceEquiv_adicValuation (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) (v : Place k F) (f : F) :
    (trPlaceEquiv e he v).adicValuation f = v.adicValuation f

theorem

trResidueFinrank

L83 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trResidueFinrank

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trResidueFinrank (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (V : ValuationSubring F) [ak : Algebra k V] [aK : Algebra K V]
    (hk : ∀ a : k, (algebraMap k V a : F) = algebraMap k F a)
    (hK : ∀ b : K, (algebraMap K V b : F) = algebraMap K F b) :
    Module.finrank k (IsLocalRing.ResidueField V) =
      Module.finrank K (IsLocalRing.ResidueField V)

theorem

trPlaceEquiv_deg

L97 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPlaceEquiv_deg

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPlaceEquiv_deg (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (v : Place k F) : (trPlaceEquiv e he v).deg = v.deg

def

trDivisorEquiv

L105 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDivisorEquiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

def trDivisorEquiv (e : k ≃+* K) (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    Divisor k F ≃+ Divisor K F

theorem

trDivisorEquiv_degree

L109 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDivisorEquiv_degree

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trDivisorEquiv_degree (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (D : Divisor k F) : Divisor.degree (trDivisorEquiv e he D) = Divisor.degree D

theorem

trDivisorEquiv_isPrincipal

L122 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDivisorEquiv_isPrincipal

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trDivisorEquiv_isPrincipal (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (D : Divisor k F) : (trDivisorEquiv e he D).IsPrincipal ↔ D.IsPrincipal

theorem

trDivisorEquiv_map_degZero

L140 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDivisorEquiv_map_degZero

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trDivisorEquiv_map_degZero (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    (Divisor.degZero (K := k) (F := F)).map (trDivisorEquiv e he : Divisor k F →+ Divisor K F)
      = Divisor.degZero (K := K) (F := F)

def

trDegZeroEquiv

L156 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDegZeroEquiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

def trDegZeroEquiv (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    Divisor.degZero (K := k) (F := F) ≃+ Divisor.degZero (K := K) (F := F)

theorem

trDegZeroEquiv_coe

L162 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDegZeroEquiv_coe

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trDegZeroEquiv_coe (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (D : Divisor.degZero (K := k) (F := F)) :
    ((trDegZeroEquiv e he D : Divisor.degZero (K := K) (F := F)) : Divisor K F) =
      trDivisorEquiv e he D

theorem

trDegZeroEquiv_map_principal

L168 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trDegZeroEquiv_map_principal

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trDegZeroEquiv_map_principal (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    ((Divisor.principal (K := k) (F := F)).addSubgroupOf (Divisor.degZero (K := k) (F := F))).map
        (trDegZeroEquiv e he : Divisor.degZero (K := k) (F := F) →+
          Divisor.degZero (K := K) (F := F)) =
      (Divisor.principal (K := K) (F := F)).addSubgroupOf
        (Divisor.degZero (K := K) (F := F))

def

trPic0Equiv

L188 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPic0Equiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

def trPic0Equiv (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    Pic0 k F ≃+ Pic0 K F

def

trPiEquiv

L193 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPiEquiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · full declaration

def trPiEquiv (e : k ≃+* K) (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    (Place k F → F) ≃ₐ[F] (Place K F → F) where
  toFun α := fun w => α ((trPlaceEquiv e he).symm w)
  invFun β := fun v => β (trPlaceEquiv e he v)
  left_inv α := funext fun v => congrArg α ((trPlaceEquiv e he).symm_apply_apply v)
  right_inv β := funext fun w => congrArg β ((trPlaceEquiv e he).apply_symm_apply w)
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
  commutes' _ := rfl

theorem

trPiEquiv_apply

L203 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPiEquiv_apply

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPiEquiv_apply (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (α : Place k F → F) (w : Place K F) : trPiEquiv e he α w = α ((trPlaceEquiv e he).symm w)

theorem

trPiEquiv_map_repartitions

L207 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trPiEquiv_map_repartitions

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trPiEquiv_map_repartitions (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    (repartitions k F).map (trPiEquiv e he).toAlgHom = repartitions K F

def

trRepEquiv

L232 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

def trRepEquiv (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    ↥(repartitions k F) ≃ₐ[F] ↥(repartitions K F)

theorem

trRepEquiv_coe

L239 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv_coe

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trRepEquiv_coe (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (α : ↥(repartitions k F)) (w : Place K F) :
    ((trRepEquiv e he α : ↥(repartitions K F)) : Place K F → F) w
      = (α : Place k F → F) ((trPlaceEquiv e he).symm w)

theorem

trRepEquiv_mem_repartitionsOf

L245 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv_mem_repartitionsOf

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trRepEquiv_mem_repartitionsOf (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) (α : ↥(repartitions k F)) :
    trRepEquiv e he α ∈ repartitionsOf (0 : Divisor K F) ↔
      α ∈ repartitionsOf (0 : Divisor k F)

theorem

trRepEquiv_mem_principalRepartitions

L264 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv_mem_principalRepartitions

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trRepEquiv_mem_principalRepartitions (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) (α : ↥(repartitions k F)) :
    trRepEquiv e he α ∈ principalRepartitions K F ↔ α ∈ principalRepartitions k F

theorem

trRepEquiv_mem_sup

L278 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv_mem_sup

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trRepEquiv_mem_sup (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (α : ↥(repartitions k F)) :
    trRepEquiv e he α ∈ repartitionsOf (0 : Divisor K F) ⊔ principalRepartitions K F ↔
      α ∈ repartitionsOf (0 : Divisor k F) ⊔ principalRepartitions k F

theorem

trRepEquiv_map_sup

L299 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv_map_sup

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trRepEquiv_map_sup (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    ((repartitionsOf (0 : Divisor k F) ⊔ principalRepartitions k F).restrictScalars ℤ).map
        ((trRepEquiv e he).toAddEquiv.toIntLinearEquiv :
          ↥(repartitions k F) →ₗ[ℤ] ↥(repartitions K F))
      = (repartitionsOf (0 : Divisor K F) ⊔ principalRepartitions K F).restrictScalars ℤ

def

trH1Equiv

L317 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trH1Equiv

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

def trH1Equiv (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    H1 (0 : Divisor k F) ≃+ H1 (0 : Divisor K F)

theorem

trH1Equiv_mk

L327 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trH1Equiv_mk

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trH1Equiv_mk (e : k ≃+* K) (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (α : ↥(repartitions k F)) :
    trH1Equiv e he (Submodule.Quotient.mk α) = Submodule.Quotient.mk (trRepEquiv e he α)

theorem

trRepEquiv_smul

L331 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trRepEquiv_smul

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trRepEquiv_smul (e : k ≃+* K)
    (he : algebraMap k F = (algebraMap K F).comp e.toRingHom)
    (c : k) (α : ↥(repartitions k F)) : trRepEquiv e he (c • α) = e c • trRepEquiv e he α

theorem

trGenusFF

L340 ↗

JacobianVarieties.Pic0.Proofs.ConstantFieldGenus.trGenusFF

Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.ConstantFieldGenus
open AlgebraicCurve
section ConstantRenaming
variable {k K F : Type*} [Field k] [Field K] [Field F] [Algebra K F] [Algebra k F]

Lean source · statement

theorem trGenusFF (e : k ≃+* K) (he : algebraMap k F = (algebraMap K F).comp e.toRingHom) :
    genusFF k F = genusFF K F

theorem