Equivalence between two set of minimal generators over local ring

theorem LinearMap.baseChange_bijective_of_surjective_of_spanFinrank_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {F₁ : Type u_3} [AddCommGroup F₁] [Module R F₁] [IsLocalRing R] [Module.Finite R M] [Module.Finite R F₁] (f : F₁ →ₗ[R] M) (surj : Function.Surjective ⇑f) (hrk : ⊤.spanFinrank = ⊤.spanFinrank) : Function.Bijective ⇑(baseChange (IsLocalRing.ResidueField R) f)

theorem LinearMap.baseChange_bijective_of_surjective_of_rank_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {F₁ : Type u_3} [AddCommGroup F₁] [Module R F₁] [IsLocalRing R] [Module.Free R F₁] [Module.Finite R M] (f : F₁ →ₗ[R] M) (surj : Function.Surjective ⇑f) (hrk : Module.rank R F₁ = ↑⊤.spanFinrank) : Function.Bijective ⇑(baseChange (IsLocalRing.ResidueField R) f)

theorem LinearMap.bijective_of_surjective_of_rank_eq_of_of_comp_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {F₁ : Type u_3} {F₂ : Type u_4} [AddCommGroup F₁] [Module R F₁] [AddCommGroup F₂] [Module R F₂] [IsLocalRing R] [Module.Free R F₁] [Module.Free R F₂] [Module.Finite R M] (f : F₁ →ₗ[R] M) (surjf : Function.Surjective ⇑f) (g : F₂ →ₗ[R] M) (surjg : Function.Surjective ⇑g) (hrk1 : Module.rank R F₁ = ↑⊤.spanFinrank) (hrk2 : Module.rank R F₂ = ↑⊤.spanFinrank) (h : F₁ →ₗ[R] F₂) (eq : g ∘ₗ h = f) : Function.Bijective ⇑h

theorem LinearMap.bijective_of_rank_eq_of_of_comp_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {F₁ : Type u_3} {F₂ : Type u_4} [AddCommGroup F₁] [Module R F₁] [AddCommGroup F₂] [Module R F₂] [IsLocalRing R] [Module.Free R F₁] [Module.Free R F₂] (N : Submodule R M) (fg : N.FG) (f : F₁ →ₗ[R] M) (g : F₂ →ₗ[R] M) (hrf : f.range = N) (hrg : g.range = N) (hrk1 : Module.rank R F₁ = ↑N.spanFinrank) (hrk2 : Module.rank R F₂ = ↑N.spanFinrank) (h : F₁ →ₗ[R] F₂) (eq : g ∘ₗ h = f) : Function.Bijective ⇑h

theorem LinearEquiv.exists_of_length_eq_spanRank {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) (fg : I.FG) {l l' : List R} (eq1 : Ideal.ofList l = I) (eq2 : Ideal.ofList l' = I) (len1 : l.length = Submodule.spanFinrank I) (len2 : l'.length = Submodule.spanFinrank I) : ∃ (e : (Fin l.length → R) ≃ₗ[R] Fin l'.length → R), Fintype.linearCombination R l'.get ∘ₗ ↑e = Fintype.linearCombination R l.get