KMSKernelOrbits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Equal kernels give the same orbit under invertible postcomposition. The canonical range equivalence comes from the first isomorphism theorem; Mathlib's finite-dimensional subspace extension theorem then extends it to an automorphism of the ambient codomain. No orbit or counting premise is assumed.

def OAI.MaxCutGames.Inverse.KMSKernelOrbits.rangeEquivOfKerEq line 21
Source documentation
The range identification induced by a common kernel.
```
def rangeEquivOfKerEq (S T : F →ₗ[K] E) (hker : S.ker = T.ker) :
    S.range ≃ₗ[K] T.range :=
…
```
theorem OAI.MaxCutGames.Inverse.KMSKernelOrbits.rangeEquivOfKerEq_apply line 28
Source documentation
This identification respects every original vector, including vectors in the kernel and maps of rank zero.
```
theorem rangeEquivOfKerEq_apply (S T : F →ₗ[K] E) (hker : S.ker = T.ker) (x : F) :
    (rangeEquivOfKerEq S T hker ⟨S x, ⟨x, rfl⟩⟩ : E) = T x := by
…
```
Mentions: OAI.MaxCutGames.Inverse.KMSKernelOrbits.rangeEquivOfKerEq
theorem OAI.MaxCutGames.Inverse.KMSKernelOrbits.exists_postcomp_equiv_of_ker_eq line 39
Source documentation
Finite-dimensional image suffices: the ambient codomain and domain may otherwise be infinite-dimensional.
```
theorem exists_postcomp_equiv_of_ker_eq (S T : F →ₗ[K] E)
    [FiniteDimensional K S.range] (hker : S.ker = T.ker) :
    ∃ g : E ≃ₗ[K] E, g.toLinearMap.comp S = T := by
…
```
theorem OAI.MaxCutGames.Inverse.KMSKernelOrbits.ker_eq_iff_exists_postcomp_equiv line 51
Source documentation
Invertible postcomposition never changes the kernel. Thus the kernel is an exact orbit invariant, rather than only a necessary condition.
```
theorem ker_eq_iff_exists_postcomp_equiv (S T : F →ₗ[K] E)
    [FiniteDimensional K S.range] :
    S.ker = T.ker ↔ ∃ g : E ≃ₗ[K] E, g.toLinearMap.comp S = T := by
…
```