Rename Foa to FOA

Signed-off-by: zeramorphic <[email protected]>

ConNF.lean

@@ -3,4 +3,4 @@ import ConNF.BaseType
 import ConNF.Structural
 import ConNF.Fuzz
 import ConNF.NewTangle
-import ConNF.Foa
+import ConNF.FOA

ConNF/FOA.lean

@@ -0,0 +1,6 @@
+import ConNF.FOA.Basic
+import ConNF.FOA.Approximation
+import ConNF.FOA.Action
+import ConNF.FOA.Complete
+import ConNF.FOA.Properties
+import ConNF.FOA.Result

ConNF/FOA/Action.lean

@@ -0,0 +1,6 @@
+import ConNF.FOA.Action.NearLitterAction
+import ConNF.FOA.Action.Complete
+import ConNF.FOA.Action.FillAtomOrbits
+import ConNF.FOA.Action.FillAtomRange
+import ConNF.FOA.Action.StructAction
+import ConNF.FOA.Action.Refine

ConNF/Foa/Action/Complete.lean → ConNF/FOA/Action/Complete.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Action.NearLitterAction
+import ConNF.FOA.Action.NearLitterAction
 
 /-!
 # Completed permutations
@@ -13,7 +13,7 @@ universe u
 namespace ConNF
 
 variable [Params.{u}] (φ : NearLitterAction) [BasePositions] [Level]
-  [FoaAssumptions] {β : Λ} {A : ExtendedIndex β}
+  [FOAAssumptions] {β : Λ} {A : ExtendedIndex β}
 
 namespace NearLitterAction
 

ConNF/Foa/Action/FillAtomOrbits.lean → ConNF/FOA/Action/FillAtomOrbits.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Action.NearLitterAction
+import ConNF.FOA.Action.NearLitterAction
 
 open Cardinal Quiver Set Sum WithBot
 

ConNF/Foa/Action/FillAtomRange.lean → ConNF/FOA/Action/FillAtomRange.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Action.NearLitterAction
+import ConNF.FOA.Action.NearLitterAction
 
 open Cardinal Quiver Set Sum WithBot
 

ConNF/Foa/Action/NearLitterAction.lean → ConNF/FOA/Action/NearLitterAction.lean

@@ -1,6 +1,6 @@
-import ConNF.Foa.Basic.CompleteOrbit
-import ConNF.Foa.Basic.Reduction
-import ConNF.Foa.Approximation.NearLitterApprox
+import ConNF.FOA.Basic.CompleteOrbit
+import ConNF.FOA.Basic.Reduction
+import ConNF.FOA.Approximation.NearLitterApprox
 
 open Cardinal Quiver Set Sum WithBot
 
@@ -246,7 +246,7 @@ theorem roughLitterMapOrElse_injOn (hφ : φ.Lawful) :
   rw [φ.roughLitterMapOrElse_of_dom hL₁, φ.roughLitterMapOrElse_of_dom hL₂] at h
   exact hφ.litterMap_injective hL₁ hL₂ (NearLitter.inter_nonempty_of_fst_eq_fst h)
 
-variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} {A : ExtendedIndex β}
+variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} {A : ExtendedIndex β}
 
 theorem mk_not_bannedLitter_and_flexible : #{L | ¬φ.BannedLitter L ∧ Flexible A L} = #μ := by
   refine' le_antisymm ((mk_subtype_le _).trans mk_litter.le) _

ConNF/Foa/Action/Refine.lean → ConNF/FOA/Action/Refine.lean

@@ -1,7 +1,7 @@
-import ConNF.Foa.Basic.Flexible
-import ConNF.Foa.Action.StructAction
-import ConNF.Foa.Action.FillAtomRange
-import ConNF.Foa.Action.FillAtomOrbits
+import ConNF.FOA.Basic.Flexible
+import ConNF.FOA.Action.StructAction
+import ConNF.FOA.Action.FillAtomRange
+import ConNF.FOA.Action.FillAtomOrbits
 
 open Quiver Set
 
@@ -87,7 +87,7 @@ end StructAction
 
 namespace StructAction
 
-variable [BasePositions] [Level] [FoaAssumptions] {β : Λ}
+variable [BasePositions] [Level] [FOAAssumptions] {β : Λ}
 
 /-- Refine and complete this action into a structural approximation. -/
 noncomputable def rc (φ : StructAction β) (h : φ.Lawful) : StructApprox β :=

ConNF/Foa/Action/StructAction.lean → ConNF/FOA/Action/StructAction.lean

