def directSumBilinForm {K : Type u_1} [Field K] {V₁ : Type u_2} [AddCommGroup V₁] [Module K V₁] {V₂ : Type u_3} [AddCommGroup V₂] [Module K V₂] (B₁ : V₁ →ₗ[K] V₁ →ₗ[K] K) (B₂ : V₂ →ₗ[K] V₂ →ₗ[K] K) : V₁ × V₂ →ₗ[K] V₁ × V₂ →ₗ[K] K

def Submodule.localize {A : Type u_1} [CommRing A] {V : Type u_2} [AddCommGroup V] [Module A V] (S : Submonoid A) (M : Submodule A V) : Submodule A V

theorem dualLattice_eq_dualSubmodule {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (φ : V →ₗ[K] V →ₗ[K] K) (M : Submodule A V) : dualLattice A K V φ M = LinearMap.BilinForm.dualSubmodule φ M

theorem prop_5_7_existence {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) : ∃ (b' : Module.Basis ι K V), ∀ (i j : ι), (B (b' i)) (b j) = if j = i then 1 else 0

theorem prop_5_7_uniqueness {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b b₁ b₂ : Module.Basis ι K V) (h₁ : ∀ (i j : ι), (B (b₁ i)) (b j) = if j = i then 1 else 0) (h₂ : ∀ (i j : ι), (B (b₂ i)) (b j) = if j = i then 1 else 0) : ⇑b₁ = ⇑b₂

noncomputable def dualBasis_inM_of_perfectPairing {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : M →ₗ[A] M →ₗ[A] A) [B.IsPerfPair] (b : Module.Basis ι A M) : Module.Basis ι A M

theorem dualBasis_inM_of_perfectPairing_apply {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : M →ₗ[A] M →ₗ[A] A) [B.IsPerfPair] (b : Module.Basis ι A M) (i j : ι) : (B ((dualBasis_inM_of_perfectPairing B b) i)) (b j) = if j = i then 1 else 0

theorem prop_5_7_existence_general {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : M →ₗ[A] M →ₗ[A] A) [B.IsPerfPair] (b : Module.Basis ι A M) : ∃ (b' : Module.Basis ι A M), ∀ (i j : ι), (B (b' i)) (b j) = if j = i then 1 else 0

theorem prop_5_7_uniqueness_general {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {ι : Type u_3} [DecidableEq ι] (B : M →ₗ[A] M →ₗ[A] A) [B.IsPerfPair] (b b₁ b₂ : Module.Basis ι A M) (h₁ : ∀ (i j : ι), (B (b₁ i)) (b j) = if j = i then 1 else 0) (h₂ : ∀ (i j : ι), (B (b₂ i)) (b j) = if j = i then 1 else 0) : ⇑b₁ = ⇑b₂

theorem dualSubmodule_antitone {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (B : V →ₗ[K] V →ₗ[K] K) : Antitone (LinearMap.BilinForm.dualSubmodule B)

theorem thm_5_12_dualSubmodule_free_lattice {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] {ι : Type u_4} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) : LinearMap.BilinForm.dualSubmodule B (Submodule.span A (Set.range ⇑b)) = Submodule.span A (Set.range ⇑(LinearMap.BilinForm.dualBasis B hB b))

theorem thm_5_12_fg_key {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] {ι : Type u_4} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) (M : Submodule A V) (hbM : Submodule.span A (Set.range ⇑b) ≤ M) : LinearMap.BilinForm.dualSubmodule B M ≤ Submodule.span A (Set.range ⇑(LinearMap.BilinForm.dualBasis B hB b))

