English
Stronger form of congrLinearEquiv.trans for semilinear maps; equality holds unconditionally when composing via trans.
Русский
Усиленная форма congrLinearEquiv.trans для семилинейных отображений; равенство выполняется безусловно при композиции через trans.
LaTeX
$$$ congrLinearEquiv\; e_{12}.trans\; e_{23} = congrLinearEquiv (e_{12}.trans e_{23}) $$$
Lean4
/-- **Goursat's lemma** for a submodule of a product with surjective projections.
If `L` is a submodule of `M × N` which projects fully on both factors, then there exist submodules
`M' ≤ M` and `N' ≤ N` such that `M' × N' ≤ L` and the image of `L` in `(M ⧸ M') × (N ⧸ N')` is the
graph of an isomorphism of `R`-modules `(M ⧸ M') ≃ (N ⧸ N')`.
`M` and `N` can be explicitly constructed as `L.goursatFst` and `L.goursatSnd` respectively. -/
theorem goursat_surjective :
∃ e : (M ⧸ L.goursatFst) ≃ₗ[R] N ⧸ L.goursatSnd,
LinearMap.range ((L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ).comp L.subtype) = e.graph :=
by
-- apply add-group result
obtain ⟨(e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd), he⟩ := L.toAddSubgroup.goursat_surjective hL₁ hL₂
have (r : R) (x : M ⧸ L.goursatFst) : e (r • x) = r • e x :=
by
change (r • x, r • e x) ∈ e.toAddMonoidHom.graph
rw [← he, ← Prod.smul_mk]
have : (x, e x) ∈ e.toAddMonoidHom.graph := rfl
rw [← he, AddMonoidHom.mem_range] at this
rcases this with ⟨⟨l, hl⟩, hl'⟩
use ⟨r • l, L.smul_mem r hl⟩
rw [← hl']
rfl
-- define the map as an R-linear equiv
use { e with map_smul' := this }
rw [← toAddSubgroup_injective.eq_iff]
convert he using 1
ext v
rw [mem_toAddSubgroup, mem_graph_iff, Eq.comm]
rfl
