NYLL
Module

Divisor_sum_galois_smul_eq_pullback_pushforward.lean

Nyll.AlgebraicCurves.Divisors.Divisor_sum_galois_smul_eq_pullback_pushforward
21 declarations indexed from sourceView source ↗

Module documentation

Divisor sum galois smul eq pullback pushforward

Imports6
Imported by1

Declarations

abbrev

act

L38 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.act
Documentation

The semilinear automorphism obtained by restricting an automorphism of the extension field.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
abbrev act (σ : M ≃ₐ[F] M) : SemilinearAut K M
theorem

act_mul

L40 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.act_mul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem act_mul (σ τ : M ≃ₐ[F] M) : act (K := K) (σ * τ) = act (K := K) σ * act (K := K) τ
theorem

act_one

L46 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.act_one
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem act_one : act (K := K) (1 : M ≃ₐ[F] M) = 1
theorem

act_smul_smul

L51 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.act_smul_smul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem act_smul_smul (σ τ : M ≃ₐ[F] M) (W : Place K M) :
    act (K := K) σ • (act (K := K) τ • W) = act (K := K) (σ * τ) • W
theorem

act_one_smul

L55 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.act_one_smul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem act_one_smul (W : Place K M) : act (K := K) (1 : M ≃ₐ[F] M) • W = W
theorem

act_algebraMap

L58 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.act_algebraMap
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem act_algebraMap (σ : M ≃ₐ[F] M) (f : F) :
    act (K := K) σ • algebraMap F M f = algebraMap F M f
theorem

ramificationIndex_act_smul

L64 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.ramificationIndex_act_smul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem ramificationIndex_act_smul (σ : M ≃ₐ[F] M) (W : Place K M) :
    (act (K := K) σ • W).ramificationIndex F = W.ramificationIndex F
theorem

restrict_act_smul

L82 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.restrict_act_smul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
omit [FiniteDimensional F M] in
Lean source · statement
theorem restrict_act_smul (σ : M ≃ₐ[F] M) (W : Place K M) :
    (act (K := K) σ • W).restrict F = W.restrict F
theorem

exists_act_smul_eq

L86 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.exists_act_smul_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem exists_act_smul_eq (W W' : Place K M) (h : W'.restrict F = W.restrict F) :
    ∃ σ : M ≃ₐ[F] M, act (K := K) σ • W = W'
def

transporter

L91 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.transporter
Documentation

The finite set of automorphisms carrying the first place to the second.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
def transporter (W W' : Place K M) : Finset (M ≃ₐ[F] M)
theorem

mem_transporter

L95 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.mem_transporter
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
omit [IsGalois F M] in
Lean source · statement
theorem mem_transporter {W W' : Place K M} {σ : M ≃ₐ[F] M} :
    σ ∈ transporter (F := F) W W' ↔ act (K := K) σ • W = W'
theorem

transporter_eq_image

L100 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.transporter_eq_image
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
omit [IsGalois F M] in
Lean source · full declaration
theorem transporter_eq_image [DecidableEq (M ≃ₐ[F] M)] (W W' : Place K M) (τ : M ≃ₐ[F] M)
    (hτ : act (K := K) τ • W = W') :
    transporter (F := F) W W' = (transporter (F := F) W W).image (fun σ => τ * σ) := by
  ext σ
  rw [mem_transporter, Finset.mem_image]
  constructor
  · intro h
    refine ⟨τ⁻¹ * σ, ?_, by group⟩
    rw [mem_transporter, ← act_smul_smul, h, ← hτ, act_smul_smul, inv_mul_cancel, act_one_smul]
  · rintro ⟨ρ, hρ, rfl⟩
    rw [mem_transporter] at hρ
    rw [← act_smul_smul, hρ, hτ]
theorem

card_transporter_eq

L113 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.card_transporter_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
omit [IsGalois F M] in
Lean source · statement
theorem card_transporter_eq (W W' : Place K M) (τ : M ≃ₐ[F] M) (hτ : act (K := K) τ • W = W') :
    (transporter (F := F) W W').card = (transporter (F := F) W W).card
theorem

card_univ_eq_sum

L119 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.card_univ_eq_sum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem card_univ_eq_sum (W : Place K M) :
    (Finset.univ : Finset (M ≃ₐ[F] M)).card
      = ∑ W' ∈ (W.restrict F).fiberOver M, (transporter (F := F) W W').card
theorem

card_transporter

L132 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.card_transporter
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem card_transporter (W W' : Place K M) (h : W'.restrict F = W.restrict F) :
    (transporter (F := F) W W').card = W.ramificationIndex F * W.inertiaDeg F
theorem

ramificationIndex_mul_inertiaDeg_eq

L153 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.ramificationIndex_mul_inertiaDeg_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem ramificationIndex_mul_inertiaDeg_eq (W W' : Place K M) (h : W'.restrict F = W.restrict F) :
    W'.ramificationIndex F * W'.inertiaDeg F = W.ramificationIndex F * W.inertiaDeg F
theorem

ramificationIndex_eq

L161 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.ramificationIndex_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem ramificationIndex_eq (W W' : Place K M) (h : W'.restrict F = W.restrict F) :
    W'.ramificationIndex F = W.ramificationIndex F
theorem

inertiaDeg_mul_ramificationIndex_eq

L166 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.inertiaDeg_mul_ramificationIndex_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem inertiaDeg_mul_ramificationIndex_eq (W W' : Place K M) (h : W'.restrict F = W.restrict F) :
    W.inertiaDeg F * W'.ramificationIndex F = W.ramificationIndex F * W.inertiaDeg F
theorem

sum_smul_single

L172 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.sum_smul_single
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
variable [HasPrincipalDivisors K M]
Lean source · statement
theorem sum_smul_single (W : Place K M) (n : ℤ) :
    ∑ σ : M ≃ₐ[F] M, act (K := K) σ • (Finsupp.single W n : Divisor K M)
      = Divisor.pullback M (Divisor.pushforward F (Finsupp.single W n))
theorem

main

L205 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward.GalTraceDiv.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
noncomputable section
namespace GalTraceDiv
open AlgebraicCurve AlgebraicCurve.SemilinearAut Finset
variable {K F M : Type*} [Field K] [Field F] [Field M]
variable [Algebra K F] [Algebra K M] [Algebra F M] [IsScalarTower K F M]
section Galois
variable [FiniteDimensional F M] [IsGalois F M]
variable [HasPrincipalDivisors K M]
Lean source · statement
theorem main (D : Divisor K M) :
    ∑ σ : M ≃ₐ[F] M, act (K := K) σ • D = Divisor.pullback M (Divisor.pushforward F D)
theorem

sum_galois_smul_eq_pullback_pushforward

L220 ↗
AlgebraicCurve.Divisor.sum_galois_smul_eq_pullback_pushforward
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_sum_galois_smul_eq_pullback_pushforward
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.sum_galois_smul_eq_pullback_pushforward
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
    [IsScalarTower K F F'] [FiniteDimensional F F'] [IsGalois F F']
    [AlgebraicCurve.HasPrincipalDivisors K F'] (D : AlgebraicCurve.Divisor K F') :
    ∑ σ : F' ≃ₐ[F] F', AlgebraicCurve.SemilinearAut.ofAlgAut (σ.restrictScalars K) • D
      = AlgebraicCurve.Divisor.pullback F' (AlgebraicCurve.Divisor.pushforward F D)

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