Gluing compatible closed prefixes below a limit

structure ScottishBook155.CompatiblePrefixFamily (j : RecursionIndexZero) : Type 1

A family of closed prefixes which literally restrict to one another.

• item (i : ↑(Set.Iio j)) : ProtectedPrefix ↑i

  The closed protected prefix assigned to each index below the limit.

• coherent (i k : ↑(Set.Iio j)) (hik : ↑i ≤ ↑k) : ((self.item k).restriction hik).chain = (self.item i).chain

noncomputable def ScottishBook155.ProtectedPrefix.linkOfRestriction {i k : RecursionIndexZero} (Pi : ProtectedPrefix i) (Pk : ProtectedPrefix k) (hik : i ≤ k) (hchain : (Pk.restriction hik).chain = Pi.chain) : ProtectedLink Pi.topStage Pk.topStage 1

The top-to-top link supplied by a restriction equality.

Equations

• Pi.linkOfRestriction Pk hik hchain = ScottishBook155.ProtectedLink.castSource ⋯ (Pk.chain.link ⟨i, hik⟩ ⟨k, ⋯⟩ hik)

@[reducible, inline]

abbrev ScottishBook155.CompatiblePrefixFamily.stage {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i : ↑(Set.Iio j)) : ProtectedStage (1 / 2)

The top stage of the prefix indexed by i.

Equations

• F.stage i = (F.item i).topStage

noncomputable def ScottishBook155.CompatiblePrefixFamily.link {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k : ↑(Set.Iio j)) (hik : i ≤ k) : ProtectedLink (F.stage i) (F.stage k) 1

The canonical protected link between two members of a compatible prefix family.

Equations

• F.link i k hik = (F.item i).linkOfRestriction (F.item k) hik ⋯

theorem ScottishBook155.CompatiblePrefixFamily.stageEq {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k : ↑(Set.Iio j)) (hik : i ≤ k) : (F.item k).chain.stage ⟨↑i, hik⟩ = F.stage i

Equality between an earlier top stage and the corresponding stage inside a later compatible prefix.

theorem ScottishBook155.CompatiblePrefixFamily.link_sourceEmbedding_apply {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k : ↑(Set.Iio j)) (hik : i ≤ k) (x : (F.stage i).source.carrier) : (F.link i k hik).sourceEmbedding x = ((F.item k).chain.sourceSystem.embed ⟨↑i, hik⟩ ⟨↑k, ⋯⟩ hik) (ProtectedStage.castSourcePoint ⋯ x)

theorem ScottishBook155.CompatiblePrefixFamily.link_targetEmbedding_apply {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k : ↑(Set.Iio j)) (hik : i ≤ k) (x : (F.stage i).target.carrier) : (F.link i k hik).targetEmbedding x = ((F.item k).chain.targetSystem.embed ⟨↑i, hik⟩ ⟨↑k, ⋯⟩ hik) (ProtectedStage.castTargetPoint ⋯ x)

theorem ScottishBook155.CompatiblePrefixFamily.link_sourceProjection_apply {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k : ↑(Set.Iio j)) (hik : i ≤ k) (z : (F.stage k).source.carrier) : (F.link i k hik).sourceProjection z = ProtectedStage.castSourcePoint ⋯ (((F.item k).chain.sourceSystem.project ⟨↑i, hik⟩ ⟨↑k, ⋯⟩ hik) z)

theorem ScottishBook155.CompatiblePrefixFamily.link_targetProjection_apply {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k : ↑(Set.Iio j)) (hik : i ≤ k) (z : (F.stage k).target.carrier) : (F.link i k hik).targetProjection z = ProtectedStage.castTargetPoint ⋯ (((F.item k).chain.targetSystem.project ⟨↑i, hik⟩ ⟨↑k, ⋯⟩ hik) z)

theorem ScottishBook155.CompatiblePrefixFamily.source_cast_embed_eq_later {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k m : ↑(Set.Iio j)) (hik : i ≤ k) (hkm : k ≤ m) (x : (F.stage i).source.carrier) : ProtectedStage.castSourcePoint ⋯ (((F.item k).chain.sourceSystem.embed ⟨↑i, hik⟩ ⟨↑k, ⋯⟩ hik) (ProtectedStage.castSourcePoint ⋯ x)) = ((F.item m).chain.sourceSystem.embed ⟨↑i, ⋯⟩ ⟨↑k, hkm⟩ hik) (ProtectedStage.castSourcePoint ⋯ x)