theorem thm_5_12_injective {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (N : Submodule A V) (hN : Submodule.span K ↑N = ⊤) : Function.Injective ⇑(LinearMap.BilinForm.dualSubmoduleToDual B N)

theorem cor_5_13_directSumBilinForm_nondegenerate {K : Type u_1} [Field K] {V₁ : Type u_2} [AddCommGroup V₁] [Module K V₁] {V₂ : Type u_3} [AddCommGroup V₂] [Module K V₂] (B₁ : V₁ →ₗ[K] V₁ →ₗ[K] K) (hB₁ : B₁.Nondegenerate) (B₂ : V₂ →ₗ[K] V₂ →ₗ[K] K) (hB₂ : B₂.Nondegenerate) : (directSumBilinForm B₁ B₂).Nondegenerate

theorem cor_5_13_direct_sum_dual {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V₁ : Type u_3} [AddCommGroup V₁] [Module K V₁] [Module A V₁] [IsScalarTower A K V₁] {V₂ : Type u_4} [AddCommGroup V₂] [Module K V₂] [Module A V₂] [IsScalarTower A K V₂] (B₁ : V₁ →ₗ[K] V₁ →ₗ[K] K) (B₂ : V₂ →ₗ[K] V₂ →ₗ[K] K) (M₁ : Submodule A V₁) (M₂ : Submodule A V₂) : LinearMap.BilinForm.dualSubmodule (directSumBilinForm B₁ B₂) (M₁.prod M₂) = (LinearMap.BilinForm.dualSubmodule B₁ M₁).prod (LinearMap.BilinForm.dualSubmodule B₂ M₂)

theorem cor_5_13 {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V₁ : Type u_3} [AddCommGroup V₁] [Module K V₁] [Module A V₁] [IsScalarTower A K V₁] {V₂ : Type u_4} [AddCommGroup V₂] [Module K V₂] [Module A V₂] [IsScalarTower A K V₂] (B₁ : V₁ →ₗ[K] V₁ →ₗ[K] K) (hB₁ : B₁.Nondegenerate) (B₂ : V₂ →ₗ[K] V₂ →ₗ[K] K) (hB₂ : B₂.Nondegenerate) (M₁ : Submodule A V₁) (M₂ : Submodule A V₂) : (directSumBilinForm B₁ B₂).Nondegenerate ∧ LinearMap.BilinForm.dualSubmodule (directSumBilinForm B₁ B₂) (M₁.prod M₂) = (LinearMap.BilinForm.dualSubmodule B₁ M₁).prod (LinearMap.BilinForm.dualSubmodule B₂ M₂)

theorem cor_5_14_dual_basis_property {K : Type u_2} [Field K] {V : Type u_3} [AddCommGroup V] [Module K V] {ι : Type u_4} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) (i j : ι) : (B ((LinearMap.BilinForm.dualBasis B hB b) i)) (b j) = if j = i then 1 else 0

theorem cor_5_14_dual_basis_unique {K : Type u_2} [Field K] {V : Type u_3} [AddCommGroup V] [Module K V] {ι : Type u_4} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) (v : ι → V) (hv : ∀ (i j : ι), (B (v i)) (b j) = if j = i then 1 else 0) : v = ⇑(LinearMap.BilinForm.dualBasis B hB b)

theorem cor_5_14_dual_lattice_free {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] {ι : Type u_4} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) : LinearMap.BilinForm.dualSubmodule B (Submodule.span A (Set.range ⇑b)) = Submodule.span A (Set.range ⇑(LinearMap.BilinForm.dualBasis B hB b))

