Module

SimilitudeEigenvectors.lean

Nyll.AnabelianGeometry.GaloisRepresentations.SimilitudeEigenvectors

2 declarations indexed from sourceView source ↗

Module documentation

Excluding the multiplier as an eigenvalue of a similitude

For a nondegenerate bilinear pairing with multiplier c, the absence of fixed vectors in finite dimension excludes eigenvectors of eigenvalue c. The proof uses the surjectivity of F - 1 and does not require an eigenvalue splitting field or a diagonalization assumption.

In arithmetic applications the pairing is the Weil pairing and F is a good-reduction Frobenius. This file proves only the linear algebra; good reduction and the absence of fixed vectors must be proved separately.

Imports2

Mathlib.LinearAlgebra.BilinearForm.Basic
Mathlib.LinearAlgebra.FiniteDimensional.Basic

Imported by1

Nyll.AnabelianGeometry.GaloisRepresentations.All

theorem

eq_zero_of_similitude_eigenvector

L31 ↗

AnabelianGeometry.GaloisRepresentations.eq_zero_of_similitude_eigenvector

Documentation

If F - 1 is surjective, a nondegenerate similitude has no eigenvector for its nonzero multiplier.

Source context 3 commands

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

namespace AnabelianGeometry.GaloisRepresentations
universe u v
variable {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V]

Lean source · statement

theorem eq_zero_of_similitude_eigenvector
    (B : LinearMap.BilinForm K V) (hB : Function.Injective B)
    (F : V →ₗ[K] V) (c : K) (hc : c ≠ 0)
    (hpair : ∀ x y : V, B (F x) (F y) = c * B x y)
    (hsurj : Function.Surjective (F - (LinearMap.id : V →ₗ[K] V)))
    {v : V} (hv : F v = c • v) : v = 0

theorem

eq_zero_of_similitude_eigenvector_of_no_fixed_vectors

L50 ↗

AnabelianGeometry.GaloisRepresentations.eq_zero_of_similitude_eigenvector_of_no_fixed_vectors