LinearMap.finiteDimensional_ker_and_quotient_range_of_exact_of_finiteDimensional
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_finiteDimensional_ker_and_quotient_range_of_exact_of_finiteDimensional
universe u vLean source · statement
theorem _root_.LinearMap.finiteDimensional_ker_and_quotient_range_of_exact_of_finiteDimensional
{k : Type u} [Field k]
{A₁ A₂ A₃ B₁ B₂ B₃ : Type v}
[AddCommGroup A₁] [Module k A₁] [AddCommGroup A₂] [Module k A₂] [AddCommGroup A₃] [Module k A₃]
[AddCommGroup B₁] [Module k B₁] [AddCommGroup B₂] [Module k B₂] [AddCommGroup B₃] [Module k B₃]
(d₁ : A₁ →ₗ[k] B₁) (d₂ : A₂ →ₗ[k] B₂) (d₃ : A₃ →ₗ[k] B₃)
(f₁ : A₁ →ₗ[k] A₂) (f₂ : A₂ →ₗ[k] A₃) (g₁ : B₁ →ₗ[k] B₂) (g₂ : B₂ →ₗ[k] B₃)
(hf₁ : Function.Injective f₁) (hf : Function.Exact f₁ f₂) (hf₂ : Function.Surjective f₂)
(hg₁ : Function.Injective g₁) (hg : Function.Exact g₁ g₂)
(h₁ : g₁ ∘ₗ d₁ = d₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ d₂ = d₃ ∘ₗ f₂)
[FiniteDimensional k (LinearMap.ker d₂)] [FiniteDimensional k (B₂ ⧸ LinearMap.range d₂)]
[FiniteDimensional k (LinearMap.ker d₃)] :
FiniteDimensional k (LinearMap.ker d₁) ∧ FiniteDimensional k (B₁ ⧸ LinearMap.range d₁)