theorem ScottishBook155.CompatiblePrefixFamily.target_cast_embed_eq_later {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i k m : ↑(Set.Iio j)) (hik : i ≤ k) (hkm : k ≤ m) (x : (F.stage i).target.carrier) : ProtectedStage.castTargetPoint ⋯ (((F.item k).chain.targetSystem.embed ⟨↑i, hik⟩ ⟨↑k, ⋯⟩ hik) (ProtectedStage.castTargetPoint ⋯ x)) = ((F.item m).chain.targetSystem.embed ⟨↑i, ⋯⟩ ⟨↑k, hkm⟩ hik) (ProtectedStage.castTargetPoint ⋯ x)

theorem ScottishBook155.CompatiblePrefixFamily.source_cast_project_eq_later {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (a i k : ↑(Set.Iio j)) (hai : a ≤ i) (hik : i ≤ k) (x : (F.stage i).source.carrier) : ProtectedStage.castSourcePoint ⋯ (((F.item k).chain.sourceSystem.project ⟨↑a, ⋯⟩ ⟨↑i, hik⟩ hai) (ProtectedStage.castSourcePoint ⋯ x)) = ProtectedStage.castSourcePoint ⋯ (((F.item i).chain.sourceSystem.project ⟨↑a, hai⟩ ⟨↑i, ⋯⟩ hai) x)

theorem ScottishBook155.CompatiblePrefixFamily.target_cast_project_eq_later {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (a i k : ↑(Set.Iio j)) (hai : a ≤ i) (hik : i ≤ k) (x : (F.stage i).target.carrier) : ProtectedStage.castTargetPoint ⋯ (((F.item k).chain.targetSystem.project ⟨↑a, ⋯⟩ ⟨↑i, hik⟩ hai) (ProtectedStage.castTargetPoint ⋯ x)) = ProtectedStage.castTargetPoint ⋯ (((F.item i).chain.targetSystem.project ⟨↑a, hai⟩ ⟨↑i, ⋯⟩ hai) x)

noncomputable def ScottishBook155.CompatiblePrefixFamily.openChain {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) : ProtectedChain (1 / 2) 1

Glue a compatible family of closed prefixes into one protected chain on the open initial segment.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ScottishBook155.CompatiblePrefixFamily.closedToOpen {j : RecursionIndexZero} (i : ↑(Set.Iio j)) : ↑(Set.Iic ↑i) ↪o ↑(Set.Iio j)

Include the closed initial segment ending at i into the ambient open initial segment below j.

Equations

• ScottishBook155.CompatiblePrefixFamily.closedToOpen i = { toFun := fun (a : ↑(Set.Iic ↑i)) => ⟨↑a, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

theorem ScottishBook155.CompatiblePrefixFamily.closedToOpen_le {j : RecursionIndexZero} (i : ↑(Set.Iio j)) (a : ↑(Set.Iic ↑i)) : (closedToOpen i) a ≤ i

theorem ScottishBook155.CompatiblePrefixFamily.openChain_restriction {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i : ↑(Set.Iio j)) : F.openChain.reindex (closedToOpen i) = (F.item i).chain

The glued open chain restricts at every member of the compatible family to the closed prefix supplied at that member.

theorem ScottishBook155.ProtectedPrefix.ofLimit_restriction {j : RecursionIndexZero} (hj : Order.IsSuccLimit j) (F : CompatiblePrefixFamily j) (hSource : ∀ (i : ↑(Set.Iio j)), Cardinal.mk (F.openChain.stage i).source.carrier ≤ stageCardinal) (hTarget : ∀ (i : ↑(Set.Iio j)), Cardinal.mk (F.openChain.stage i).target.carrier ≤ stageCardinal) (i : ↑(Set.Iio j)) : (ofLimit j hj F.openChain hSource hTarget).restriction ⋯ = F.item i

The prefix obtained by adjoining a completed limit stage restricts to every member of the compatible family used to build that limit.