LinearRefinement.lean

1 import KomorebiLSM.PredictiveClosure
2 import Mathlib.Algebra.Module.Submodule.LinearMap
3 
4 /-! P22 linear bridge: a finer summary can be initialized from a coarse
5 summary exactly when the coarse kernel is contained in the fine kernel.
6 The range-codomain version supplies surjectivity rather than assuming an
7 unjustified access to the full ambient coefficient space. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM
10 universe u v w t
11 variable {R : Type u} [Ring R]
12 variable {X : Type v} [AddCommGroup X] [Module R X]
13 variable {Z : Type w} [AddCommGroup Z] [Module R Z]
14 variable {Y : Type t} [AddCommGroup Y] [Module R Y]
15 
16 theorem linear_fiber_iff_kernel (gamma : X →ₗ[R] Z) (eta : X →ₗ[R] Y) :
17     FiberConstant gamma eta ↔ (∀ x, gamma x = 0 → eta x = 0) := by
18   constructor
19   · intro h x hx
20     simpa only [map_zero] using h x 0 (hx.trans gamma.map_zero.symm)
21   · intro h x y hxy
22     have hg : gamma (x-y) = 0 := by rw [map_sub, hxy, sub_self]
23     have he := h (x-y) hg
24     rwa [map_sub, sub_eq_zero] at he
25 
26 theorem linear_factor_iff_kernel
27     (gamma : X →ₗ[R] Z) (onto : ∀ z, ∃ x, gamma x = z) (eta : X →ₗ[R] Y) :
28     (∃ J : Z →ₗ[R] Y, J.comp gamma = eta) ↔
29       (∀ x, gamma x = 0 → eta x = 0) := by
30   constructor
31   · rintro ⟨J, hj⟩ x hx
32     have h := congrArg (fun f : X →ₗ[R] Y => f x) hj
33     simpa only [LinearMap.comp_apply, hx, map_zero] using h.symm
34   · intro h
35     obtain ⟨J, hj, _⟩ := (factor_exists_unique_iff gamma onto eta).mpr
36       ((linear_fiber_iff_kernel gamma eta).mpr h)
37     let f : Z →ₗ[R] Y :=
38       { toFun := J
39         map_add' := by
40           intro z w
41           obtain ⟨x, rfl⟩ := onto z
42           obtain ⟨y, rfl⟩ := onto w
43           rw [← gamma.map_add, hj, eta.map_add, hj, hj]
44         map_smul' := by
45           intro a z
46           obtain ⟨x, rfl⟩ := onto z
47           simp only [RingHom.id_apply]
48           rw [← gamma.map_smul, hj, eta.map_smul, hj] }
49     exact ⟨f, LinearMap.ext hj⟩
50 
51 theorem linear_factor_unique
52     (gamma : X →ₗ[R] Z) (onto : ∀ z, ∃ x, gamma x = z)
53     (eta : X →ₗ[R] Y) (J K : Z →ₗ[R] Y)
54     (hj : J.comp gamma = eta) (hk : K.comp gamma = eta) : J = K := by
55   ext z
56   obtain ⟨x, rfl⟩ := onto z
57   have h := congrArg (fun f : X →ₗ[R] Y => f x) (hj.trans hk.symm)
58   exact h
59 
60 end Komorebi.LSM

Back to source controls