genericPolyMapSurjOnOfInjOn — Mathlib

English

There is an equivalence expressing the realizability of a First-Order formula corresponding to a generic polynomial map surjectivity-on-injections-on-of-indices; i.e., a semantic condition equivalent to a surjectivity statement for a constructed polynomial map.

Русский

Существуют эквивалентности между реализацией формулы первого порядка, соответствующей свойству сюръективности для заданной отображения полиномов и инъекций на индексах.

LaTeX

$$$ (K \\models genericPolyMapSurjOnOfInjOn \\varphi \\text{ mons}) \\iff \\text{(surjectivity condition for the induced } f) $$$

Lean4

/-- The collection of first-order formulas corresponding to the Ax-Grothendieck theorem. -/
noncomputable def genericPolyMapSurjOnOfInjOn [Finite ι] (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
    Language.ring.Sentence :=
  let l1 : ι → Language.ring.Formula ((Σ i : ι, mons i) ⊕ (Fin 2 × ι)) := fun i =>
    (termOfFreeCommRing (genericPolyMap mons i)).relabel (Sum.inl ∘ Sum.map id (fun i => (0, i))) ='
      (termOfFreeCommRing (genericPolyMap mons i)).relabel
        (Sum.inl ∘ Sum.map id (fun i => (1, i)))
          -- p(x) = p(y) as a formula

  let f1 : Language.ring.Formula ((Σ i : ι, mons i) ⊕ (Fin 2 × ι)) := iInf l1
  let l2 : ι → Language.ring.Formula ((Σ i : ι, mons i) ⊕ (Fin 2 × ι)) := fun i =>
    .var (Sum.inl (Sum.inr (0, i))) ='
      .var
        (Sum.inl (Sum.inr (1, i)))
          -- x = y as a formula

  let f2 : Language.ring.Formula ((Σ i : ι, mons i) ⊕ (Fin 2 × ι)) := iInf l2
  let injOn : Language.ring.Formula (α ⊕ Σ i : ι, mons i) :=
    Formula.iAlls (Fin 2 × ι)
      (φ.relabel (Sum.map Sum.inl (fun i => (0, i))) ⟹
        φ.relabel (Sum.map Sum.inl (fun i => (1, i))) ⟹
          (f1.imp f2).relabel (fun x => (Equiv.sumAssoc _ _ _).symm (Sum.inr x)))
  let l3 : ι → Language.ring.Formula ((Σ i : ι, mons i) ⊕ (Fin 2 × ι)) := fun i =>
    (termOfFreeCommRing (genericPolyMap mons i)).relabel (Sum.inl ∘ Sum.map id (fun i => (0, i))) ='
      .var (Sum.inl (Sum.inr (1, i)))
  let f3 : Language.ring.Formula ((Σ i : ι, mons i) ⊕ (Fin 2 × ι)) := iInf l3
  let surjOn : Language.ring.Formula (α ⊕ Σ i : ι, mons i) :=
    Formula.iAlls ι
      (Formula.imp (φ.relabel (Sum.map Sum.inl id)) <|
        Formula.iExs ι <|
          ((φ.relabel (Sum.map Sum.inl (fun i => (0, i)))) ⊓
                (f3.relabel (fun x => (Equiv.sumAssoc _ _ _).symm (Sum.inr x)))).relabel
            (fun (i : (α ⊕ (Σ i : ι, mons i)) ⊕ (Fin 2 × ι)) =>
              show ((α ⊕ (Σ i : ι, mons i)) ⊕ ι) ⊕ ι from
                Sum.elim (Sum.inl ∘ Sum.inl) (fun i => if i.1 = 0 then Sum.inr i.2 else (Sum.inl (Sum.inr i.2))) i))
  let mapsTo : Language.ring.Formula (α ⊕ Σ i : ι, mons i) :=
    Formula.iAlls ι
      (Formula.imp (φ.relabel (Sum.map Sum.inl id))
        (φ.subst <|
          Sum.elim (fun a => .var (Sum.inl (Sum.inl a)))
            (fun i =>
              (termOfFreeCommRing (genericPolyMap mons i)).relabel (fun i => (Equiv.sumAssoc _ _ _).symm (Sum.inr i)))))
  Formula.iAlls (α ⊕ Σ i : ι, mons i) ((mapsTo.imp <| injOn.imp <| surjOn).relabel Sum.inr)

Похожие утверждения