Module

SemilinearAut_eq_of_forall_smul_place_eq.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_eq_of_forall_smul_place_eq

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut eq of forall smul place eq

Imports4

Imported by1

Nyll.AlgebraicCurves.Divisors.Semilinear.All

theorem

solution

L36 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_eq_of_forall_smul_place_eq.solution

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_eq_of_forall_smul_place_eq
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve

Lean source · statement

theorem solution
    (F₀ : Type) [Field F₀] [Algebra (AlgebraicClosure ℚ) F₀] [IsCurveOver (AlgebraicClosure ℚ) F₀]
    [Algebra.EssFiniteType (AlgebraicClosure ℚ) F₀]
    (W W' : SemilinearAut (AlgebraicClosure ℚ) F₀)
    (hW : ∀ a : AlgebraicClosure ℚ, SemilinearAut.baseAut W a = a)
    (hW' : ∀ a : AlgebraicClosure ℚ, SemilinearAut.baseAut W' a = a)
    (h : ∀ P : Place (AlgebraicClosure ℚ) F₀, W • P = W' • P) :
    W = W'

theorem

eq_of_forall_smul_place_eq

L92 ↗

AlgebraicCurve.SemilinearAut.eq_of_forall_smul_place_eq