From 475196c827d04565d8cfb1a98e2e6f98276ecb77 Mon Sep 17 00:00:00 2001 From: acmepjz Date: Wed, 16 Oct 2024 18:29:43 +0800 Subject: [PATCH 1/6] add --- Mathlib.lean | 1 + Mathlib/RingTheory/LinearDisjoint.lean | 451 +++++++++++++++++++++++++ 2 files changed, 452 insertions(+) create mode 100644 Mathlib/RingTheory/LinearDisjoint.lean diff --git a/Mathlib.lean b/Mathlib.lean index e2a1e20cdd35a..1b3b3bfa559a9 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3989,6 +3989,7 @@ import Mathlib.RingTheory.Kaehler.Polynomial import Mathlib.RingTheory.KrullDimension.Basic import Mathlib.RingTheory.KrullDimension.Field import Mathlib.RingTheory.LaurentSeries +import Mathlib.RingTheory.LinearDisjoint import Mathlib.RingTheory.LittleWedderburn import Mathlib.RingTheory.LocalProperties.Basic import Mathlib.RingTheory.LocalProperties.IntegrallyClosed diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean new file mode 100644 index 0000000000000..73e83e8715930 --- /dev/null +++ b/Mathlib/RingTheory/LinearDisjoint.lean @@ -0,0 +1,451 @@ +/- +Copyright (c) 2024 Jz Pan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jz Pan +-/ +import Mathlib.LinearAlgebra.LinearDisjoint +import Mathlib.LinearAlgebra.TensorProduct.Subalgebra +import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition +import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition +import Mathlib.LinearAlgebra.Basis.VectorSpace +import Mathlib.Algebra.Algebra.Subalgebra.MulOpposite +import Mathlib.Algebra.Algebra.Subalgebra.Rank +import Mathlib.RingTheory.IntegralClosure.Algebra.Defs +import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic + +/-! + +# Linearly disjoint subalgebras + +This file contains basics about linearly disjoint subalgebras. + +## Main definitions + +- `Subalgebra.LinearDisjoint`: two subalgebras are linearly disjoint, if they are + linearly disjoint as submodules (`Submodule.LinearDisjoint`). + +- `Subalgebra.LinearDisjoint.mulMap`: if two subalgebras `A` and `B` of `S / R` are + linearly disjoint, then there is `A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`. + +## Main results + +### Equivalent characterization of linearly disjointness + +- `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat`: + if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of + `R`-linearly independent elements of `A`, they are also `B`-linearly independent. + +- `Subalgebra.LinearDisjoint.of_basis_left_op`: + conversely, if a basis of `A` is also `B`-linearly independent, then `A` and `B` are + linearly disjoint. + +- `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat`: + if `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of + `R`-linearly independent elements of `B`, they are also `A`-linearly independent. + +- `Subalgebra.LinearDisjoint.of_basis_right`: + conversely, if a basis of `B` is also `A`-linearly independent, + then `A` and `B` are linearly disjoint. + +- `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat`: + if `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of + `R`-linearly independent elements `{ a_i }` of `A`, and any family of + `R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is + also `R`-linearly independent. + +- `Subalgebra.LinearDisjoint.of_basis_mul`: + conversely, if `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`, + such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent, + then `A` and `B` are linearly disjoint. + +### Other main results + +- `Subalgebra.LinearDisjoint.symm_of_commute`, `Subalgebra.linearDisjoint_symm_of_commute`: + linearly disjoint is symmetric under some commutative conditions. + +- `Subalgebra.LinearDisjoint.bot_left`, `Subalgebra.LinearDisjoint.bot_right`: + the image of `R` in `S` is linearly disjoint with any other subalgebras. + +- `Subalgebra.LinearDisjoint.sup_free_of_free`: the compositum of two linearly disjoint + subalgebras is a free module, if two subalgebras are also free modules. + +- `Subalgebra.LinearDisjoint.inf_eq_bot_of_commute`, `Subalgebra.LinearDisjoint.inf_eq_bot`: + if `A` and `B` are linearly disjoint, under suitable technical conditions, they are disjoint. + +The results with name containing "of_commute" also have corresponding specialized versions +assuming `S` is commutative. + +## Tags + +linearly disjoint, linearly independent, tensor product + +-/ + +open scoped Classical TensorProduct + +noncomputable section + +universe u v w + +namespace Subalgebra + +variable {R : Type u} {S : Type v} + +section Semiring + +variable [CommSemiring R] [Semiring S] [Algebra R S] + +variable (A B : Subalgebra R S) + +/-- If `A` and `B` are subalgebras of `S / R`, +then `A` and `B` are linearly disjoint, if they are linearly disjoint as submodules of `S`. -/ +protected abbrev LinearDisjoint : Prop := (toSubmodule A).LinearDisjoint (toSubmodule B) + +theorem linearDisjoint_iff : A.LinearDisjoint B ↔ (toSubmodule A).LinearDisjoint (toSubmodule B) := + Iff.rfl + +variable {A B} + +@[nontriviality] +theorem LinearDisjoint.of_subsingleton [Subsingleton R] : A.LinearDisjoint B := + Submodule.LinearDisjoint.of_subsingleton + +/-- Linearly disjoint is symmetric if elements in the module commute. -/ +theorem LinearDisjoint.symm_of_commute (H : A.LinearDisjoint B) + (hc : ∀ (a : A) (b : B), Commute a.1 b.1) : B.LinearDisjoint A := + Submodule.LinearDisjoint.symm_of_commute H hc + +/-- Linearly disjoint is symmetric if elements in the module commute. -/ +theorem linearDisjoint_symm_of_commute + (hc : ∀ (a : A) (b : B), Commute a.1 b.1) : A.LinearDisjoint B ↔ B.LinearDisjoint A := + ⟨fun H ↦ H.symm_of_commute hc, fun H ↦ H.symm_of_commute fun _ _ ↦ (hc _ _).symm⟩ + +namespace LinearDisjoint + +variable (A B) + +/-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/ +theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B := + Submodule.LinearDisjoint.one_left _ + +/-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/ +theorem bot_right : A.LinearDisjoint ⊥ := + Submodule.LinearDisjoint.one_right _ + +end LinearDisjoint + +end Semiring + +section CommSemiring + +variable [CommSemiring R] [CommSemiring S] [Algebra R S] + +variable {A B : Subalgebra R S} + +/-- Linearly disjoint is symmetric in a commutative ring. -/ +theorem LinearDisjoint.symm (H : A.LinearDisjoint B) : B.LinearDisjoint A := + H.symm_of_commute fun _ _ ↦ mul_comm _ _ + +/-- Linearly disjoint is symmetric in a commutative ring. -/ +theorem linearDisjoint_symm : A.LinearDisjoint B ↔ B.LinearDisjoint A := + ⟨LinearDisjoint.symm, LinearDisjoint.symm⟩ + +namespace LinearDisjoint + +variable (H : A.LinearDisjoint B) +include H + +/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are +linearly disjoint, then there is the natural isomorphism +`A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`. -/ +protected def mulMap := + (AlgEquiv.ofInjective (A.mulMap B) H.injective).trans (equivOfEq _ _ (mulMap_range A B)) + +@[simp] +theorem val_mulMap_tmul (a : A) (b : B) : (H.mulMap (a ⊗ₜ[R] b) : S) = a.1 * b.1 := rfl + +/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are +linearly disjoint, and if they are free `R`-modules, then `A ⊔ B` is also a free `R`-module. -/ +theorem sup_free_of_free [Module.Free R A] [Module.Free R B] : Module.Free R ↥(A ⊔ B) := + Module.Free.of_equiv H.mulMap.toLinearEquiv + +end LinearDisjoint + +end CommSemiring + +section Ring + +namespace LinearDisjoint + +variable [CommRing R] [Ring S] [Algebra R S] + +variable (A B : Subalgebra R S) + +lemma mulLeftMap_ker_eq_bot_iff_linearIndependent_op {ι : Type*} (a : ι → A) : + LinearMap.ker (Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a) = ⊥ ↔ + LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a) := by + -- need this instance otherwise `LinearMap.ker_eq_bot` does not work + letI : AddCommGroup (ι →₀ toSubmodule B) := Finsupp.instAddCommGroup + letI : AddCommGroup (ι →₀ B.op) := Finsupp.instAddCommGroup + simp_rw [LinearIndependent, LinearMap.ker_eq_bot] + let i : (ι →₀ B) →ₗ[R] S := Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a + let j : (ι →₀ B) →ₗ[R] S := (MulOpposite.opLinearEquiv _).symm.toLinearMap ∘ₗ + (Finsupp.linearCombination B.op (MulOpposite.op ∘ A.val ∘ a)).restrictScalars R ∘ₗ + (Finsupp.mapRange.linearEquiv (linearEquivOp B)).toLinearMap + suffices i = j by + change Function.Injective i ↔ _ + simp_rw [this, j, LinearMap.coe_comp, + LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp] + rfl + ext + simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val, + Finsupp.mapRange.linearEquiv_toLinearMap, LinearEquiv.coe_coe, + MulOpposite.coe_opLinearEquiv_symm, LinearMap.coe_restrictScalars, + Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Finsupp.linearCombination_single, + MulOpposite.unop_smul, MulOpposite.unop_op, i, j] + exact Submodule.mulLeftMap_apply_single _ _ _ + +variable {A B} in +/-- If `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of +`R`-linearly independent elements of `A`, they are also `B`-linearly independent +in the opposite ring. -/ +theorem linearIndependent_left_op_of_flat (H : A.LinearDisjoint B) [Module.Flat R B] + {ι : Type*} {a : ι → A} (ha : LinearIndependent R a) : + LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a) := by + have h := Submodule.LinearDisjoint.linearIndependent_left_of_flat H ha + rwa [mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at h + +/-- If a basis of `A` is also `B`-linearly independent in the opposite ring, +then `A` and `B` are linearly disjoint. -/ +theorem of_basis_left_op {ι : Type*} (a : Basis ι R A) + (H : LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a)) : + A.LinearDisjoint B := by + rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at H + exact Submodule.LinearDisjoint.of_basis_left _ _ a H + +lemma mulRightMap_ker_eq_bot_iff_linearIndependent {ι : Type*} (b : ι → B) : + LinearMap.ker (Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b) = ⊥ ↔ + LinearIndependent A (B.val ∘ b) := by + -- need this instance otherwise `LinearMap.ker_eq_bot` does not work + letI : AddCommGroup (ι →₀ toSubmodule A) := Finsupp.instAddCommGroup + simp_rw [LinearIndependent, LinearMap.ker_eq_bot] + let i : (ι →₀ A) →ₗ[R] S := Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b + let j : (ι →₀ A) →ₗ[R] S := (Finsupp.linearCombination A (B.val ∘ b)).restrictScalars R + suffices i = j by change Function.Injective i ↔ Function.Injective j; rw [this] + ext + simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val, + LinearMap.coe_restrictScalars, Finsupp.linearCombination_single, i, j] + exact Submodule.mulRightMap_apply_single _ _ _ + +variable {A B} in +/-- If `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of +`R`-linearly independent elements of `B`, they are also `A`-linearly independent. -/ +theorem linearIndependent_right_of_flat (H : A.LinearDisjoint B) [Module.Flat R A] + {ι : Type*} {b : ι → B} (hb : LinearIndependent R b) : + LinearIndependent A (B.val ∘ b) := by + have h := Submodule.LinearDisjoint.linearIndependent_right_of_flat H hb + rwa [mulRightMap_ker_eq_bot_iff_linearIndependent] at h + +/-- If a basis of `B` is also `A`-linearly independent, then `A` and `B` are linearly disjoint. -/ +theorem of_basis_right {ι : Type*} (b : Basis ι R B) + (H : LinearIndependent A (B.val ∘ b)) : A.LinearDisjoint B := by + rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at H + exact Submodule.LinearDisjoint.of_basis_right _ _ b H + +variable {A B} in +/-- If `A` and `B` are linearly disjoint and their elements commute, if `B` is a flat `R`-module, +then for any family of `R`-linearly independent elements of `A`, +they are also `B`-linearly independent. -/ +theorem linearIndependent_left_of_flat_of_commute (H : A.LinearDisjoint B) [Module.Flat R B] + {ι : Type*} {a : ι → A} (ha : LinearIndependent R a) + (hc : ∀ (a : A) (b : B), Commute a.1 b.1) : LinearIndependent B (A.val ∘ a) := + (H.symm_of_commute hc).linearIndependent_right_of_flat ha + +/-- If a basis of `A` is also `B`-linearly independent, if elements in `A` and `B` commute, +then `A` and `B` are linearly disjoint. -/ +theorem of_basis_left_of_commute {ι : Type*} (a : Basis ι R A) + (H : LinearIndependent B (A.val ∘ a)) (hc : ∀ (a : A) (b : B), Commute a.1 b.1) : + A.LinearDisjoint B := + (of_basis_right B A a H).symm_of_commute fun _ _ ↦ (hc _ _).symm + +variable {A B} in +/-- If `A` and `B` are linearly disjoint, if `A` is flat, then for any family of +`R`-linearly independent elements `{ a_i }` of `A`, and any family of +`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is +also `R`-linearly independent. -/ +theorem linearIndependent_mul_of_flat_left (H : A.LinearDisjoint B) [Module.Flat R A] + {κ ι : Type*} {a : κ → A} {b : ι → B} (ha : LinearIndependent R a) + (hb : LinearIndependent R b) : LinearIndependent R fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1 := + Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left H ha hb + +variable {A B} in +/-- If `A` and `B` are linearly disjoint, if `B` is flat, then for any family of +`R`-linearly independent elements `{ a_i }` of `A`, and any family of +`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is +also `R`-linearly independent. -/ +theorem linearIndependent_mul_of_flat_right (H : A.LinearDisjoint B) [Module.Flat R B] + {κ ι : Type*} {a : κ → A} {b : ι → B} (ha : LinearIndependent R a) + (hb : LinearIndependent R b) : LinearIndependent R fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1 := + Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right H ha hb + +variable {A B} in +/-- If `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of +`R`-linearly independent elements `{ a_i }` of `A`, and any family of +`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is +also `R`-linearly independent. -/ +theorem linearIndependent_mul_of_flat (H : A.LinearDisjoint B) + (hf : Module.Flat R A ∨ Module.Flat R B) + {κ ι : Type*} {a : κ → A} {b : ι → B} (ha : LinearIndependent R a) + (hb : LinearIndependent R b) : LinearIndependent R fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1 := + Submodule.LinearDisjoint.linearIndependent_mul_of_flat H hf ha hb + +/-- If `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`, +such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent, +then `A` and `B` are linearly disjoint. -/ +theorem of_basis_mul {κ ι : Type*} (a : Basis κ R A) (b : Basis ι R B) + (H : LinearIndependent R fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1) : A.LinearDisjoint B := + Submodule.LinearDisjoint.of_basis_mul _ _ a b H + +variable {A B} + +section + +variable (H : A.LinearDisjoint B) +include H + +theorem of_le_left_of_flat {A' : Subalgebra R S} + (h : A' ≤ A) [Module.Flat R B] : A'.LinearDisjoint B := + Submodule.LinearDisjoint.of_le_left_of_flat H h + +theorem of_le_right_of_flat {B' : Subalgebra R S} + (h : B' ≤ B) [Module.Flat R A] : A.LinearDisjoint B' := + Submodule.LinearDisjoint.of_le_right_of_flat H h + +theorem of_le_of_flat_right {A' B' : Subalgebra R S} + (ha : A' ≤ A) (hb : B' ≤ B) [Module.Flat R B] [Module.Flat R A'] : + A'.LinearDisjoint B' := (H.of_le_left_of_flat ha).of_le_right_of_flat hb + +theorem of_le_of_flat_left {A' B' : Subalgebra R S} + (ha : A' ≤ A) (hb : B' ≤ B) [Module.Flat R A] [Module.Flat R B'] : + A'.LinearDisjoint B' := (H.of_le_right_of_flat hb).of_le_left_of_flat ha + +end + +end LinearDisjoint + +end Ring + +section CommRing + +namespace LinearDisjoint + +variable [CommRing R] [CommRing S] [Algebra R S] + +variable (A B : Subalgebra R S) + +variable {A B} in +/-- In a commutative ring, if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, +then for any family of `R`-linearly independent elements of `A`, +they are also `B`-linearly independent. -/ +theorem linearIndependent_left_of_flat (H : A.LinearDisjoint B) [Module.Flat R B] + {ι : Type*} {a : ι → A} (ha : LinearIndependent R a) : LinearIndependent B (A.val ∘ a) := + H.linearIndependent_left_of_flat_of_commute ha fun _ _ ↦ mul_comm _ _ + +/-- In a commutative ring, if a basis of `A` is also `B`-linearly independent, +then `A` and `B` are linearly disjoint. -/ +theorem of_basis_left {ι : Type*} (a : Basis ι R A) + (H : LinearIndependent B (A.val ∘ a)) : A.LinearDisjoint B := + of_basis_left_of_commute A B a H fun _ _ ↦ mul_comm _ _ + +/-- If `A/R` is integral, such that `A'` and `B` are linearly disjoint for all subalgebras `A'` +of `A` which are finitely generated `R`-modules, then `A` and `B` are linearly disjoint. -/ +theorem of_linearDisjoint_finite_left [Algebra.IsIntegral R A] + (H : ∀ A' : Subalgebra R S, A' ≤ A → [Module.Finite R A'] → A'.LinearDisjoint B) : + A.LinearDisjoint B := by + rw [linearDisjoint_iff, Submodule.linearDisjoint_iff] + intro x y hxy + obtain ⟨M', hM, hf, h⟩ := + TensorProduct.exists_finite_submodule_left_of_finite' {x, y} (Set.toFinite _) + obtain ⟨s, hs⟩ := Module.Finite.iff_fg.1 hf + have hs' : (s : Set S) ⊆ A := by rwa [← hs, Submodule.span_le] at hM + let A' := Algebra.adjoin R (s : Set S) + have hf' : Submodule.FG (toSubmodule A') := fg_adjoin_of_finite s.finite_toSet fun x hx ↦ + (isIntegral_algHom_iff A.val Subtype.val_injective).2 + (Algebra.IsIntegral.isIntegral (R := R) (A := A) ⟨x, hs' hx⟩) + replace hf' : Module.Finite R A' := Module.Finite.iff_fg.2 hf' + have hA : toSubmodule A' ≤ toSubmodule A := Algebra.adjoin_le_iff.2 hs' + replace h : {x, y} ⊆ (LinearMap.range (LinearMap.rTensor (toSubmodule B) + (Submodule.inclusion hA)) : Set _) := fun _ hx ↦ by + have : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion + (show M' ≤ toSubmodule A' by + rw [← hs, Submodule.span_le]; exact Algebra.adjoin_le_iff.1 (le_refl _)) := rfl + rw [this, LinearMap.rTensor_comp] at h + exact LinearMap.range_comp_le_range _ _ (h hx) + obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp) + obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp) + rw [← hx', ← hy']; congr + exact (H A' hA).injective (by simp [← Submodule.mulMap_comp_rTensor _ hA, hx', hy', hxy]) + +/-- If `B/R` is integral, such that `A` and `B'` are linearly disjoint for all subalgebras `B'` +of `B` which are finitely generated `R`-modules, then `A` and `B` are linearly disjoint. -/ +theorem of_linearDisjoint_finite_right [Algebra.IsIntegral R B] + (H : ∀ B' : Subalgebra R S, B' ≤ B → [Module.Finite R B'] → A.LinearDisjoint B') : + A.LinearDisjoint B := + (of_linearDisjoint_finite_left B A fun B' hB' _ ↦ (H B' hB').symm).symm + +variable {A B} + +/-- If `A/R` and `B/R` are integral, such that any finite subalgebras in `A` and `B` are +linearly disjoint, then `A` and `B` are linearly disjoint. -/ +theorem of_linearDisjoint_finite + [Algebra.IsIntegral R A] [Algebra.IsIntegral R B] + (H : ∀ (A' B' : Subalgebra R S), A' ≤ A → B' ≤ B → + [Module.Finite R A'] → [Module.Finite R B'] → A'.LinearDisjoint B') : + A.LinearDisjoint B := + of_linearDisjoint_finite_left A B fun _ hA' _ ↦ + of_linearDisjoint_finite_right _ B fun _ hB' _ ↦ H _ _ hA' hB' + +end LinearDisjoint + +end CommRing + +section FieldAndRing + +namespace LinearDisjoint + +variable [Field R] [Ring S] [Algebra R S] + +variable {A B : Subalgebra R S} + +theorem inf_eq_bot_of_commute (H : A.LinearDisjoint B) + (hc : ∀ (a b : ↥(A ⊓ B)), Commute a.1 b.1) : A ⊓ B = ⊥ := + eq_bot_of_rank_le_one (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left H hc) + +theorem eq_bot_of_commute_of_self (H : A.LinearDisjoint A) + (hc : ∀ (a b : A), Commute a.1 b.1) : A = ⊥ := by + rw [← inf_of_le_left (le_refl A)] at hc ⊢ + exact H.inf_eq_bot_of_commute hc + +end LinearDisjoint + +end FieldAndRing + +section FieldAndCommRing + +namespace LinearDisjoint + +variable [Field R] [CommRing S] [Algebra R S] + +variable {A B : Subalgebra R S} + +theorem inf_eq_bot (H : A.LinearDisjoint B) : A ⊓ B = ⊥ := + H.inf_eq_bot_of_commute fun _ _ ↦ mul_comm _ _ + +theorem eq_bot_of_self (H : A.LinearDisjoint A) : A = ⊥ := + H.eq_bot_of_commute_of_self fun _ _ ↦ mul_comm _ _ + +end LinearDisjoint + +end FieldAndCommRing + +end Subalgebra From 559c1e01a0ded5cfb9d78b645e336814f87ca0be Mon Sep 17 00:00:00 2001 From: acmepjz Date: Wed, 16 Oct 2024 18:46:06 +0800 Subject: [PATCH 2/6] fix import --- Mathlib/RingTheory/LinearDisjoint.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean index 73e83e8715930..ef74be50e38cb 100644 --- a/Mathlib/RingTheory/LinearDisjoint.lean +++ b/Mathlib/RingTheory/LinearDisjoint.lean @@ -9,7 +9,6 @@ import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.Algebra.Algebra.Subalgebra.MulOpposite -import Mathlib.Algebra.Algebra.Subalgebra.Rank import Mathlib.RingTheory.IntegralClosure.Algebra.Defs import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic From ef201dd70275607a555c005229fdc8f93f614a88 Mon Sep 17 00:00:00 2001 From: acmepjz Date: Wed, 16 Oct 2024 21:03:16 +0800 Subject: [PATCH 3/6] add a little bit docstring --- Mathlib/RingTheory/LinearDisjoint.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean index ef74be50e38cb..2e55e6aca8b2e 100644 --- a/Mathlib/RingTheory/LinearDisjoint.lean +++ b/Mathlib/RingTheory/LinearDisjoint.lean @@ -17,6 +17,8 @@ import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic # Linearly disjoint subalgebras This file contains basics about linearly disjoint subalgebras. +We adapt the definitions in . +See the file `Mathlib/LinearAlgebra/LinearDisjoint.lean` for details. ## Main definitions From 5eb34412ce5c18cac2483a984e1b1aa0d115c6bd Mon Sep 17 00:00:00 2001 From: acmepjz Date: Wed, 16 Oct 2024 21:03:33 +0800 Subject: [PATCH 4/6] apply suggestions --- Mathlib/RingTheory/LinearDisjoint.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean index 2e55e6aca8b2e..e6d7c8d1bd7e5 100644 --- a/Mathlib/RingTheory/LinearDisjoint.lean +++ b/Mathlib/RingTheory/LinearDisjoint.lean @@ -182,12 +182,10 @@ variable [CommRing R] [Ring S] [Algebra R S] variable (A B : Subalgebra R S) +set_option maxSynthPendingDepth 2 in lemma mulLeftMap_ker_eq_bot_iff_linearIndependent_op {ι : Type*} (a : ι → A) : LinearMap.ker (Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a) = ⊥ ↔ LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a) := by - -- need this instance otherwise `LinearMap.ker_eq_bot` does not work - letI : AddCommGroup (ι →₀ toSubmodule B) := Finsupp.instAddCommGroup - letI : AddCommGroup (ι →₀ B.op) := Finsupp.instAddCommGroup simp_rw [LinearIndependent, LinearMap.ker_eq_bot] let i : (ι →₀ B) →ₗ[R] S := Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a let j : (ι →₀ B) →ₗ[R] S := (MulOpposite.opLinearEquiv _).symm.toLinearMap ∘ₗ @@ -195,9 +193,8 @@ lemma mulLeftMap_ker_eq_bot_iff_linearIndependent_op {ι : Type*} (a : ι → A) (Finsupp.mapRange.linearEquiv (linearEquivOp B)).toLinearMap suffices i = j by change Function.Injective i ↔ _ - simp_rw [this, j, LinearMap.coe_comp, - LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp] - rfl + simp_rw [this, j, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_injective, + EquivLike.injective_comp, LinearMap.coe_restrictScalars] ext simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val, Finsupp.mapRange.linearEquiv_toLinearMap, LinearEquiv.coe_coe, @@ -224,11 +221,10 @@ theorem of_basis_left_op {ι : Type*} (a : Basis ι R A) rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at H exact Submodule.LinearDisjoint.of_basis_left _ _ a H +set_option maxSynthPendingDepth 2 in lemma mulRightMap_ker_eq_bot_iff_linearIndependent {ι : Type*} (b : ι → B) : LinearMap.ker (Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b) = ⊥ ↔ LinearIndependent A (B.val ∘ b) := by - -- need this instance otherwise `LinearMap.ker_eq_bot` does not work - letI : AddCommGroup (ι →₀ toSubmodule A) := Finsupp.instAddCommGroup simp_rw [LinearIndependent, LinearMap.ker_eq_bot] let i : (ι →₀ A) →ₗ[R] S := Submodule.mulRightMap (toSubmodule A) (N := toSubmodule B) b let j : (ι →₀ A) →ₗ[R] S := (Finsupp.linearCombination A (B.val ∘ b)).restrictScalars R From 6a674079644a5efe645b77c1ec098832778ad03d Mon Sep 17 00:00:00 2001 From: Jz Pan Date: Mon, 28 Oct 2024 14:09:36 +0800 Subject: [PATCH 5/6] Apply suggestions from code review Co-authored-by: Johan Commelin --- Mathlib/RingTheory/LinearDisjoint.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean index e6d7c8d1bd7e5..b80a3cd7e521a 100644 --- a/Mathlib/RingTheory/LinearDisjoint.lean +++ b/Mathlib/RingTheory/LinearDisjoint.lean @@ -33,7 +33,7 @@ See the file `Mathlib/LinearAlgebra/LinearDisjoint.lean` for details. ### Equivalent characterization of linearly disjointness - `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat`: - if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of + if `A` and `B` are linearly disjoint, and if `B` is a flat `R`-module, then for any family of `R`-linearly independent elements of `A`, they are also `B`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_left_op`: @@ -41,7 +41,7 @@ See the file `Mathlib/LinearAlgebra/LinearDisjoint.lean` for details. linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat`: - if `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of + if `A` and `B` are linearly disjoint, and if `A` is a flat `R`-module, then for any family of `R`-linearly independent elements of `B`, they are also `A`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_right`: @@ -49,7 +49,7 @@ See the file `Mathlib/LinearAlgebra/LinearDisjoint.lean` for details. then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat`: - if `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of + if `A` and `B` are linearly disjoint, and if one of `A` and `B` is flat, then for any family of `R`-linearly independent elements `{ a_i }` of `A`, and any family of `R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is also `R`-linearly independent. From e3b75b0cf5a3cdeb3d69868bb58167ec86b0e9db Mon Sep 17 00:00:00 2001 From: acmepjz Date: Mon, 28 Oct 2024 16:55:37 +0800 Subject: [PATCH 6/6] fix --- Mathlib/RingTheory/LinearDisjoint.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/LinearDisjoint.lean b/Mathlib/RingTheory/LinearDisjoint.lean index b80a3cd7e521a..aa4a0530b4c11 100644 --- a/Mathlib/RingTheory/LinearDisjoint.lean +++ b/Mathlib/RingTheory/LinearDisjoint.lean @@ -126,12 +126,14 @@ namespace LinearDisjoint variable (A B) /-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/ -theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B := - Submodule.LinearDisjoint.one_left _ +theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B := by + rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot] + exact Submodule.LinearDisjoint.one_left _ /-- The image of `R` in `S` is linearly disjoint with any other subalgebras. -/ -theorem bot_right : A.LinearDisjoint ⊥ := - Submodule.LinearDisjoint.one_right _ +theorem bot_right : A.LinearDisjoint ⊥ := by + rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot] + exact Submodule.LinearDisjoint.one_right _ end LinearDisjoint