Documentation

ConNF.FOA.Approx.StructApprox

Structural approximations #

In this file, we define structural approximations, which are trees of base approximations.

Main declarations #

source
@[reducible, inline]
abbrev ConNF.StructApprox [ConNF.Params] (α : ConNF.TypeIndex) :
Type u

A β-structural approximation is a tree of base approximations.

Equations
Instances For

    The notions of approximation and exact approximation are defined "branchwise".

    source
    def ConNF.StructApprox.Approximates [ConNF.Params] {β : ConNF.TypeIndex} (π₀ : ConNF.StructApprox β) (π : ConNF.StructPerm β) :
    Prop
    Equations
    Instances For
      source
      def ConNF.StructApprox.ExactlyApproximates [ConNF.Params] {β : ConNF.TypeIndex} (π₀ : ConNF.StructApprox β) (π : ConNF.StructPerm β) :
      Prop
      Equations
      • π₀.ExactlyApproximates π = ∀ (A : ConNF.ExtendedIndex β), (π₀ A).ExactlyApproximates (π A)
      Instances For
        source
        def ConNF.StructApprox.Free [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (π₀ : ConNF.StructApprox ↑β) :
        Prop

        A structural approximation is said to be free if its derivative along any path A is A-free.

        Equations
        Instances For
          source
          theorem ConNF.StructApprox.Approximates.comp [ConNF.Params] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {π₀ : ConNF.StructApprox β} {π : ConNF.StructPerm β} (h : π₀.Approximates π) (A : Quiver.Path β γ) :
          ConNF.StructApprox.Approximates (ConNF.Tree.comp A π₀) (ConNF.Tree.comp A π)
          source
          theorem ConNF.StructApprox.ExactlyApproximates.comp [ConNF.Params] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {π₀ : ConNF.StructApprox β} {π : ConNF.StructPerm β} (h : π₀.ExactlyApproximates π) (A : Quiver.Path β γ) :
          ConNF.StructApprox.ExactlyApproximates (ConNF.Tree.comp A π₀) (ConNF.Tree.comp A π)