OAI/Algebra/BogomolovPop/Injectivity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BogomolovPop.purely_inseparable_pow_mem_mono line 14
2. theorem OAI.BogomolovPop.uniform_frobenius_clearing line 22
3. lemma OAI.BogomolovPop.purely_inseparable_ringHom_ext line 64
4. def OAI.BogomolovPop.frobeniusPerfectIsom line 74
5. lemma OAI.BogomolovPop.frobeniusPerfectIsom_apply line 93
6. lemma OAI.BogomolovPop.frobeniusPerfectIsom_eqvGen line 99
7. theorem OAI.BogomolovPop.frobenius_orbit_of_iterates line 129
8. theorem OAI.BogomolovPop.perfect_scalar_iterates line 143
9. theorem OAI.BogomolovPop.pullback_scalar_frobenius line 213
10. theorem OAI.BogomolovPop.main_canonical_injective line 276
11. theorem OAI.BogomolovPop.main_graph_injective line 305

    Source documentation

    Injectivity of the canonical Galois graph on its prescribed orbit sets.

    Distinct definitions of this name: ComparatorChallenges/BogomolovPopInjectivity.lean:117 (same statement text; different proof or body). Qualify references as OAI.BogomolovPop.main_graph_injective@path.

    theorem main_graph_injective (ell : ℕ) [Fact ell.Prime]
        (k K l L : Type*) [Field k] [Field K] [Field l] [Field L]
        [IsAlgClosed k] [IsAlgClosed l] [Algebra k K] [Algebra l L]
        [Algebra.EssFiniteType k K] [Algebra.EssFiniteType l L]
        (hk : (ell : k) ≠ 0) (hl : (ell : l) ≠ 0)
        (hK : 2 ≤ Algebra.trdeg k K) (hL : 2 ≤ Algebra.trdeg l L) :
        ∀ (a a' : IsomF k K l L) (b : IsomCUnits ell K L),
          PhiGraph a b → PhiGraph a' b → a = a'  := by
    …

    Mentions: OAI.BogomolovPop.IsomF, OAI.BogomolovPop.IsomCUnits, OAI.BogomolovPop.PhiGraph