NYLL
Module

Place_exists_algEquiv_smul_eq_of_restrict_eq.lean

Nyll.AlgebraicCurves.Places.Place_exists_algEquiv_smul_eq_of_restrict_eq
3 declarations indexed from sourceView source ↗

Module documentation

Place exists alg Equiv smul eq of restrict eq

Imports6
Imported by9

Declarations

theorem

restrict_ofAlgAut_restrictScalars_smul

L46 ↗
AlgebraicCurves.Places.Proofs.Place_exists_algEquiv_smul_eq_of_restrict_eq.AlgebraicCurve.Place.restrict_ofAlgAut_restrictScalars_smul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algEquiv_smul_eq_of_restrict_eq
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F' M : Type*} [Field K] [Field F'] [Field M] [Algebra K F'] [Algebra K M]
  [Algebra F' M] [IsScalarTower K F' M]
section Restrict
variable [Algebra.IsIntegral F' M]
Lean source · statement
theorem restrict_ofAlgAut_restrictScalars_smul (σ : M ≃ₐ[F'] M) (W : Place K M) :
    (SemilinearAut.ofAlgAut (σ.restrictScalars K) • W).restrict F' = W.restrict F'
theorem

ord_smul_eq

L59 ↗
AlgebraicCurves.Places.Proofs.Place_exists_algEquiv_smul_eq_of_restrict_eq.AlgebraicCurve.Place.ord_smul_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algEquiv_smul_eq_of_restrict_eq
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F' M : Type*} [Field K] [Field F'] [Field M] [Algebra K F'] [Algebra K M]
  [Algebra F' M] [IsScalarTower K F' M]
section Restrict
variable [Algebra.IsIntegral F' M]
Lean source · statement
theorem ord_smul_eq (g : SemilinearAut K M) (W : Place K M) (y : M) :
    (g • W).ord y = W.ord (g⁻¹ • y)
theorem

exists_algEquiv_smul_eq_of_restrict_eq

L70 ↗
AlgebraicCurve.Place.exists_algEquiv_smul_eq_of_restrict_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_algEquiv_smul_eq_of_restrict_eq
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped Pointwise
open _root_.AlgebraicCurve.Place AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_algEquiv_smul_eq_of_restrict_eq {K F' M : Type*} [Field
  K] [Field F'] [Field M]
    [Algebra K F'] [Algebra K M] [Algebra F' M] [IsScalarTower K F' M]
    [FiniteDimensional F' M] [IsGalois F' M] (W W' : Place K M)
    (h : W'.restrict F' = W.restrict F') :
    ∃ σ : M ≃ₐ[F'] M, SemilinearAut.ofAlgAut (σ.restrictScalars K) • W = W'

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