Module

Place_smul_restrictAlong.lean

Nyll.AlgebraicCurves.Places.Place_smul_restrictAlong

8 declarations indexed from sourceView source ↗

Module documentation

Place smul restrict Along

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

mem_restrictAlong_iff

L33 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.mem_restrictAlong_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem mem_restrictAlong_iff (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w : Place K F') (f :
  F) :
    f ∈ (w.restrictAlong φ hφ).toValuationSubring ↔ φ f ∈ w.toValuationSubring

theorem

mem_smul_iff

L37 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.mem_smul_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem mem_smul_iff (σ : F' ≃ₐ[K] F') (w : Place K F') (x : F') :
    x ∈ (σ • w).toValuationSubring ↔ σ.symm x ∈ w.toValuationSubring

theorem

deg_restrictAlong_mul_inertiaDegAlong

L42 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.deg_restrictAlong_mul_inertiaDegAlong

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem deg_restrictAlong_mul_inertiaDegAlong (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w :
  Place K F') :
    (w.restrictAlong φ hφ).deg * w.inertiaDegAlong φ hφ = w.deg

theorem

sq_symm

L54 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.sq_symm

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (α β : F →ₐ[K] F') (hα : α.toRingHom.IsIntegral) (hβ : β.toRingHom.IsIntegral)
  (σ : F' ≃ₐ[K] F') (τ : F ≃ₐ[K] F) (h : ∀ x, α (τ x) = σ (β x))
include h

Lean source · statement

theorem sq_symm (x : F) : σ.symm (α x) = β (τ.symm x)

theorem

smul_restrictAlong

L58 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.smul_restrictAlong

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (α β : F →ₐ[K] F') (hα : α.toRingHom.IsIntegral) (hβ : β.toRingHom.IsIntegral)
  (σ : F' ≃ₐ[K] F') (τ : F ≃ₐ[K] F) (h : ∀ x, α (τ x) = σ (β x))
include h

Lean source · statement

theorem smul_restrictAlong (W : Place K F') :
    (σ • W).restrictAlong α hα = τ • (W.restrictAlong β hβ)

theorem

ramificationIndexAlong_smul

L67 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.ramificationIndexAlong_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (α β : F →ₐ[K] F') (hα : α.toRingHom.IsIntegral) (hβ : β.toRingHom.IsIntegral)
  (σ : F' ≃ₐ[K] F') (τ : F ≃ₐ[K] F) (h : ∀ x, α (τ x) = σ (β x))
include h

Lean source · statement

theorem ramificationIndexAlong_smul (W : Place K F') :
    (σ • W).ramificationIndexAlong α = W.ramificationIndexAlong β

theorem

inertiaDegAlong_smul

L81 ↗

AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong.FibreSolG.inertiaDegAlong_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
noncomputable section
open AlgebraicCurve
namespace FibreSolG
section Generic
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (α β : F →ₐ[K] F') (hα : α.toRingHom.IsIntegral) (hβ : β.toRingHom.IsIntegral)
  (σ : F' ≃ₐ[K] F') (τ : F ≃ₐ[K] F) (h : ∀ x, α (τ x) = σ (β x))
include h

Lean source · statement

theorem inertiaDegAlong_smul (W : Place K F') (hdeg : (W.restrictAlong β hβ).deg = 1) :
    (σ • W).inertiaDegAlong α hα = W.inertiaDegAlong β hβ

theorem

smul_restrictAlong

L96 ↗

AlgebraicCurve.Place.smul_restrictAlong

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_restrictAlong
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.smul_restrictAlong {K F F' : Type*} [Field K] [Field F] [Field
  F'] [Algebra K F] [Algebra K F'] (α β : F →ₐ[K] F') (hα : α.toRingHom.IsIntegral) (hβ :
  β.toRingHom.IsIntegral) (σ : F' ≃ₐ[K] F') (τ : F ≃ₐ[K] F) (h : ∀ x, α (τ x) = σ (β x)) (W : Place
  K F') : (σ • W).restrictAlong α hα = τ • W.restrictAlong β hβ

Module documentation

Place smul restrict Along

Declarations