CofinalReindexing.lean

1import BFPP.Families2import Mathlib.Order.Cofinal34/-! # Cofinal reindexing preserves inseparability -/56namespace BFPP78set_option autoImplicit false9open Set1011universe u v w v' w'12variable {K : Type u} {ι : Type v} {κ : Type w} {ι' : Type v'} {κ' : Type w'}13  [TopologicalSpace K] [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]14  [LinearOrder ι'] [OrderBot ι'] [LinearOrder κ'] [OrderBot κ']1516namespace IncreasingFamily1718def reindex (F : IncreasingFamily K ι) (φ : ι' → ι) (hφ : Monotone φ) (h₀ : φ ⊥ = ⊥) :19    IncreasingFamily K ι' where20  functions i := F.functions (φ i)21  monotone t := (F.monotone t).comp hφ22  bounds i t := F.bounds (φ i) t23  at_bot := by rw [h₀, F.at_bot]2425@[simp] theorem reindex_levels (F : IncreasingFamily K ι) (φ : ι' → ι)26    (hφ : Monotone φ) (h₀ : φ ⊥ = ⊥) (i : ι') :27    (F.reindex φ hφ h₀).levels i = F.levels (φ i) := rfl2829theorem reindex_union (F : IncreasingFamily K ι) (φ : ι' → ι)30    (hφ : Monotone φ) (h₀ : φ ⊥ = ⊥) (hcof : IsCofinal (range φ)) :31    (⋃ i, (F.reindex φ hφ h₀).levels i) = ⋃ i, F.levels i := by32  ext t33  simp only [mem_iUnion, reindex_levels]34  constructor35  · rintro ⟨i, hi⟩36    exact ⟨φ i, hi⟩37  · rintro ⟨i, hi⟩38    obtain ⟨_, ⟨j, rfl⟩, hij⟩ := hcof i39    exact ⟨j, F.levels_monotone hij hi⟩4041end IncreasingFamily4243namespace InseparablePair4445def reindex (F : InseparablePair K ι κ) (φ : ι' → ι) (ψ : κ' → κ)46    (hφ : Monotone φ) (hψ : Monotone ψ) (hφ₀ : φ ⊥ = ⊥) (hψ₀ : ψ ⊥ = ⊥)47    (hφcof : IsCofinal (range φ)) (hψcof : IsCofinal (range ψ)) : InseparablePair K ι' κ' where48  positive := F.positive.reindex φ hφ hφ₀49  negative := F.negative.reindex ψ hψ hψ₀50  orthogonal i j t := F.orthogonal (φ i) (ψ j) t51  inseparable := by52    rw [F.positive.reindex_union φ hφ hφ₀ hφcof, F.negative.reindex_union ψ hψ hψ₀ hψcof]53    exact F.inseparable5455end InseparablePair56end BFPP

SHA-256