OAI/Analysis/NuclearUltrapower/DyadicGroup.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NuclearUltrapower.dyadicTwo_val line 14
2. abbrev OAI.NuclearUltrapower.IntegralVector3 line 19
3. def OAI.NuclearUltrapower.integralAction line 21
4. abbrev OAI.NuclearUltrapower.IntegralGroup line 26
5. def OAI.NuclearUltrapower.integralTranslation line 28
6. def OAI.NuclearUltrapower.integralTheta line 31
7. theorem OAI.NuclearUltrapower.integralTheta_left line 43
8. theorem OAI.NuclearUltrapower.integralTheta_right line 46
9. theorem OAI.NuclearUltrapower.integralTheta_injective line 49
10. theorem OAI.NuclearUltrapower.integralTheta_translation line 59
11. theorem OAI.NuclearUltrapower.integralTheta_pow_translation line 62
12. def OAI.NuclearUltrapower.integralInclusion line 72

    Source documentation

    The inclusion is literally integer coordinate inclusion into Z[1/2].

    def integralInclusion : IntegralGroup →* G where
    …

    Mentions: OAI.NuclearUltrapower.IntegralGroup, OAI.NuclearUltrapower.G

13. def OAI.NuclearUltrapower.stableLetter line 86

    Source documentation

    The stable letter t=(0,I,1).

    def stableLetter : G :=
    …

    Mentions: OAI.NuclearUltrapower.G

14. theorem OAI.NuclearUltrapower.stableLetter_conjugation line 90

    Source documentation

    The source group law implements exactly multiplication of translations by two.

    theorem stableLetter_conjugation (g : IntegralGroup) :
        stableLetter * integralInclusion g * stableLetter⁻¹ = integralInclusion (integralTheta g) := by
    …

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

15. theorem OAI.NuclearUltrapower.integralInclusion_injective line 106

    Source documentation

    The integral copy is genuinely a subgroup, not merely a homomorphic image.

    theorem integralInclusion_injective : Function.Injective integralInclusion := by
    …

    Mentions: OAI.NuclearUltrapower.integralInclusion

16. abbrev OAI.NuclearUltrapower.Residue3 line 118
17. def OAI.NuclearUltrapower.residue line 120
18. def OAI.NuclearUltrapower.residueMatrix line 122
19. theorem OAI.NuclearUltrapower.residue_mul line 125
20. theorem OAI.NuclearUltrapower.residue_one line 131
21. theorem OAI.NuclearUltrapower.residue_theta line 133
22. theorem OAI.NuclearUltrapower.mem_theta_range_iff line 139
23. theorem OAI.NuclearUltrapower.leftRel_theta_iff line 156
24. def OAI.NuclearUltrapower.thetaCosetEquiv line 170

    Source documentation

    The eight left cosets are precisely the three translation residues.

    def thetaCosetEquiv : (IntegralGroup ⧸ integralTheta.range) ≃ Residue3 where
    …

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

25. theorem OAI.NuclearUltrapower.integralTheta_index line 183
26. instance OAI.NuclearUltrapower.(instance at line 187) line 187