@@ -1,6 +1,6 @@
-import ConNF.Foa.Basic.Flexible
-import ConNF.Foa.Approximation.StructApprox
-import ConNF.Foa.Action.Complete
+import ConNF.FOA.Basic.Flexible
+import ConNF.FOA.Approximation.StructApprox
+import ConNF.FOA.Action.Complete
 
 open Cardinal Quiver Set Sum WithBot
 
@@ -27,7 +27,7 @@ def Lawful {β : TypeIndex} (φ : StructAction β) : Prop :=
   ∀ B, (φ B).Lawful
 
 /-- This structural action maps flexible litters to flexible litters. -/
-def MapFlexible [BasePositions] [Level] [FoaAssumptions] {β : Λ} (φ : StructAction β) :
+def MapFlexible [BasePositions] [Level] [FOAAssumptions] {β : Λ} (φ : StructAction β) :
     Prop :=
   ∀ (B) (L : Litter) (hL), Flexible B L → Flexible B (((φ B).litterMap L).get hL).1
 
@@ -36,7 +36,7 @@ section Precise
 def Precise {β : TypeIndex} (φ : StructAction β) : Prop :=
   ∀ B, (φ B).Precise
 
-variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} (φ : StructAction β)
+variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} (φ : StructAction β)
 
 noncomputable def complete (hφ : φ.Lawful) : StructApprox β := fun B => (φ B).complete (hφ B) B
 
@@ -67,7 +67,7 @@ theorem smul_nearLitter_eq_of_precise {hφ : φ.Lawful} (hφp : φ.Precise) {π
 
 end Precise
 
-variable [BasePositions] [Level] [FoaAssumptions] {β : Λ}
+variable [BasePositions] [Level] [FOAAssumptions] {β : Λ}
 
 instance {β : TypeIndex} : PartialOrder (StructAction β)
     where

ConNF/FOA/Approximation.lean

@@ -0,0 +1,2 @@
+import ConNF.FOA.Approximation.NearLitterApprox
+import ConNF.FOA.Approximation.StructApprox

ConNF/Foa/Approximation/NearLitterApprox.lean → ConNF/FOA/Approximation/NearLitterApprox.lean

@@ -1,6 +1,6 @@
 import ConNF.Mathlib.Logic.Equiv.LocalPerm
-import ConNF.Foa.Basic.Flexible
-import ConNF.Foa.Basic.Sublitter
+import ConNF.FOA.Basic.Flexible
+import ConNF.FOA.Basic.Sublitter
 
 open Quiver Set Sum
 
@@ -196,7 +196,7 @@ theorem ExactlyApproximates.mem_litterSet_inv {π₀ : NearLitterApprox} {π : N
     (hπ : π₀.ExactlyApproximates π) (a : Atom) (ha : a ∉ π₀.atomPerm.domain) :
     π⁻¹ • a ∈ litterSet (π⁻¹ • a.1) := by contrapose! ha; exact hπ.exception_mem _ (Or.inr ha)
 
-def Free [BasePositions] [Level] [FoaAssumptions] {β : TypeIndex} (π : NearLitterApprox)
+def Free [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox)
     (A : ExtendedIndex β) : Prop :=
   ∀ L ∈ π.litterPerm.domain, Flexible A L
 

ConNF/Foa/Approximation/StructApprox.lean → ConNF/FOA/Approximation/StructApprox.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Approximation.NearLitterApprox
+import ConNF.FOA.Approximation.NearLitterApprox
 
 open Quiver Set Sum
 
@@ -27,7 +27,7 @@ def Approximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β)
 def ExactlyApproximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β) : Prop :=
   ∀ A, (π₀ A).ExactlyApproximates (π A)
 
-variable [BasePositions] [Level] [FoaAssumptions]
+variable [BasePositions] [Level] [FOAAssumptions]
 
 def Free {β : Λ} (π₀ : StructApprox β) : Prop :=
   ∀ A, (π₀ A).Free A

ConNF/FOA/Basic.lean

@@ -0,0 +1,6 @@
+import ConNF.FOA.Basic.CompleteOrbit
+import ConNF.FOA.Basic.Sublitter
+import ConNF.FOA.Basic.Hypotheses
+import ConNF.FOA.Basic.Constrains
+import ConNF.FOA.Basic.Reduction
+import ConNF.FOA.Basic.Flexible

ConNF/Foa/Basic/Constrains.lean → ConNF/FOA/Basic/Constrains.lean

@@ -1,6 +1,6 @@
 import Mathlib.Data.Prod.Lex
 import ConNF.Fuzz
-import ConNF.Foa.Basic.Hypotheses
+import ConNF.FOA.Basic.Hypotheses
 
 /-!
 # Constraints
@@ -58,7 +58,7 @@ theorem pos_atomNearLitter_inr (N : NearLitter) :
 
 end ExtendedIndex
 
