NYLL
Module

SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq
4 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut eq of base Aut eq of forall smul place eq

Imports5
Imported by1

Declarations

def

algEquivOfBaseAutEqOne

L48 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq.QForm1b.algEquivOfBaseAutEqOne
Documentation

The algebra automorphism underlying a semilinear automorphism whose base automorphism is the identity.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_eq_of_baseAut_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
universe u v
open AlgebraicCurve
namespace QForm1b
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
def algEquivOfBaseAutEqOne (k : SemilinearAut K F) (hk : SemilinearAut.baseAut k = 1)
  :
    F ≃ₐ[K] F
theorem

ofAlgAut_algEquivOfBaseAutEqOne

L55 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq.QForm1b.ofAlgAut_algEquivOfBaseAutEqOne
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_eq_of_baseAut_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
universe u v
open AlgebraicCurve
namespace QForm1b
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ofAlgAut_algEquivOfBaseAutEqOne (k : SemilinearAut K F) (hk : SemilinearAut.baseAut k = 1) :
    SemilinearAut.ofAlgAut (algEquivOfBaseAutEqOne k hk) = k
theorem

solution

L65 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq.solution
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_eq_of_baseAut_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
universe u v
open AlgebraicCurve
open QForm1b in
Lean source · statement
theorem solution
    {K : Type u} {F : Type v} [Field K] [IsAlgClosed K] [Field F] [Algebra K F] [IsCurveOver K F]
    [Algebra.EssFiniteType K F]
    (g g' : SemilinearAut K F) (hb : SemilinearAut.baseAut g = SemilinearAut.baseAut g')
    (h : ∀ v : Place K F, g • v = g' • v) : g = g'
theorem

eq_of_baseAut_eq_of_forall_smul_place_eq

L105 ↗
AlgebraicCurve.SemilinearAut.eq_of_baseAut_eq_of_forall_smul_place_eq
Source context 6 commands

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

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
universe u v
open AlgebraicCurves.Divisors.Semilinear.Proofs in
open SemilinearAut_eq_of_baseAut_eq_of_forall_smul_place_eq
  renaming solution → semilinearProof in
Lean source · statement
theorem AlgebraicCurve.SemilinearAut.eq_of_baseAut_eq_of_forall_smul_place_eq
    {K : Type u} {F : Type v} [Field K] [IsAlgClosed K] [Field F] [Algebra K F] [IsCurveOver K F]
    [Algebra.EssFiniteType K F]
    (g g' : SemilinearAut K F) (hb : SemilinearAut.baseAut g = SemilinearAut.baseAut g')
    (h : ∀ v : Place K F, g • v = g' • v) : g = g'

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