NYLL
Module

GenusFF_eq_of_algEquiv.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusFF_eq_of_algEquiv
18 declarations indexed from sourceView source ↗

Module documentation

The function-field genus is invariant under an algebra equivalence. Transport of places and repartitions identifies the defining quotient spaces.

Imports1
Imported by9

Declarations

theorem

adicValuation_le_one_iff_mem

L39 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.Place.adicValuation_le_one_iff_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Helpers
variable {F : Type*} [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.adicValuation_le_one_iff_mem (v : Place K F) (x : F) :
    v.adicValuation x ≤ 1 ↔ x ∈ v.toValuationSubring
def

congr

L62 ↗
AlgebraicCurve.Place.congr
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
namespace Place
open scoped _root_.AlgebraicCurve.Place in
Lean source · full declaration
def _root_.AlgebraicCurve.Place.congr (v : Place K F₁) : Place K F₂ where
  toValuationSubring := v.toValuationSubring.comap e.symm
  algebraMap_mem' a := by
    change (e.symm : F₂ →+* F₁) (algebraMap K F₂ a) ∈ v.toValuationSubring
    simp only [RingHom.coe_coe, AlgEquiv.commutes]
    exact v.algebraMap_mem' a
  ne_top' := by
    intro htop
    apply v.ne_top'
    refine SetLike.ext fun x => ⟨fun _ => ValuationSubring.mem_top x, fun _ => ?_⟩
    have : e x ∈ v.toValuationSubring.comap (e.symm : F₂ →+* F₁) :=
      htop ▸ ValuationSubring.mem_top _
    rw [ValuationSubring.mem_comap] at this
    simpa using this
  isPrincipalIdealRing' := by
    have := v.isPrincipalIdealRing'
    let σ : ↥v.toValuationSubring →+* ↥(v.toValuationSubring.comap (e.symm : F₂ →+* F₁)) :=
      { toFun := fun x => ⟨e x.1, by
          change (e.symm : F₂ →+* F₁) (e x.1) ∈ v.toValuationSubring; simp⟩
        map_one' := Subtype.ext (map_one _)
        map_mul' := fun _ _ => Subtype.ext (map_mul _ _ _)
        map_zero' := Subtype.ext (map_zero _)
        map_add' := fun _ _ => Subtype.ext (map_add _ _ _) }
    refine IsPrincipalIdealRing.of_surjective σ (fun y => ?_)
    have hy₁ : e.symm (y : F₂) ∈ v.toValuationSubring := by
      have h := y.2; rwa [ValuationSubring.mem_comap] at h
    exact ⟨⟨e.symm y.1, hy₁⟩, Subtype.ext (e.apply_symm_apply y.1)⟩
theorem

congr_toValuationSubring

L93 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.Place.congr_toValuationSubring
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.congr_toValuationSubring (v : Place K F₁) :
    (v.congr e).toValuationSubring = v.toValuationSubring.comap e.symm
theorem

mem_congr_iff

L98 ↗
AlgebraicCurve.Place.mem_congr_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
namespace Place
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_congr_iff (v : Place K F₁) (x : F₁) :
    e x ∈ (v.congr e).toValuationSubring ↔ x ∈ v.toValuationSubring
theorem

congr_symm_congr

L106 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.Place.congr_symm_congr
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.congr_symm_congr (v : Place K F₁) :
    (v.congr e).congr e.symm = v
theorem

congr_congr_symm

L114 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.Place.congr_congr_symm
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.congr_congr_symm (w : Place K F₂) :
    (w.congr e.symm).congr e = w
theorem

congr_adicValuation_le_one_iff

L120 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.Place.congr_adicValuation_le_one_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.congr_adicValuation_le_one_iff (v : Place K F₁) (x : F₁) :
    (v.congr e).adicValuation (e x) ≤ 1 ↔ v.adicValuation x ≤ 1
def

piMap

L129 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.piMap
Documentation

Transport a family of field elements along the algebra equivalence and its induced place equivalence.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
def piMap : (Place K F₁ → F₁) →+* (Place K F₂ → F₂)
theorem

piMap_apply

L132 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.piMap_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem piMap_apply (α : Place K F₁ → F₁) (w : Place K F₂) :
    piMap e α w = e (α (w.congr e.symm))
theorem

piMap_symm_piMap

L135 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.piMap_symm_piMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem piMap_symm_piMap (α : Place K F₁ → F₁) :
    piMap e.symm (piMap e α) = α
theorem

piMap_algebraMap

L141 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.piMap_algebraMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem piMap_algebraMap (c : F₁) :
    piMap e (algebraMap F₁ (Place K F₁ → F₁) c) = algebraMap F₂ _ (e c)
theorem

piMap_mem_repartitions

L145 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.piMap_mem_repartitions
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem piMap_mem_repartitions :
    ∀ α ∈ (repartitions K F₁ : Set _), piMap e α ∈ repartitions K F₂
def

repLinMap

L168 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.repLinMap
Documentation

Transport repartitions along the algebra equivalence as a linear map.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · full declaration
def repLinMap : ↥(repartitions K F₁) →ₗ[K] ↥(repartitions K F₂) where
  toFun α := ⟨piMap e α, piMap_mem_repartitions e α α.2⟩
  map_add' α β := Subtype.ext (map_add _ _ _)
  map_smul' c α := by
    apply Subtype.ext
    ext w
    simp only [RingHom.id_apply, Subalgebra.coe_smul, piMap_apply, Pi.smul_apply,
      _root_.map_smul]
theorem

repLinMap_apply_coe

L177 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.repLinMap_apply_coe
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem repLinMap_apply_coe (α : ↥(repartitions K F₁)) :
    ((repLinMap e α : repartitions K F₂) : Place K F₂ → F₂) = piMap e ↑α
theorem

repLinMap_symm_repLinMap

L180 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.repLinMap_symm_repLinMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem repLinMap_symm_repLinMap (α : ↥(repartitions K F₁)) :
    repLinMap e.symm (repLinMap e α) = α
theorem

repLinMap_mem_repartitionsOf_zero

L184 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.repLinMap_mem_repartitionsOf_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem repLinMap_mem_repartitionsOf_zero (α : ↥(repartitions K F₁))
    (hα : α ∈ repartitionsOf (0 : Divisor K F₁)) :
    repLinMap e α ∈ repartitionsOf (0 : Divisor K F₂)
theorem

repLinMap_mem_principal

L195 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv.AlgebraicCurve.repLinMap_mem_principal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K : Type*} [Field K]
section Congr
variable {F₁ F₂ : Type*} [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
variable (e : F₁ ≃ₐ[K] F₂)
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem repLinMap_mem_principal (α : ↥(repartitions K F₁))
    (hα : α ∈ principalRepartitions K F₁) :
    repLinMap e α ∈ principalRepartitions K F₂
theorem

genusFF_eq_of_algEquiv

L210 ↗
AlgebraicCurve.genusFF_eq_of_algEquiv
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.GenusFF_eq_of_algEquiv
open _root_.AlgebraicCurve
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs in
Lean source · statement
theorem _root_.AlgebraicCurve.genusFF_eq_of_algEquiv
    {K F₁ F₂ : Type*} [Field K] [Field F₁] [Field F₂] [Algebra K F₁] [Algebra K F₂]
    (e : F₁ ≃ₐ[K] F₂) :
    genusFF K F₁ = genusFF K F₂

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.