NYLL
Module

SemilinearAut_pic0_correspondence_swap_smul.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_pic0_correspondence_swap_smul
12 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut pic0 correspondence swap smul

Imports1
Imported by1

Declarations

def

CrossIntertwines

L33 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.CrossIntertwines
Documentation

The two embeddings intertwine the source and target semilinear actions in the stated order.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
def CrossIntertwines (φ ψ : F →ₐ[K] F') (g : SemilinearAut K F) (g' : SemilinearAut K F') :
    Prop
theorem

inv

L37 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.CrossIntertwines.inv
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem CrossIntertwines.inv (h : CrossIntertwines φ ψ g g') :
    CrossIntertwines ψ φ g⁻¹ g'⁻¹
theorem

restrictAlong_smul

L44 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.restrictAlong_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem restrictAlong_smul (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (h : CrossIntertwines φ ψ g g') (w : Place K F') :
    (g' • w).restrictAlong ψ hψ = g • w.restrictAlong φ hφ
theorem

ord_smul

L56 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.ord_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem ord_smul (h : CrossIntertwines φ ψ g g') (w : Place K F') (f : F) :
    (g' • w).ord (ψ f) = w.ord (φ (g⁻¹ • f))
theorem

ramificationIndexAlong_smul

L61 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.ramificationIndexAlong_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem ramificationIndexAlong_smul (h : CrossIntertwines φ ψ g g') (w : Place K F') :
    (g' • w).ramificationIndexAlong ψ = w.ramificationIndexAlong φ
def

restrictEquiv

L80 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.restrictEquiv
Documentation

The ring equivalence between restricted valuation rings induced by the intertwining semilinear automorphisms.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · full declaration
def restrictEquiv (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (h : CrossIntertwines φ ψ g g') (w : Place K F') :
    (w.restrictAlong φ hφ).toValuationSubring ≃+*
      ((g' • w).restrictAlong ψ hψ).toValuationSubring where
  toFun x := ⟨g • (x : F), by
    have hx : φ (x : F) ∈ w.toValuationSubring := x.2
    change ψ (g • (x : F)) ∈ (g' • w).toValuationSubring
    rw [SemilinearAut.smul_toValuationSubring, ← h (x : F)]
    exact ValuationSubring.smul_mem_pointwise_smul g' _ _ hx⟩
  invFun y := ⟨g⁻¹ • (y : F), by
    have hy : ψ (y : F) ∈ (g' • w).toValuationSubring := y.2
    change φ (g⁻¹ • (y : F)) ∈ w.toValuationSubring
    rw [SemilinearAut.smul_toValuationSubring,
      ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem] at hy
    rw [← h.inv (y : F)]
    exact hy⟩
  left_inv x := by ext; exact inv_smul_smul g (x : F)
  right_inv y := by ext; exact smul_inv_smul g (y : F)
  map_mul' x y := by ext; exact smul_mul' g (x : F) (y : F)
  map_add' x y := by ext; exact smul_add g (x : F) (y : F)
theorem

inertiaDegAlong_smul

L101 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.inertiaDegAlong_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem inertiaDegAlong_smul (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (h : CrossIntertwines φ ψ g g') (w : Place K F') :
    (g' • w).inertiaDegAlong ψ hψ = w.inertiaDegAlong φ hφ
theorem

pullbackAlong_smul

L123 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.pullbackAlong_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem pullbackAlong_smul [HasPrincipalDivisors K F'] (hφ : φ.toRingHom.IsIntegral)
    (hψ : ψ.toRingHom.IsIntegral) (h : CrossIntertwines φ ψ g g') (D : Divisor K F) :
    Divisor.pullbackAlong ψ hψ (g • D) = g' • Divisor.pullbackAlong φ hφ D
theorem

pushforwardAlong_smul

L131 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.pushforwardAlong_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem pushforwardAlong_smul (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (h : CrossIntertwines φ ψ g g') (E : Divisor K F') :
    Divisor.pushforwardAlong ψ hψ (g' • E) = g • Divisor.pushforwardAlong φ hφ E
theorem

correspondence_smul_exchange

L143 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.SwapSmul.correspondence_smul_exchange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
namespace SwapSmul
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable {g : SemilinearAut K F} {g' : SemilinearAut K F'}
variable {φ ψ : F →ₐ[K] F'}
Lean source · statement
theorem correspondence_smul_exchange [HasPrincipalDivisors K F']
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (h₁ : CrossIntertwines φ ψ g g') (h₂ : CrossIntertwines ψ φ g g') (D : Divisor K F) :
    Divisor.correspondence φ ψ hφ hψ (g • D) = g • Divisor.correspondence ψ φ hψ hφ D
theorem

solution

L153 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul.solution
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_pic0_correspondence_swap_smul
open AlgebraicCurve
open scoped _root_.Pointwise
open SwapSmul in
Lean source · statement
theorem solution {K F F' : Type*} [Field K]
    [Field F] [Field F'] [Algebra K F] [Algebra K F'] {g : SemilinearAut K F}
    {g' : SemilinearAut K F'} [HasPrincipalDivisors K F'] (φ ψ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hFIφ : FundamentalIdentityAlong K φ hφ) (hfinψ : FiniteAlong K ψ)
    (hNψ : NormFormulaAlong K ψ hfinψ)
    (hFIψ : FundamentalIdentityAlong K ψ hψ) (hfinφ : FiniteAlong K φ)
    (hNφ : NormFormulaAlong K φ hfinφ)
    (h₁ : ∀ x : F, g' • (φ x) = ψ (g • x)) (h₂ : ∀ x : F, g' • (ψ x) = φ (g • x))
    (c : Pic0 K F) :
    Pic0.correspondence φ ψ hφ hψ hFIφ hfinψ hNψ (g • c)
      = g • Pic0.correspondence ψ φ hψ hφ hFIψ hfinφ hNφ c
theorem

pic0_correspondence_swap_smul

L182 ↗
AlgebraicCurve.SemilinearAut.pic0_correspondence_swap_smul
Source context 3 commands

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

open AlgebraicCurve
open AlgebraicCurves.Divisors.Semilinear.Proofs in
open SemilinearAut_pic0_correspondence_swap_smul
  renaming solution → semilinearProof in
Lean source · statement
theorem AlgebraicCurve.SemilinearAut.pic0_correspondence_swap_smul {K F F' : Type*} [Field K]
    [Field F] [Field F'] [Algebra K F] [Algebra K F'] {g : SemilinearAut K F}
    {g' : SemilinearAut K F'} [HasPrincipalDivisors K F'] (φ ψ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hFIφ : FundamentalIdentityAlong K φ hφ) (hfinψ : FiniteAlong K ψ)
    (hNψ : NormFormulaAlong K ψ hfinψ)
    (hFIψ : FundamentalIdentityAlong K ψ hψ) (hfinφ : FiniteAlong K φ)
    (hNφ : NormFormulaAlong K φ hfinφ)
    (h₁ : ∀ x : F, g' • (φ x) = ψ (g • x)) (h₂ : ∀ x : F, g' • (ψ x) = φ (g • x))
    (c : Pic0 K F) :
    Pic0.correspondence φ ψ hφ hψ hFIφ hfinψ hNψ (g • c)
      = g • Pic0.correspondence ψ φ hψ hφ hFIψ hfinφ hNφ c

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