DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Use mathlib definition of inverses for Isomorphism.lean

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-06-24 14:30:00 -05:00
parent 97a9150bf3
commit 9ab43b34ef
2 changed files with 4 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
lean/Spa/Isomorphism.lean
View File

@@ -5,20 +5,18 @@ namespace Spa
def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β] def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
[I : FiniteHeightLattice α] (f : α → β) (g : β → α) [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
(hf : Monotone f) (hg : Monotone g) (hf : Monotone f) (hg : Monotone g)
(hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) : (hgf : Function.LeftInverse g f) (hfg : Function.LeftInverse f g) :
FiniteHeightLattice β where FiniteHeightLattice β where
bot := f ⊥ bot := f ⊥
top := f ⊤ top := f ⊤
height := I.height height := I.height
longestChain := longestChain :=
{ series := { series :=
I.longestChain.series.map f I.longestChain.series.map f (hf.strictMono_of_injective hgf.injective)
(hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
head_series := congrArg f I.longestChain.head_series head_series := congrArg f I.longestChain.head_series
last_series := congrArg f I.longestChain.last_series last_series := congrArg f I.longestChain.last_series
length_series := I.longestChain.length_series } length_series := I.longestChain.length_series }
chains_bounded := fun c => chains_bounded := fun c =>
I.chains_bounded I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
(c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
end Spa end Spa

2
lean/Spa/Lattice/FiniteMap.lean
View File

@@ -516,7 +516,7 @@ def fixedHeight [FiniteHeightLattice B] (ks : List A) :
FiniteHeightLattice (FiniteMap A B ks) := FiniteHeightLattice (FiniteMap A B ks) :=
FiniteHeightLattice.transport FiniteHeightLattice.transport
(ofIter ks) toIter (ofIter_monotone ks) toIter_monotone (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
(toIter_ofIter ks) (fun fm => ofIter_toIter fm) (toIter_ofIter ks) ofIter_toIter
instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) := instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
fixedHeight ks fixedHeight ks