NYLL
Module

FinitelyGeneratedPositiveChar.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.FinitelyGeneratedPositiveChar
2 declarations indexed from sourceView source ↗

Module documentation

Positive-characteristic finitely generated fields are ab-faithful

Finite Galois automorphisms move discrete valuations, so local Artin--Schreier characters detect the action on abelianization modulo the characteristic.

Imports3
Imported by2

Declarations

theorem

finitelyGenerated_posChar_isSigmaAbFaithful

L25 ↗
Yamaguchi26AbfaithfulGalois.finitelyGenerated_posChar_isSigmaAbFaithful
Documentation

An infinite finitely generated field of characteristic p is {p}-ab-faithful, without any perfection hypothesis.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem finitelyGenerated_posChar_isSigmaAbFaithful
    (K : Type u) [Field K] [Infinite K] (p : ℕ) [Fact p.Prime] [CharP K p]
    (hfg : Field.FG K) : IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K)
theorem

finitelyGenerated_posChar_isAbFaithful

L34 ↗
Yamaguchi26AbfaithfulGalois.finitelyGenerated_posChar_isAbFaithful
Documentation

The positive-characteristic ab-faithfulness assertion needed in Example 5.9(2), proved through discrete valuations and weak approximation.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem finitelyGenerated_posChar_isAbFaithful
    (K : Type u) [Field K] [Infinite K] (hfg : Field.FG K)
    (hchar : ringChar K ≠ 0) : IsAbFaithful Gal(AlgebraicClosure K/K)

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