FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Functoriality of the absolute Galois group

For a field extension K → L, the induced map between absolute Galois groups Γ L → Γ K is Field.absoluteGaloisGroup.map in Mathlib; here we record how it interacts with the chosen embedding of the algebraic closures, together with finite-index results for fixing subgroups.

Imports (8)
Imported by 2 files
  1. lemma Field.absoluteGaloisGroup.lift_map line 53 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, RingHom, Field.absoluteGaloisGroup, AlgebraicClosure, Eq, AlgebraicClosure.map, ContinuousMonoidHom, Field.absoluteGaloisGroup.map

    Proof uses: Algebra, RingHom.toAlgebra, AlgEquiv.restrictNormal_commutes, MonoidHom, AlgEquiv, AlgEquiv.restrictScalarsHom, AlgHom.toRingHom, IsAlgClosed.lift

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  2. lemma isIntegral_of_spectralNorm_le_one line 72 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: LinearOrderedCommGroupWithZero, Field, Valued, Valuation.RankOne, Valued.v, Algebra, Algebra.IsAlgebraic, LE.le, Real, spectralNorm, Valued.toNormedField, OfNat.ofNat, IsIntegral, Subtype, Membership.mem, Subring, Valuation.integer

    Proof uses: Polynomial, Subsemiring, Polynomial.lifts, Subring.subtype, minpoly, Iff.mpr, Nat, Set, Set.range, RingHom, Finsupp, Polynomial.coeff, Polynomial.lifts_iff_coeff_lifts, spectralValueTerms, Iff.mp, iSup, ciSup_le_iff, spectralValueTerms_bddAbove, dite, LT.lt and 64 more

    197 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

    Open to load the checked before-and-after goal states.

  3. lemma spectralNorm_inv line 93 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NontriviallyNormedField, Field, Algebra, IsUltrametricDist, CompleteSpace, Algebra.IsAlgebraic, Eq, Real, spectralNorm, Inv.inv

    Proof uses: dite, OfNat.ofNat, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, congrArg, inv_zero, spectralNorm_zero, eq_self, Not, eq_inv_of_mul_eq_one_right, Eq.mpr, HMul.hMul, AlgebraNorm, spectralAlgNorm, id, Eq.symm, spectralAlgNorm_def and 4 more

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  4. instance (instance at line 103) line 103 source
  5. instance valuationRing_integralClosure line 105 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Algebra, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Algebra.IsAlgebraic, ValuationRing, IntegralClosure, Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

    Proof uses: ValuationSubring.mk, Subalgebra.toSubring, integralClosure, LE.le, Real, spectralNorm, OfNat.ofNat, Or, Set, Subsemigroup.carrier, Submonoid.toSubsemigroup, Subsemiring.toSubmonoid, Subring.toSubsemiring, Inv.inv, le_total, Or.inl, isIntegral_of_spectralNorm_le_one, WithZero, Multiplicative, Int and 6 more

    87 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  6. def localInertiaGroup line 119 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subgroup, Field.absoluteGaloisGroup, IsDedekindDomain.HeightOneSpectrum.adicCompletion, AlgebraicClosure

    Proof uses: AddSubgroup.inertia, IntegralClosure, Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Submodule.toAddSubgroup, IsLocalRing.maximalIdeal

    48 instances, coercions and auxiliary constants left out.

  7. def localTameAbelianInertiaGroup line 130 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subgroup, Field.absoluteGaloisGroup, IsDedekindDomain.HeightOneSpectrum.adicCompletion, AlgebraicClosure

    Proof uses: Subgroup.mk, Submonoid.mk, Subsemigroup.mk, Set.ofPred, Membership.mem, IntermediateField, IntermediateField.fixedField, localInertiaGroup, HPow.hPow, Nat, HSub.hSub, Nat.card, IsLocalRing.ResidueField, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, OfNat.ofNat, Eq, Set

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  8. instance (instance at line 138) line 138 source
  9. instance (instance at line 141) line 141 source
  10. instance (instance at line 146) line 146 source
  11. instance finite_adicCompletionIntegers_quotient line 148 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Ideal, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Ideal.IsPrime, NeZero, Finite, HasQuotient.Quotient

    Proof uses: IsLocalRing.maximalIdeal, Eq.symm, ExistsUnique.unique, And, Ne, Bot.bot, And.right, IsPrincipalIdealRing, ExistsUnique, Iff.mp, IsDiscreteValuationRing, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime, inferInstance, And.intro, NeZero.ne, IsDiscreteValuationRing.not_a_field

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  12. instance neZero_maximalIdeal_integralClosure line 155 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, NeZero, Ideal, IntegralClosure, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, AlgebraicClosure, IsLocalRing.maximalIdeal

    Proof uses: Ne, Top.top, Eq, IsDiscreteValuationRing.not_isField, Eq.rec, IsField, MulEquiv.isField, Semifield.toIsField, RingEquiv.toMulEquiv, Subring, Subring.topEquiv, Eq.symm, NeZero.mk, LT.lt.ne', Bot.bot, Ideal.bot_lt_of_maximal, not_isField_integralClosure

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  13. def Field.AbsoluteGaloisGroup.adicArithFrob line 165 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Field.absoluteGaloisGroup, IsDedekindDomain.HeightOneSpectrum.adicCompletion

    Proof uses: arithFrobAt', Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IntegralClosure, AlgebraicClosure, IsLocalRing.maximalIdeal

    40 instances, coercions and auxiliary constants left out.

  14. lemma Field.AbsoluteGaloisGroup.isArithFrobAt_adicArithFrob line 170 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsArithFrobAt, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IntegralClosure, AlgebraicClosure, Field.absoluteGaloisGroup, Field.AbsoluteGaloisGroup.adicArithFrob, IsLocalRing.maximalIdeal

    Proof uses: IsArithFrobAt.arithFrobAt', Ideal.under

    110 instances, coercions and auxiliary constants left out.