feat(Topology/Algebra/Algebra): add ContinuousAlgHom

[mariainesdff]

We add the class ContinuousAlgHom for continuous algebra homomorphisms.

Co-authored-by: Antoine Chambert-Loir [email protected]

---

[github-actions[bot]]

PR summary 2cf06ce174

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ContinuousAlgHom + Simps.apply + Simps.coe + _root_.DenseRange.topologicalClosure_map_subalgebra + _root_.Subalgebra.coe_valA + _root_.Subalgebra.coe_valA' + _root_.Subalgebra.topologicalClosure + _root_.Subalgebra.topologicalClosure_coe + _root_.Subalgebra.topologicalClosure_map + _root_.Subalgebra.valA + _root_.Subalgebra.valA_apply + _root_.Submodule.range_valA + codRestrict + coe_codRestrict + coe_codRestrict_apply + coe_coe + coe_comp + coe_comp' + coe_copy + coe_eq_id + coe_fst + coe_fst' + coe_id + coe_id' + coe_inj + coe_mk + coe_mk' + coe_mul + coe_pow + coe_prod + coe_prodMap + coe_prodMap' + coe_rangeRestrict + coe_restrictScalars + coe_restrictScalars' + coe_snd + coe_snd' + comp + comp_apply + comp_assoc + comp_id + continuous + copy + copy_eq + eqOn_adjoin_iff + eqOn_closure_adjoin + eqOn_sup + equalizer_eq_top + equalizer_same + equalizer_toSubmodule + ext + ext_iff + ext_on + ext_on_codisjoint + ext_ring + ext_ring_iff + fst + fst_comp_prod + fst_prod_snd + id + id_apply + id_comp + instance (s : Subalgebra R A) : TopologicalSemiring s + instance : AlgHomClass (A →A[R] B) R A B + instance : ContinuousMapClass (A →A[R] B) A B + instance : FunLike (A →A[R] B) A B + instance : Monoid (A →A[R] A) + instance : Mul (A →A[R] A) := ⟨comp⟩ + instance : One (A →A[R] A) := ⟨ContinuousAlgHom.id R A⟩ + instance [TopologicalSemiring A] [DiscreteTopology R] : + instance {D : Type*} [UniformSpace D] [CompleteSpace D] + le_equalizer + map_add + map_neg + map_smul + map_smul_of_tower + map_sub + map_sum + map_zero + mul_apply + mul_def + one_apply + one_def + prod + prodEquiv + prod_apply + rangeRestrict + restrictScalars + snd + snd_comp_prod + toAlgHomMonoidHom + toAlgHom_eq_coe + uniformContinuous ++ prodMap - Subalgebra.topologicalClosure - Subalgebra.topologicalClosure_coe - Subalgebra.topologicalSemiring

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[j-loreaux]

It looks like there were a bunch of comments that never got addressed (probably because they were hidden in the fold). Can you address and resolve them please?

[AntoineChambert-Loir]

I'm surprised, I had the impression to have addressed all questions.

[AntoineChambert-Loir]

Now it should be OK, sorry.

[AntoineChambert-Loir]

You were right, it was appropriate to change from submodules to subalgebras. Now, a new part of Subalgebra/Basic contains new material about AlgHom.equalizer that may deserve an independent PR (but that will be simpler if it can be avoided). Moreover, I asked here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/AlgHom.2Eequalizer.20.2F.20LinearMap.2EeqLocus/near/454500957 if AlgHom.equalizer should be renamed AlgHom.eqLocus.

[j-loreaux]

Looks so much nicer that it's phrased in terms of subalgebras now. Thanks! I appreciate the work on the Subalgebra API to get it across the line. The AlgHomClass usage is good, and as for renaming, that can always occur later if we want.

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style