EtaleFundamentalGroups.Kummer.exists_cyclicQuotientGrading_range_eq_gradeZero
For a finite-index additive subgroup H ≤ L, choose cyclic coordinates on L ⧸ H. In those coordinates, the image of R[H] → R[L] remains exactly the degree-zero subalgebra.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
universe u vLean source · statement
theorem exists_cyclicQuotientGrading_range_eq_gradeZero
{R : Type u} {L : Type v} [CommSemiring R] [AddCommGroup L]
(H : AddSubgroup L) [Finite (L ⧸ H)] :
∃ (ι : Type) (_ : Fintype ι) (n : ι → ℕ),
(∀ i, 1 < n i) ∧
∃ e : (L ⧸ H) ≃+ (∀ i, ZMod (n i)),
(AddMonoidAlgebra.mapDomainAlgHom R R H.subtype).range =
SetLike.GradeZero.subalgebra
(AddMonoidAlgebra.gradeBy R
(e.toAddMonoidHom.comp (QuotientAddGroup.mk' H)))