embeddingsEquivPrimitiveRoots — Mathlib

English

Applying the equivalence to a morphism φ' yields the image φ'(ζ).

Русский

Применение эквивалентности к морфизму φ' даёт образ φ'(ζ).

LaTeX

$$$(h\zeta.embeddingsEquivPrimitiveRoots C hirr \phi' : C) = φ'\zeta$$$

Lean4

/-- The equivalence between `L →ₐ[K] C` and `primitiveRoots n C` given by a primitive root `ζ`. -/
noncomputable def embeddingsEquivPrimitiveRoots (C : Type*) [CommRing C] [IsDomain C] [Algebra K C]
    (hirr : Irreducible (cyclotomic n K)) : (L →ₐ[K] C) ≃ primitiveRoots n C :=
  (hζ.powerBasis K).liftEquiv.trans
    { toFun := fun x => by
        haveI := IsCyclotomicExtension.neZero' n K L
        haveI hn := NeZero.of_faithfulSMul K C n
        refine ⟨x.1, ?_⟩
        cases x
        rwa [mem_primitiveRoots (NeZero.pos _), ← isRoot_cyclotomic_iff, IsRoot.def, ←
          map_cyclotomic _ (algebraMap K C), hζ.minpoly_eq_cyclotomic_of_irreducible hirr, ← eval₂_eq_eval_map, ←
          aeval_def]
      invFun := fun x => by
        haveI := IsCyclotomicExtension.neZero' n K L
        haveI hn := NeZero.of_faithfulSMul K C n
        refine ⟨x.1, ?_⟩
        cases x
        rwa [aeval_def, eval₂_eq_eval_map, hζ.powerBasis_gen K, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr,
          map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff, ← mem_primitiveRoots (NeZero.pos _)] }
      -- Porting note: renamed argument `φ`: "expected '_' or identifier"

Похожие утверждения