chore(RingTheory): Module.Flat is invariant under ULift (#37998)

From Proetale.

Author: chrisflav

Mathlib/LinearAlgebra/TensorProduct/Tower.lean

@@ -589,6 +589,30 @@ theorem tensorTensorTensorComm_eq :
 
 end tensorTensorTensorComm
 
+section
+
+universe u₁ u₂ u₃ u₄
+
+attribute [local instance] ULift.algebra' in
+/-- `ULift` commutes with tensor products. -/
+def uliftEquiv : ULift.{u₁} (M ⊗[R] N) ≃ₗ[A] ULift.{u₂} M ⊗[ULift.{u₃} R] ULift.{u₄} N :=
+  ULift.moduleEquiv ≪≫ₗ
+    AlgebraTensorModule.congr ULift.moduleEquiv.symm ULift.moduleEquiv.symm ≪≫ₗ
+    (equivOfCompatibleSMul _ _ _ _ _)
+
+variable {M N}
+
+@[simp]
+lemma down_uliftEquiv_symm_tmul (m : ULift M) (n : ULift N) :
+    ((uliftEquiv R A M N).symm (m ⊗ₜ n)).down = m.down ⊗ₜ n.down :=
+  rfl
+
+@[simp]
+lemma uliftEquiv_tmul (m : M) (n : N) : uliftEquiv R A M N ⟨m ⊗ₜ n⟩ = ⟨m⟩ ⊗ₜ ⟨n⟩ :=
+  rfl
+
+end
+
 end CommSemiring
 
 end AlgebraTensorModule

Mathlib/RingTheory/Flat/Stability.lean

@@ -29,7 +29,7 @@ We show that flatness is stable under composition and base change.
 
 public section
 
-universe u v w t
+universe u v w t t'
 
 open Function (Injective Surjective)
 
@@ -68,6 +68,19 @@ theorem trans [Flat R S] [Flat S M] : Flat R M := by
   iterate 2 apply Flat.lTensor_preserves_injective_linearMap
   exact Subtype.val_injective
 
+variable {R M} in
+@[simp]
+lemma ulift_left_iff : Flat (ULift.{t} R) M ↔ Flat R M := by
+  refine ⟨fun h ↦ .trans _ (ULift R) _, fun h ↦ ?_⟩
+  have : Module.Flat (ULift.{t} R) R := .of_ulift
+  let _ := ULift.algebra'
+  exact .trans _ R _
+
+variable {R M} in
+@[simp]
+lemma ulift_right_iff : Flat R (ULift.{t} M) ↔ Flat R M :=
+  Flat.equiv_iff ULift.moduleEquiv
+
 end Composition
 
 section BaseChange

Mathlib/RingTheory/RingHom/Flat.lean

@@ -18,7 +18,7 @@ In this file we define flat ring homomorphisms and show their meta properties.
 
 @[expose] public section
 
-universe u v
+universe u₁ u₂ u v
 
 open TensorProduct
 
@@ -170,6 +170,30 @@ lemma tensorProductMap {f : A →ₐ[S] C} {g : B →ₐ[R] D} (hf : f.Flat) (hg
 
 end
 
+lemma comp_iff_of_bijective_left {f : R →+* S} {g : S →+* T} (hg : Function.Bijective g) :
+    (g.comp f).Flat ↔ f.Flat := by
+  refine ⟨fun hf ↦ ?_, fun hf ↦ .comp hf (.of_bijective hg)⟩
+  let e := RingEquiv.ofBijective g hg
+  have : f = e.symm.toRingHom.comp (e.toRingHom.comp f) := by ext; simp
+  rw [this]
+  exact .comp hf (.of_bijective e.symm.bijective)
+
+lemma comp_iff_of_bijective_right {f : R →+* S} {g : T →+* R} (hg : Function.Bijective g) :
+    (f.comp g).Flat ↔ f.Flat := by
+  refine ⟨fun hf ↦ ?_, fun hf ↦ .comp (.of_bijective hg) hf⟩
+  let e := RingEquiv.ofBijective g hg
+  have : f = (f.comp e.toRingHom).comp e.symm.toRingHom := by ext; simp
+  rw [this]
+  exact .comp (.of_bijective e.symm.bijective) hf
+
+@[simp]
+lemma ulift_iff {f : R →+* S} : (ulift.{u₁, u₂} f).Flat ↔ f.Flat := by
+  refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
+  · rwa [← comp_ulift_eq.{u₁, u₂} f, comp_iff_of_bijective_left (Equiv.bijective _),
+      comp_iff_of_bijective_right (Equiv.bijective _)]
+  · exact .comp (.comp (.of_bijective <| Equiv.bijective _) hf)
+      (.of_bijective <| Equiv.bijective _)
+
 end RingHom.Flat
 
 section
@@ -195,3 +219,24 @@ lemma CommRingCat.inl_injective_of_flat
     |>.injective.comp (Algebra.TensorProduct.includeLeft_injective (S := R) (A := S) hg)
 
 end
+
+open CategoryTheory
+
+namespace CommRingCat
+
+/-- The morphism property of flat ring maps. -/
+def flat : MorphismProperty CommRingCat.{u} :=
+  RingHom.toMorphismProperty fun f ↦ f.Flat
+
+@[simp]
+lemma flat_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    flat f ↔ f.hom.Flat := .rfl
+
+lemma flat_ofHom_iff {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
+    flat (ofHom f) ↔ f.Flat := .rfl
+
+instance : flat.IsStableUnderCobaseChange := by
+  rw [flat, RingHom.isStableUnderCobaseChange_toMorphismProperty_iff]
+  exact RingHom.Flat.isStableUnderBaseChange
+
+end CommRingCat

Mathlib/RingTheory/TensorProduct/Maps.lean

@@ -851,3 +851,46 @@ variable {C : Subalgebra R A}
 
 lemma Subalgebra.tmul_mem_baseChange {x : A} (hx : x ∈ C) (b : B) : b ⊗ₜ[R] x ∈ C.baseChange B :=
   ⟨(b ⊗ₜ[R] ⟨x, hx⟩), rfl⟩
+
+section
+
+universe u₁ u₂ u₃ u₄ u₅
+
+variable (R S A B : Type*) [CommSemiring R] [CommSemiring S] [Algebra R S]
+  [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B]
+
+attribute [local instance] ULift.algebra' in
+/-- `ULift` commutes with tensor products of algebras. -/
+def Algebra.TensorProduct.uliftEquiv :
+    ULift.{u₁} (A ⊗[R] B) ≃ₐ[S] ULift.{u₂} A ⊗[ULift.{u₃} R] ULift.{u₄} B :=
+  AlgEquiv.trans ULift.algEquiv
+    (.trans (congr ULift.algEquiv.symm ULift.algEquiv.symm) <|
+      Algebra.TensorProduct.equivOfCompatibleSMul _ _ _ _ _)
+
+variable {A B}
+
+@[simp]
+lemma Algebra.TensorProduct.uliftEquiv_tmul (a : A) (b : B) :
+    uliftEquiv R S A B ⟨a ⊗ₜ b⟩ = ⟨a⟩ ⊗ₜ ⟨b⟩ :=
+  rfl
+
+attribute [local instance] ULift.algebra' in
+@[simp]
+lemma Algebra.TensorProduct.down_uliftEquiv_symm_tmul (a : ULift A) (b : ULift B) :
+    ((uliftEquiv R S A B).symm (a ⊗ₜ b)).down = a.down ⊗ₜ b.down :=
+  rfl
+
+attribute [local instance] ULift.algebra' in
+lemma Algebra.TensorProduct.uliftEquiv_symm_tmul (a : ULift A) (b : ULift B) :
+    (uliftEquiv R S A B).symm (a ⊗ₜ b) = ⟨a.down ⊗ₜ b.down⟩ :=
+  rfl
+
+set_option backward.isDefEq.respectTransparency false in
+attribute [local instance] ULift.algebra' in
+lemma Algebra.TensorProduct.lmul'_ulift :
+    TensorProduct.lmul' (S := ULift.{u₂} S) (ULift.{u₁} R) =
+      (TensorProduct.lmul' (S := S) R).ulift.comp
+        (uliftEquiv _ _ _ _).symm.toAlgHom := by
+  ext <;> simp
+
+end