OAI/Analysis/NuclearUltrapower/ModTwo.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.residuePermutation line 17

   Source documentation

   Reduction modulo two, acting by affine permutations on its eight points.

   def residuePermutation : IntegralGroup →* Equiv.Perm Residue3 where
   …

   Mentions: OAI.NuclearUltrapower.IntegralGroup, OAI.NuclearUltrapower.Residue3

2. theorem OAI.NuclearUltrapower.residuePermutation_apply line 29
3. abbrev OAI.NuclearUltrapower.ResidueHilbert line 32
4. def OAI.NuclearUltrapower.residueUnitary line 34
5. theorem OAI.NuclearUltrapower.residueUnitary_apply line 48
6. def OAI.NuclearUltrapower.augmentation line 51
7. theorem OAI.NuclearUltrapower.mem_augmentation line 56
8. theorem OAI.NuclearUltrapower.augmentation_invariant line 59
9. def OAI.NuclearUltrapower.augmentationVector line 64
10. theorem OAI.NuclearUltrapower.augmentationVector_mem line 67
11. theorem OAI.NuclearUltrapower.augmentationVector_ne_zero line 70
12. instance OAI.NuclearUltrapower.augmentation_nontrivial line 79
13. def OAI.NuclearUltrapower.augmentationRep line 86
14. theorem OAI.NuclearUltrapower.augmentation_no_translation_invariants line 90

    Source documentation

    A translation-fixed vector in the augmentation representation is zero.

    theorem augmentation_no_translation_invariants (f : augmentationRep)
        (hf : ∀ v : IntegralVector3, augmentationRep.action (integralTranslation v) f = f) :
        f = 0 := by
    …

    Mentions: OAI.NuclearUltrapower.augmentationRep, OAI.NuclearUltrapower.IntegralVector3, OAI.NuclearUltrapower.integralTranslation

15. theorem OAI.NuclearUltrapower.augmentation_pull_translation line 115

    Source documentation

    All positive dilation pullbacks kill the translation subgroup.

    theorem augmentation_pull_translation (j : ℕ) (hj : 0 < j) (v : IntegralVector3) :
        augmentationRep.action ((integralTheta ^ j) (integralTranslation v)) = 1 := by
    …

    Mentions: OAI.NuclearUltrapower.IntegralVector3, OAI.NuclearUltrapower.integralTheta, OAI.NuclearUltrapower.integralTranslation

16. theorem OAI.NuclearUltrapower.exists_aperiodic_integral_rep line 131

    Source documentation

    The required irreducible mod-two representation is a constituent of the augmentation representation, hence has no translation-fixed vectors.

    theorem exists_aperiodic_integral_rep :
        ∃ π : FiniteUnitaryRep.{0,0} IntegralGroup, π.Irreducible ∧
          (∀ j : ℕ, 0 < j → ¬ π.Equivalent (π.pull (integralTheta ^ j))) := by
    …

    Mentions: OAI.NuclearUltrapower.IntegralGroup, OAI.NuclearUltrapower.integralTheta