Documentation

Q2Presentation.Lifting.ExtensionGammaA

source
theorem Q2Presentation.Lifting.liftMarking_x0_mem_LY {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) :
liftMarking E boundaryPackage_GammaA F g f Gen.x0 ∈ Yt.LY

Lifts send x₀ into the wild part.

source
theorem Q2Presentation.Lifting.liftMarking_x1_mem_LY {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) :
liftMarking E boundaryPackage_GammaA F g f Gen.x1 ∈ Yt.LY

Lifts send x₁ into the wild part.

source
theorem Q2Presentation.Lifting.perturb_x0_mem_LY {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) (n : Gen → ↥E.N) :
perturb E (liftMarking E boundaryPackage_GammaA F g f₀) n Gen.x0 ∈ Yt.LY

Kernel perturbations keep x₀ in the wild part.

source
theorem Q2Presentation.Lifting.perturb_x1_mem_LY {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) (n : Gen → ↥E.N) :
perturb E (liftMarking E boundaryPackage_GammaA F g f₀) n Gen.x1 ∈ Yt.LY

Kernel perturbations keep x₁ in the wild part.

source
def Q2Presentation.Lifting.RowSystem {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) :
Type

The row system: kernel tuples killing both relator shadows at the base lift's marking.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Q2Presentation.Lifting.liftHom_equiv_rowSystem {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) :
    TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g ≃ RowSystem E F g f₀

    The lift fiber is the row system (N3): relative to a base lift, framed lifts biject with row-satisfying kernel tuples.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Q2Presentation.Lifting.liftHom_card_rowSystem {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) :
      Nat.card (TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) = Nat.card (RowSystem E F g f₀)

      Cardinality transport: |liftHom| = |row system|.

      source
      def Q2Presentation.Lifting.rowSystem_equiv_ker {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) :
      RowSystem E F g f₀ ≃ ↥(rowMap E (liftMarking E boundaryPackage_GammaA F g f₀)).ker

      The row system is the kernel of the row map (additive dictionary).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Q2Presentation.Lifting.liftHom_card_of_rowMap_surjective {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) (hsurj : Function.Surjective ⇑(rowMap E (liftMarking E boundaryPackage_GammaA F g f₀))) :
        Nat.card (TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) = Nat.card (NAdd E) ^ 2

        The master count reduction: when the row map at the base marking is surjective, the framed lifts number exactly |N|².