NYLL
Module

SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
8 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut exists Unique base Aut eq smul algebra Map eq of constant Field Extension

Imports2
Imported by2

Declarations

def

twistHom

L40 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.G5.twistHom
Documentation

The additive map on the tensor product induced by compatible automorphisms of its two factors.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
namespace G5
section Twist
variable {K F K' : Type*} [Field K] [Field F] [Field K'] [Algebra K F] [Algebra K K']
  (g : SemilinearAut K F) (τ : K' ≃+* K')
  (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a))
Lean source · statement
def twistHom (σ : K' ≃+* K') (φ : F ≃+* F)
    (h : ∀ a : K, ∀ c : K', ∀ y : F, σ (a • c) ⊗ₜ[K] φ y = σ c ⊗ₜ[K] φ (a • y)) :
    K' ⊗[K] F →+ K' ⊗[K] F
theorem

twistHom_tmul

L49 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.G5.twistHom_tmul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
namespace G5
section Twist
variable {K F K' : Type*} [Field K] [Field F] [Field K'] [Algebra K F] [Algebra K K']
  (g : SemilinearAut K F) (τ : K' ≃+* K')
  (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a))
Lean source · statement
theorem twistHom_tmul (σ : K' ≃+* K') (φ : F ≃+* F)
    (h : ∀ a : K, ∀ c : K', ∀ y : F, σ (a • c) ⊗ₜ[K] φ y = σ c ⊗ₜ[K] φ (a • y)) (c : K') (y : F) :
    twistHom σ φ h (c ⊗ₜ y) = σ c ⊗ₜ φ y
theorem

twist_compat

L54 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.G5.twist_compat
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
namespace G5
section Twist
variable {K F K' : Type*} [Field K] [Field F] [Field K'] [Algebra K F] [Algebra K K']
  (g : SemilinearAut K F) (τ : K' ≃+* K')
  (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a))
include hτ in
Lean source · statement
theorem twist_compat : ∀ a : K, ∀ c : K', ∀ y : F,
    τ (a • c) ⊗ₜ[K] (SemilinearAut.toRingAut g) y = τ c ⊗ₜ[K] (SemilinearAut.toRingAut g) (a • y)
theorem

twist_compat_symm

L61 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.G5.twist_compat_symm
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
namespace G5
section Twist
variable {K F K' : Type*} [Field K] [Field F] [Field K'] [Algebra K F] [Algebra K K']
  (g : SemilinearAut K F) (τ : K' ≃+* K')
  (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a))
include hτ in
Lean source · statement
theorem twist_compat_symm : ∀ a : K, ∀ c : K', ∀ y : F,
    τ.symm (a • c) ⊗ₜ[K] (SemilinearAut.toRingAut g).symm y =
      τ.symm c ⊗ₜ[K] (SemilinearAut.toRingAut g).symm (a • y)
def

twist

L80 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.G5.twist
Documentation

The ring equivalence on the tensor product induced by the compatible semilinear twists.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
namespace G5
section Twist
variable {K F K' : Type*} [Field K] [Field F] [Field K'] [Algebra K F] [Algebra K K']
  (g : SemilinearAut K F) (τ : K' ≃+* K')
  (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a))
Lean source · full declaration
def twist : K' ⊗[K] F ≃+* K' ⊗[K] F where
  toFun := twistHom τ (SemilinearAut.toRingAut g) (twist_compat g τ hτ)
  invFun := twistHom τ.symm (SemilinearAut.toRingAut g).symm (twist_compat_symm g τ hτ)
  left_inv x := by
    induction x using TensorProduct.inductionOn with
    | tmul c y => simp [twistHom_tmul]
    | add x y hx hy => simp only [map_add, hx, hy]
  right_inv x := by
    induction x using TensorProduct.inductionOn with
    | tmul c y => simp [twistHom_tmul]
    | add x y hx hy => simp only [map_add, hx, hy]
  map_add' x y := map_add _ x y
  map_mul' x y := by
    induction x using TensorProduct.inductionOn with
    | tmul c z =>
      induction y using TensorProduct.inductionOn with
      | tmul c' z' => simp [twistHom_tmul, Algebra.TensorProduct.tmul_mul_tmul]
      | add y y' hy hy' => simp only [mul_add, map_add, hy, hy']
    | add x x' hx hx' => simp only [add_mul, map_add, hx, hx']
theorem

twist_tmul

L100 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.G5.twist_tmul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
namespace G5
section Twist
variable {K F K' : Type*} [Field K] [Field F] [Field K'] [Algebra K F] [Algebra K K']
  (g : SemilinearAut K F) (τ : K' ≃+* K')
  (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a))
Lean source · statement
theorem twist_tmul (c : K') (y : F) : twist g τ hτ (c ⊗ₜ y) = τ c ⊗ₜ (g • y)
theorem

solution

L109 ↗
AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension.solution
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs
namespace SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
open AlgebraicCurve
open scoped TensorProduct
open AlgebraicCurve G5 in
Lean source · statement
theorem solution
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (g : SemilinearAut K F) (τ : K' ≃+* K')
    (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a)) :
    ∃! g' : SemilinearAut K' F',
      (∀ c : K', SemilinearAut.baseAut g' c = τ c) ∧
      ∀ y : F, g' • algebraMap F F' y = algebraMap F F' (g • y)
theorem

existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension

L221 ↗
AlgebraicCurve.SemilinearAut.existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
Source context 3 commands

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

open _root_.AlgebraicCurve hiding linearIndependent_of_constantFieldExtension
open AlgebraicCurves.Divisors.Semilinear.Proofs in
open SemilinearAut_existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
  renaming solution → semilinearProof in
Lean source · statement
theorem
  AlgebraicCurve.SemilinearAut.existsUnique_baseAut_eq_smul_algebraMap_eq_of_constantFieldExtension
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (g : SemilinearAut K F) (τ : K' ≃+* K')
    (hτ : ∀ a : K, τ (algebraMap K K' a) = algebraMap K K' (SemilinearAut.baseAut g a)) :
    ∃! g' : SemilinearAut K' F',
      (∀ c : K', SemilinearAut.baseAut g' c = τ c) ∧
      ∀ y : F, g' • algebraMap F F' y = algebraMap F F' (g • y)

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