Issue #259: A_K/K is compact if A_Q/Q is compact #315
Conversation
…g that A_Q/Q is compact
…g that A_Q/Q is compact
|
Is this still WIP? Note that ContinuousAlgEquiv was merged into mathlib a while ago and we've updated FLT since then. You also edited this file in #312 and I fixed the conflicts there, but the file you're editing here is long gone. |
|
This one is still WIP although nearly there, I'll let you know when it's ready for review again |
|
This is now ready to review again |
| letI := (f.toAlgHom.restrictDomain B).toRingHom.toAlgebra | ||
| C ≃ₐ[B] D where |
There was a problem hiding this comment.
Is this def actually usable? If D is already a B-algebra then this will cause a diamond perhaps. But maybe it's fine?
There was a problem hiding this comment.
Yeah you have to be careful with this one. In this PR it's used in
-- `𝔸 K ⊗[K] L ≃ₗ[𝔸 K] L ⊗[K] 𝔸 K`
let comm := (Algebra.TensorProduct.comm K (𝔸 K) L).extendScalars (𝔸 K) |>.toLinearEquiv
Which works because Algebra.TensorProduct.rightAlgebra on the RHS defeqs to Algebra.TensorProduct.includeRight.toRingHom.toAlgebra and includeRight is TensorProduct.comm.restrictDomain 𝔸 K. But the other way around
let comm := (Algebra.TensorProduct.comm K L (𝔸 K)).extendScalars (𝔸 K) |>.toLinearEquiv
causes issues. Note that AlgHom.extendScalars in mathlib is the same in this respect. Maybe the right way to state this is to add [Algebra B D] and some kind of CompatibleSMul instance?
| def QuotientAddGroup.continuousAddEquiv (G H : Type*) [AddCommGroup G] [AddCommGroup H] [TopologicalSpace G] | ||
| [TopologicalSpace H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] | ||
| (e : G ≃ₜ+ H) (h : AddSubgroup.map e G' = H') : | ||
| G ⧸ G' ≃ₜ+ H ⧸ H' := | ||
| (Submodule.Quotient.continuousLinearEquiv _ _ (AddSubgroup.toIntSubmodule G') | ||
| (AddSubgroup.toIntSubmodule H') e.toIntContinuousLinearEquiv | ||
| (congrArg AddSubgroup.toIntSubmodule h)).toContinuousAddEquiv |
There was a problem hiding this comment.
Probably all his should be done for CommGroup and then @[to_additive]d.
There was a problem hiding this comment.
Also, is there a reason why you went for map e G' = H? I would have thought that comap e H' = G' was easier to work with, because it has better definitional properties (the definition of map uses image so has an exists in, but the definition of comap uses preimage so doesn't).
There was a problem hiding this comment.
No particular reason other than using Submodule.Quotient.equiv as a model. It sounds like comap would be better!
| {y : Fin (Module.finrank K L) → K} | ||
| (h : ∀ i, algebraMap K (𝔸 K) (y i) = x i) : | ||
| piEquiv K L x = algebraMap L _ (Module.Finite.equivPi _ _ |>.symm y) := by | ||
| simp [← funext h] |
There was a problem hiding this comment.
Can you squeeze the simp?
Closes #259