-variable [BasePositions] [Level] [FoaAssumptions] {β : Λ}
+variable [BasePositions] [Level] [FOAAssumptions] {β : Λ}
 
 /-- Support conditions can be said to *constrain* each other in a number of ways.
 1. `(L, A) ≺ (a, A)` when `a ∈ L` and `L` is a litter. We can say that an atom is constrained by the

ConNF/Foa/Basic/Flexible.lean → ConNF/FOA/Basic/Flexible.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Basic.Constrains
+import ConNF.FOA.Basic.Constrains
 
 open Quiver Set Sum WithBot
 
@@ -8,7 +8,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : TypeIndex}
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex}
 
 /-- A litter is *inflexible* if it is the image of some f-map. -/
 @[mk_iff]

ConNF/Foa/Basic/Hypotheses.lean → ConNF/FOA/Basic/Hypotheses.lean

@@ -9,8 +9,8 @@ This file contains the inductive hypotheses required for proving the freedom of
 
 * `ConNF.PositionedTypedObjects`: Asserts that the positions of typed objects agree with the
     position functions defined on atoms and near-litters in `BasePositions`.
-* `ConNF.FoaData`: Contains various kinds of tangle data for all levels below `α`.
-* `ConNF.FoaAssumptions`: Describes how the type levels in the `FoaData` tangle together.
+* `ConNF.FOAData`: Contains various kinds of tangle data for all levels below `α`.
+* `ConNF.FOAAssumptions`: Describes how the type levels in the `FOAData` tangle together.
 -/
 
 open Set WithBot
@@ -49,15 +49,15 @@ This structure combines the following data:
 * `pos : Tangle β ↪ μ`
 * `typedAtom` and `typedNearLitter`
 -/
-class FoaData where
+class FOAData where
   lowerTangleData : ∀ β : Λ, [LeLevel β] → TangleData β
   lowerPositionedTangles : ∀ β : Λ, [LtLevel β] → PositionedTangles β
   lowerTypedObjects : ∀ β : Λ, [LeLevel β] → TypedObjects β
   lowerPositionedTypedObjects : ∀ β : Λ, [LtLevel β] → PositionedTypedObjects β
 
-namespace FoaData
+namespace FOAData
 
-variable [FoaData] {β : Λ} [LeLevel β] {γ : Λ} [LtLevel γ]
+variable [FOAData] {β : Λ} [LeLevel β] {γ : Λ} [LtLevel γ]
 
 instance tangleData : TangleData β :=
   lowerTangleData β
@@ -79,10 +79,10 @@ noncomputable instance iioBotPositionedTangles : ∀ β : TypeIndex, [LtLevel β
   | ⊥, _ => Bot.positionedTangles
   | (β : Λ), _ => lowerPositionedTangles β
 
-end FoaData
+end FOAData
 
 /-- Assumptions detailing how the different levels of the tangled structure interact. -/
-class FoaAssumptions extends FoaData where
+class FOAAssumptions extends FOAData where
   /-- The one-step derivative map between types of allowable permutations.
   We can think of this map as `cons`ing a single morphism on a path. -/
   allowableCons :
@@ -117,12 +117,12 @@ class FoaAssumptions extends FoaData where
     (γ : TypeIndex) [LtLevel γ] (hγ : γ < β) :
     allowableCons hγ (allowableOfSmulFuzz β ρs h) = ρs γ hγ
 
-export FoaAssumptions (allowableCons allowableCons_eq designatedSupport_smul
+export FOAAssumptions (allowableCons allowableCons_eq designatedSupport_smul
   smul_fuzz allowableOfSmulFuzz allowableOfSmulFuzz_comp_eq)
 
 attribute [simp] designatedSupport_smul allowableOfSmulFuzz_comp_eq
 
-variable [FoaAssumptions]
+variable [FOAAssumptions]
 
 /-- A primitive version of `Allowable.comp` with different arguments. This is always the wrong
 spelling to use. -/
@@ -148,7 +148,7 @@ def Allowable.comp {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (A : Quiver.Pat
   Allowable.comp' A
 
 /-! We prove that `Allowable.comp` is functorial. In addition, we prove a number of lemmas about
-`FoaAssumptions`. -/
+`FOAAssumptions`. -/
 
 @[simp]
 theorem Allowable.comp_nil {β : TypeIndex} [LeLevel β] :

ConNF/Foa/Basic/Reduction.lean → ConNF/FOA/Basic/Reduction.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Basic.Constrains
+import ConNF.FOA.Basic.Constrains
 
 /-!
 # Reductions of supports
@@ -25,7 +25,7 @@ open scoped Cardinal Pointwise
 
 namespace ConNF
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions]
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions]
 variable {β : Λ} {G : Type _} {τ : Type _} [SMul G (SupportCondition β)] [SMul G τ] {x : τ}
 
 /-- A support condition is *reduced* if it is an atom or a litter. -/

ConNF/FOA/Complete.lean

@@ -0,0 +1,6 @@
+import ConNF.FOA.Complete.HypAction
+import ConNF.FOA.Complete.AtomCompletion
+import ConNF.FOA.Complete.FlexibleCompletion
+import ConNF.FOA.Complete.LitterCompletion
+import ConNF.FOA.Complete.NearLitterCompletion
+import ConNF.FOA.Complete.CompleteAction

ConNF/Foa/Complete/AtomCompletion.lean → ConNF/FOA/Complete/AtomCompletion.lean

@@ -1,5 +1,5 @@
-import ConNF.Foa.Complete.HypAction
-import ConNF.Foa.Approximation
+import ConNF.FOA.Complete.HypAction
+import ConNF.FOA.Approximation
 
 open Set Sum
 
@@ -9,7 +9,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} (π : StructApprox β)
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} (π : StructApprox β)
 
 namespace StructApprox
 

