SameKernel

formal source

 113
 114/-- Two primitive interfaces have the same kernel if they make the same
 115distinctions invisible. -/
 116def SameKernel {K : Type*} (I J : PrimitiveInterface K) : Prop :=
 117  ∀ x y : K, I.kernel x y ↔ J.kernel x y
 118
 119/-- If two interfaces have the same kernel, then their recognition lattices
 120are canonically equivalent. -/
 121noncomputable def latticeEquivOfSameKernel {K : Type*}
 122    (I J : PrimitiveInterface K) (h : SameKernel I J) :
 123    RecognitionLattice I ≃ RecognitionLattice J where
 124  toFun := Quotient.map (fun x => x) (by
 125    intro x y hxy
 126    exact (h x y).mp hxy)
 127  invFun := Quotient.map (fun x => x) (by
 128    intro x y hxy
 129    exact (h x y).mpr hxy)
 130  left_inv := by
 131    intro c
 132    refine Quotient.inductionOn c ?_
 133    intro x
 134    rfl
 135  right_inv := by
 136    intro c
 137    refine Quotient.inductionOn c ?_
 138    intro x
 139    rfl
 140
 141/-- The canonical equivalence sends each cell to the cell of the same
 142configuration. -/
 143theorem latticeEquivOfSameKernel_cell {K : Type*}
 144    (I J : PrimitiveInterface K) (h : SameKernel I J) (x : K) :
 145    latticeEquivOfSameKernel I J h (cellOf I x) = cellOf J x := rfl
 146