AffinePairContract.lean

1 module
2 public import AffineSharedCorrection
3 
4 @[expose] public section
5 set_option autoImplicit false
6 
7 open Komorebi.NativeAffine Komorebi.AffinePair
8 
9 /-- Exact application contract: both original congruences and the lower
10 residue condition are expanded, as is the quotient by the two actual kernels. -/
11 example (d e f p L : ℕ) (hp : 0 < p)
12     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
13     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
14     (b r : Fin e → ℤ) (c s : Fin f → ℤ) (x u v : Fin d → ℤ)
15     (hr : A x - b = (p : ℤ)^L • r)
16     (hs : B x - c = (p : ℤ)^L • s)
17     (hu : reduction p e (r + A u) = 0)
18     (hv : reduction p f (s + B v) = 0) :
19     (∃ y : Fin d → ℤ,
20       (∀ i, (p : ℤ)^L ∣ (y - x) i) ∧
21       (∀ i, (p : ℤ)^(L+1) ∣ (A y - b) i) ∧
22       (∀ i, (p : ℤ)^(L+1) ∣ (B y - c) i)) ↔
23     (Submodule.Quotient.mk u : (Fin d → ℤ) ⧸
24         (LinearMap.ker (digitMap p A) ⊔ LinearMap.ker (digitMap p B))) =
25       Submodule.Quotient.mk v :=
26   joint_lift_iff_class_eq p L hp A B b r c s x u v hr hs hu hv
27 
28 example (d e f p : ℕ) (hp : 0 < p)
29     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
30     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ)) :
31     Finite ((Fin d → ℤ) ⧸
32       (LinearMap.ker (digitMap p A) ⊔ LinearMap.ker (digitMap p B))) :=
33   shared_obstruction_finite p hp A B

Back to source controls