Module

Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul

3 declarations indexed from sourceView source ↗

Module documentation

Divisor pullback Along alg Equiv eq of Alg Aut smul

Imports2

Imported by2

theorem

restrictAlong_algEquiv

L31 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul.AutPull.restrictAlong_algEquiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul
open AlgebraicCurve
open scoped Pointwise
namespace AutPull
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem restrictAlong_algEquiv (σ : F ≃ₐ[K] F) (hσ : (σ : F →ₐ[K] F).toRingHom.IsIntegral)
    (w : Place K F) :
    w.restrictAlong (σ : F →ₐ[K] F) hσ = (SemilinearAut.ofAlgAut σ)⁻¹ • w

theorem

ramificationIndexAlong_algEquiv

L45 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul.AutPull.ramificationIndexAlong_algEquiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul
open AlgebraicCurve
open scoped Pointwise
namespace AutPull
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ramificationIndexAlong_algEquiv [HasPrincipalDivisors K F] (σ : F ≃ₐ[K] F)
    (hσ : (σ : F →ₐ[K] F).toRingHom.IsIntegral) (w : Place K F) :
    Place.ramificationIndexAlong (σ : F →ₐ[K] F) w = 1

theorem

pullbackAlong_algEquiv_eq_ofAlgAut_smul

L64 ↗

AlgebraicCurve.Divisor.pullbackAlong_algEquiv_eq_ofAlgAut_smul

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_algEquiv_eq_ofAlgAut_smul
open AlgebraicCurve
open scoped Pointwise
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.pullbackAlong_algEquiv_eq_ofAlgAut_smul {K F : Type*} [Field
  K] [Field F] [Algebra K F] [AlgebraicCurve.HasPrincipalDivisors K F]
    (σ : F ≃ₐ[K] F) (hσ : (σ : F →ₐ[K] F).toRingHom.IsIntegral) (D : AlgebraicCurve.Divisor K F) :
    AlgebraicCurve.Divisor.pullbackAlong (σ : F →ₐ[K] F) hσ D =
      AlgebraicCurve.SemilinearAut.ofAlgAut σ • D

Module documentation

Divisor pullback Along alg Equiv eq of Alg Aut smul

Declarations

restrictAlong_algEquiv

ramificationIndexAlong_algEquiv

pullbackAlong_algEquiv_eq_ofAlgAut_smul