structure IsLocALattice (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (S : Submonoid A) (N : Submodule A V) : Prop

• fg_loc : ∃ (T : Finset V), N = Submodule.localize S (Submodule.span A ↑T)
• span_eq_top : Submodule.span K ↑N = ⊤

def BilinForm.dualSubmoduleLoc {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (B : V →ₗ[K] V →ₗ[K] K) (S : Submonoid A) (M : Submodule A V) : Submodule A V

theorem Submodule.le_localize {A : Type u_1} [CommRing A] {V : Type u_2} [AddCommGroup V] [Module A V] (S : Submonoid A) (M : Submodule A V) : M ≤ localize S M

theorem isLocALattice_of_localize {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (S : Submonoid A) (M : Submodule A V) (hM : IsALattice A K V M) : IsLocALattice A K V S (Submodule.localize S M)

theorem dualSubmodule_isALattice {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (M : Submodule A V) (hM : IsALattice A K V M) : IsALattice A K V (LinearMap.BilinForm.dualSubmodule B M)

theorem thm_5_12_surjective {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (M : Submodule A V) (hM : IsALattice A K V M) : Function.Surjective ⇑(LinearMap.BilinForm.dualSubmoduleToDual B M)

theorem thm_5_12 {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (M : Submodule A V) (hM : IsALattice A K V M) : IsALattice A K V (LinearMap.BilinForm.dualSubmodule B M) ∧ Function.Bijective ⇑(LinearMap.BilinForm.dualSubmoduleToDual B M)

noncomputable def thm_5_12_linearEquiv {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (M : Submodule A V) (hM : IsALattice A K V M) : ↥(LinearMap.BilinForm.dualSubmodule B M) ≃ₗ[A] Module.Dual A ↥M

theorem lem_5_15_localization_dual {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (M : Submodule A V) (hM : IsALattice A K V M) (S : Submonoid A) : IsLocALattice A K V S (Submodule.localize S M) ∧ IsLocALattice A K V S (Submodule.localize S (LinearMap.BilinForm.dualSubmodule B M)) ∧ BilinForm.dualSubmoduleLoc B S (Submodule.localize S M) = Submodule.localize S (LinearMap.BilinForm.dualSubmodule B M)

theorem prop_5_16_double_dual_free {A : Type u_1} [CommRing A] {K : Type u_2} [Field K] [Algebra A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] {ι : Type u_4} [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (hB' : LinearMap.BilinForm.IsSymm B) (b : Module.Basis ι K V) : LinearMap.BilinForm.dualSubmodule B (LinearMap.BilinForm.dualSubmodule B (Submodule.span A (Set.range ⇑b))) = Submodule.span A (Set.range ⇑b)

theorem prop_2_6_lattice_eq_inter_localizations {A : Type u_5} [CommRing A] {V : Type u_6} [AddCommGroup V] [Module A V] (M : Submodule A V) (v : V) : (∀ (P : MaximalSpectrum A), ∃ s ∈ P.asIdeal.primeCompl, s • v ∈ M) → v ∈ M

theorem dvr_localize_lattice_free {A : Type u_5} [CommRing A] [IsDomain A] [IsDedekindDomain A] {K : Type u_6} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_7} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (M : Submodule A V) (hM : IsALattice A K V M) (P : MaximalSpectrum A) : ∃ (ι : Type) (x : Fintype ι) (b : Module.Basis ι K V), Submodule.localize P.asIdeal.primeCompl M = Submodule.localize P.asIdeal.primeCompl (Submodule.span A (Set.range ⇑b))

theorem double_dual_local_dvr_step {A : Type u_5} [CommRing A] [IsDomain A] [IsDedekindDomain A] {K : Type u_6} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_7} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (hB' : LinearMap.BilinForm.IsSymm B) (M : Submodule A V) (hM : IsALattice A K V M) (P : MaximalSpectrum A) (v : V) (hv : v ∈ LinearMap.BilinForm.dualSubmodule B (LinearMap.BilinForm.dualSubmodule B M)) : ∃ s ∈ P.asIdeal.primeCompl, s • v ∈ M

theorem double_dual_sub_original {A : Type u_5} [CommRing A] [IsDomain A] [IsDedekindDomain A] {K : Type u_6} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_7} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (hB' : LinearMap.BilinForm.IsSymm B) (M : Submodule A V) (hM : IsALattice A K V M) : LinearMap.BilinForm.dualSubmodule B (LinearMap.BilinForm.dualSubmodule B M) ≤ M

theorem prop_5_16_double_dual_dedekind {A : Type u_5} [CommRing A] [IsDomain A] [IsDedekindDomain A] {K : Type u_6} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_7} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (hB' : LinearMap.BilinForm.IsSymm B) (M : Submodule A V) (hM : IsALattice A K V M) : dualLattice A K V B (dualLattice A K V B M) = M

theorem dualBasis_exists {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b : Module.Basis ι K V) : ∃ (b' : Module.Basis ι K V), ∀ (i j : ι), (B (b' i)) (b j) = if j = i then 1 else 0

Alias of prop_5_7_existence.

theorem dualBasis_unique {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {ι : Type u_3} [DecidableEq ι] [Finite ι] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (b b₁ b₂ : Module.Basis ι K V) (h₁ : ∀ (i j : ι), (B (b₁ i)) (b j) = if j = i then 1 else 0) (h₂ : ∀ (i j : ι), (B (b₂ i)) (b j) = if j = i then 1 else 0) : ⇑b₁ = ⇑b₂

Alias of prop_5_7_uniqueness.

theorem dualSubmoduleToDual_injective {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (N : Submodule A V) (hN : Submodule.span K ↑N = ⊤) : Function.Injective ⇑(LinearMap.BilinForm.dualSubmoduleToDual B N)

Alias of thm_5_12_injective.

theorem directSumBilinForm_nondegenerate {K : Type u_1} [Field K] {V₁ : Type u_2} [AddCommGroup V₁] [Module K V₁] {V₂ : Type u_3} [AddCommGroup V₂] [Module K V₂] (B₁ : V₁ →ₗ[K] V₁ →ₗ[K] K) (hB₁ : B₁.Nondegenerate) (B₂ : V₂ →ₗ[K] V₂ →ₗ[K] K) (hB₂ : B₂.Nondegenerate) : (directSumBilinForm B₁ B₂).Nondegenerate

Alias of cor_5_13_directSumBilinForm_nondegenerate.

theorem localization_dual_comm {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [FiniteDimensional K V] (B : V →ₗ[K] V →ₗ[K] K) (hB : B.Nondegenerate) (M : Submodule A V) (hM : IsALattice A K V M) (S : Submonoid A) : IsLocALattice A K V S (Submodule.localize S M) ∧ IsLocALattice A K V S (Submodule.localize S (LinearMap.BilinForm.dualSubmodule B M)) ∧ BilinForm.dualSubmoduleLoc B S (Submodule.localize S M) = Submodule.localize S (LinearMap.BilinForm.dualSubmodule B M)

Alias of lem_5_15_localization_dual.