ConNF/Foa/Complete/CompleteAction.lean → ConNF/FOA/Complete/CompleteAction.lean

@@ -1,6 +1,6 @@
 import Mathlib.Order.Extension.Well
-import ConNF.Foa.Complete.AtomCompletion
-import ConNF.Foa.Complete.NearLitterCompletion
+import ConNF.FOA.Complete.AtomCompletion
+import ConNF.FOA.Complete.NearLitterCompletion
 
 open Equiv Function Quiver Set Sum WithBot
 
@@ -12,7 +12,7 @@ namespace ConNF
 
 namespace StructApprox
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
   [FreedomOfActionHypothesis β]
 
 /-!

ConNF/Foa/Complete/FlexibleCompletion.lean → ConNF/FOA/Complete/FlexibleCompletion.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Approximation.NearLitterApprox
+import ConNF.FOA.Approximation.NearLitterApprox
 
 open Set
 
@@ -8,7 +8,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : TypeIndex}
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex}
   (π : NearLitterApprox) (A : ExtendedIndex β)
 
 namespace NearLitterApprox

ConNF/Foa/Complete/HypAction.lean → ConNF/FOA/Complete/HypAction.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Basic.Constrains
+import ConNF.FOA.Basic.Constrains
 
 open Quiver Set Sum
 
@@ -8,7 +8,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions]
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions]
 
 /-!
 # Induction on support conditions

ConNF/Foa/Complete/LitterCompletion.lean → ConNF/FOA/Complete/LitterCompletion.lean

@@ -1,7 +1,7 @@
-import ConNF.Foa.Basic.Reduction
-import ConNF.Foa.Complete.HypAction
-import ConNF.Foa.Action.Refine
-import ConNF.Foa.Complete.FlexibleCompletion
+import ConNF.FOA.Basic.Reduction
+import ConNF.FOA.Complete.HypAction
+import ConNF.FOA.Action.Refine
+import ConNF.FOA.Complete.FlexibleCompletion
 
 open Quiver Set Sum WithBot
 
@@ -13,16 +13,16 @@ namespace ConNF
 
 namespace StructApprox
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions]
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions]
 
 /-- The inductive hypothesis used for proving freedom of action:
 Every free approximation exactly approximates some allowable permutation. -/
-def FoaIh (β : Λ) [LeLevel β] : Prop :=
+def FOAIh (β : Λ) [LeLevel β] : Prop :=
   ∀ π₀ : StructApprox β, π₀.Free →
   ∃ π : Allowable β, π₀.ExactlyApproximates (Allowable.toStructPerm π)
 
 class FreedomOfActionHypothesis (β : Λ) [LeLevel β] : Prop where
-  freedomOfAction_of_lt : ∀ γ < β, [LeLevel γ] → FoaIh γ
+  freedomOfAction_of_lt : ∀ γ < β, [LeLevel γ] → FOAIh γ
 
 export FreedomOfActionHypothesis (freedomOfAction_of_lt)
 

ConNF/Foa/Complete/NearLitterCompletion.lean → ConNF/FOA/Complete/NearLitterCompletion.lean

@@ -1,4 +1,4 @@
-import ConNF.Foa.Complete.LitterCompletion
+import ConNF.FOA.Complete.LitterCompletion
 
 open Set Sum
 
@@ -10,7 +10,7 @@ namespace ConNF
 
 namespace StructApprox
 
-variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
   [FreedomOfActionHypothesis β]
 
 def nearLitterHypothesis (A : ExtendedIndex β) (N : NearLitter) (H : HypAction ⟨A, inr N⟩) :