NYLL
Module

AlgEquiv_eq_one_of_forall_smul_place_eq.lean

Nyll.AlgebraicCurves.Places.AlgEquiv_eq_one_of_forall_smul_place_eq
5 declarations indexed from sourceView source ↗

Module documentation

Alg Equiv eq one of forall smul place eq

Imports5
Imported by3

Declarations

theorem

ord_map_eq

L43 ↗
AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_of_forall_smul_place_eq.QForm1.ord_map_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_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 IntermediateField
namespace QForm1
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_map_eq (σ : F ≃ₐ[K] F) (h : ∀ v : Place K F, σ • v = v) (v : Place K F) (f : F) :
    v.ord (σ f) = v.ord f
theorem

exists_map_eq_algebraMap_mul

L50 ↗
AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_of_forall_smul_place_eq.QForm1.exists_map_eq_algebraMap_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_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 IntermediateField
namespace QForm1
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K]
Lean source · statement
theorem exists_map_eq_algebraMap_mul (j : F) (hj : Transcendental K j) [FiniteDimensional K⟮j⟯ F]
    (σ : F ≃ₐ[K] F) (h : ∀ v : Place K F, σ • v = v) {f : F} (hf : f ≠ 0) :
    ∃ c : K, σ f = algebraMap K F c * f
theorem

algEquiv_eq_one_of_forall_smul_place_eq

L60 ↗
AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_of_forall_smul_place_eq.QForm1.algEquiv_eq_one_of_forall_smul_place_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_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 IntermediateField
namespace QForm1
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K]
Lean source · statement
theorem algEquiv_eq_one_of_forall_smul_place_eq (j : F) (hj : Transcendental K j)
    [FiniteDimensional K⟮j⟯ F]
    (σ : F ≃ₐ[K] F) (h : ∀ v : Place K F, σ • v = v) : σ = 1
theorem

algebra_transcendental_of_nontrivial_kaehler

L99 ↗
AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_of_forall_smul_place_eq.QForm1.algebra_transcendental_of_nontrivial_kaehler
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_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 IntermediateField
namespace QForm1
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K]
Lean source · statement
theorem algebra_transcendental_of_nontrivial_kaehler [Nontrivial (Ω[F⁄K])] :
    Algebra.Transcendental K F
theorem

eq_one_of_forall_smul_place_eq

L112 ↗
AlgebraicCurve.AlgEquiv.eq_one_of_forall_smul_place_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.AlgEquiv_eq_one_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 IntermediateField
open QForm1 in
Lean source · statement
theorem _root_.AlgebraicCurve.AlgEquiv.eq_one_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]
    (σ : F ≃ₐ[K] F) (h : ∀ v : Place K F, σ • v = v) : σ = 1

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