Infinite.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

13 declarations, 0 contain sorry, 0 declared as axioms

Equivalence between continuous `G`-finite sets and `k`-etale algebras

Given a group G, fields L/K with L separably closed, such that G acts on L by K-algebra homomorphisms. We have a contravariant adjunction G-set ↔ K-algebra X → Hom_G(X, L), Hom_K(A, L) ← A with unit and counits: AlgHom.evalMulActionHom: A →ₐ[K] ((A →ₐ[K] L) →[G] L) MulActionHom.evalAlgHom: X →[G] ((X →[G] L) →ₐ[K] L)

Suppose L/K is galois with galois group G:

If X is finite discrete with continuous G action, then X →[G] L is finite etale.
InfiniteGalois.evalAlgHom_bijective: If X is finite discrete with continuous G action, then MulActionHom.evalAlgHom is bijective.
If A/K is finite dimensional then A →ₐ[K] L is finite discrete with continuous G action.
InfiniteGalois.evalMulActionHom_bijective: If A/K is etale, and L contains all residue fields of A (in particular when L is separably closed), then AlgHom.evalMulActionHom is bijective.

Taking L = Kˢᵉᵖ, the adjunction restricts to a (contravariant) equivalence between finite discrete Gₖ-sets and finite etale k-algebras.

Material destined for Mathlib.

Imports (14)

Imported by 3 files

def MulAction.etaleSubalgebraEquiv Documented declaration: etaleSubalgebraEquiv line 70 source
Source documentation
Given a representative for each orbit of X under G := Gal(L/K), and for each x : X a choice of σ that sends x to the representative, we obtain a K-algebra isomorphism between G-equivariant homs from X and the product of Stab(x)-fixed points over each orbit representative x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, MulAction, AlgEquiv, MulAction.orbitRel, Eq, HSMul.hSMul, MulActionHom, id, Set.range, Subtype, Membership.mem, IntermediateField, IntermediateField.fixedField, MulAction.stabilizer, Set
Proof uses: Equiv, MulAction.fixedPoints, Subgroup, MulAction.homEquivProdFixedPoints, AlgEquiv.mk
104 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def MulAction.etaleSubalgebraEquiv
    (σ : X → L ≃ₐ[K] L) (hσ : ∀ a b, orbitRel (L ≃ₐ[K] L) X a b → σ a • a = σ b • b) :
    (X →[L ≃ₐ[K] L] L) ≃ₐ[K]
      Π i : Set.range (fun i ↦ σ i • i), fixedField (stabilizer (L ≃ₐ[K] L) i.1) where
…
```
def InfiniteGalois.quotientEquivFixedFieldEmb line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsGalois, ClosedSubgroup, AlgEquiv, Equiv, HasQuotient.Quotient, Subgroup, AlgHom, Subtype, Membership.mem, IntermediateField, IntermediateField.fixedField
Proof uses: Equiv.mk, Quotient.lift, QuotientGroup.leftRel, AlgHom.comp, IntermediateField.val, AlgEquiv.ofBijective, AlgHom.liftNormal
56 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma InfiniteGalois.evalAlgHom_bijective line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, MulAction, AlgEquiv, IsGalois, Finite, ContinuousSMulDiscrete, Function.Bijective, AlgHom, MulActionHom, id, MulActionHom.evalAlgHom
Proof uses: Quotient, MulAction.orbitRel, Eq, Quotient.mk, HSMul.hSMul, Eq.trans, Quotient.mk'', congr_arg, Iff.mpr, Quotient.eq'', Eq.symm, Equiv, Equiv.trans, Set.range, Subtype, Membership.mem, IntermediateField, IntermediateField.fixedField, MulAction.stabilizer, Set and 33 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
instance (instance at line 125) line 125 source
instance (instance at line 136) line 136 source
instance (instance at line 150) line 150 source
instance (instance at line 156) line 156 source
lemma InfiniteGalois.evalMulActionHom_bijective line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, Algebra.Etale, IsGalois, Ideal, Ideal.IsMaximal, Nonempty, AlgHom, HasQuotient.Quotient, Function.Bijective, MulActionHom, AlgEquiv, id, AlgHom.evalMulActionHom
Proof uses: Nonempty.some, IsReduced, Algebra.FormallyUnramified.isReduced_of_field, Module.Finite, Algebra.FormallyUnramified.finite_of_free, IsArtinianRing, isArtinian_of_tower, inferInstance, IsArtinian, Membership.mem, IntermediateField, AlgHom.fieldRange, Ideal.Quotient.field, AlgHom.comp, Ideal.Quotient.mkₐ, Eq.mpr, IntermediateField.fixedField, IntermediateField.fixingSubgroup, Eq, congrArg and 59 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma InfiniteGalois.evalMulActionHom_bijective_of_isSepClosed line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, CommRing, Algebra.Etale, IsGalois, IsSepClosed, Function.Bijective, MulActionHom, AlgEquiv, id, AlgHom, AlgHom.evalMulActionHom
Proof uses: InfiniteGalois.evalMulActionHom_bijective, Ideal, Ideal.IsMaximal, Nonempty.intro, HasQuotient.Quotient, IsSepClosed.lift, Ideal.Quotient.field
54 instances, coercions and auxiliary constants left out.
instance finiteIndex_fixingSubgroup line 220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IntermediateField, FiniteDimensional, Subtype, Membership.mem, Subgroup.FiniteIndex, AlgEquiv, IntermediateField.fixingSubgroup
Proof uses: HasQuotient.Quotient, Subgroup, AlgHom, Quotient.lift, QuotientGroup.leftRel, AlgHom.comp, IntermediateField.val, HasEquiv.Equiv, MulOpposite, Subgroup.op, Eq, HSMul.hSMul, AlgHom.ext, DFunLike.congr_arg, Equiv, MulEquiv.toEquiv, RingEquiv.toMulEquiv, AlgEquiv.toRingEquiv, MulOpposite.unop, RingHom and 24 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
instance (instance at line 233) line 233 source
instance (instance at line 299) line 299 source
instance (instance at line 312) line 312 source

FLT/Mathlib/FieldTheory/Galois/Infinite.lean

Equivalence between continuous G-finite sets and k-etale algebras

`FLT/Mathlib/FieldTheory/Galois/Infinite.lean`

Equivalence between continuous `G`-finite sets and `k`-etale algebras