The universe-zero group boundary imposed by integral representations.
Lean source · statement
abbrev IntegralRepGroupTypeIntegralRepUniverse.lean
Nyll.GaloisCohomology.Cyclic.IntegralRepUniverse
1 declaration indexed from sourceView source ↗
Module documentation
Universe boundary for integral representations
Mathlib's Rep ℤ G currently requires the coefficient ring and acting group to inhabit the same universe. Since ℤ : Type 0, every representation-bearing part of local class field theory uses this single named boundary. Keeping the restriction here makes a future universe-polymorphic migration searchable and prevents individual subtrees from inventing private aliases.
Imports0
None.
Imported by18
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.Fields
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.Norm
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.NormConjugation
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.ClassFieldCandidate
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.CanonicalUnramifiedNormQuotient
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FiniteNormQuotient
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.NormSubgroup
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.RelativeNormDoubleCoset
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FieldRepresentation
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Main
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.MaximalUnramifiedReciprocity
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.NormTopology
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.NormTopologyCharacterization
- Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Reduction
- Nyll.GaloisCohomology.Cyclic.All
- Nyll.GaloisCohomology.Kummer.Abstract.KummerCyclicOperator
- Nyll.GaloisCohomology.Kummer.Abstract.KummerDelta
- Nyll.GaloisCohomology.Kummer.Abstract.KummerFixedField